throw567643u8

They don't necessarily deserve credit, it is just the bare minimum courteous behaviour in academia to reach out to other researchers in the same area before publishing a result.

I'm also unaware of the quality of the consultation with the relevant mathematicians, colour me skeptical there.

I'd love to hear from a Rust programmer on the human readability of the Rust code produced in this port.

The reason Anders gave at the time was Rust effectively outlaws cyclic data structures, which was not fitting of their implementation.

lambda + DB is an antipattern.

Something is on fire. Literally or figuratively.

>Dr. Tao

Professor Tao.

No I don't have any reason to believe you are mistaken other than general suspicion.

So would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?

Has Lean proved the Four Colour Theorem? I thought only Rocq had.

AI is hopeless at using existing code, it likes to append only.

With the size of the proof object, a potential buffer overflow comes to mind.

I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.

13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.

LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.

US centric viewpoints. The UK is running out of space for landfills. Burning it is best for all.

Repo will be inactive and obsolete within 12 months.