Comment by nilkn
2 months ago
Since this isn't in Lean and it's extremely easy for something like this to contain a subtle mistake, I think I'd prefer this be announced by a professional mathematician. The proof appears relatively short and elementary (not to be confused with easy -- just not using any advanced or modern machinery) so it shouldn't take long for the mathematics community to do a peer review. Without that, you could easily crank out hundreds or thousands of PDFs like this that all look plausible and are beyond the ability of a gifted amateur to review.
https://github.com/openai/cdc-lean
Perfect -- that's great to see. The proof strategy in Lean appears essentially identical to the natural language strategy (as much as is reasonably possible). I think this settles it!
But they used LateX
…and thank God it's not Lean.
Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.
Human unreadable proofs have only limited value.
5 replies →
Why not both? Not sure why you're presenting this as one or the other.
What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
4 replies →