News for hackers. Stuff that matters.

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

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 ]