News for hackers. Stuff that matters.

A comment on Formalizing Fermat's Last Theorem. Parent comment

Re:Formalizing Fermat's Last Theorem by skobes on Friday September 04, 2026 @05:54PM (#49570692)
Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?

How have we not merely substituted one verification problem for another?

[ Parent | on HN ]
Re:Formalizing Fermat's Last Theorem by Legend2440 on Friday September 04, 2026 @06:28PM (#49570980)
The point of Lean is that it can be mechanically verified by a proof checker.
[ Parent | on HN ]
Re:Formalizing Fermat's Last Theorem by sashank_1509 on Friday September 04, 2026 @08:00PM (#49571613)
Not always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful
[ Parent | on HN ]
Re:Formalizing Fermat's Last Theorem by make3 on Saturday September 05, 2026 @05:37PM (#49580936)
Lean is adversarial in a way. Lean is better thought of as a constraint language with a verifier that checks if the constraints are respected, than a programming language.

Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms.

If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.

[ Parent | on HN ]