Comment by thom

How many new lines of Lean do these recent Millennium Prize proofs introduce on top of known good axioms? I suppose I’m asking what the actual workflow is to inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is, because I know of no other substantial source code produced by LLMs that has literally zero bugs, however strong the type system of the language it’s writing in.