2 ms·
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker
by Smaug123 22d ago
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
- jmusall 22d agoThe comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.
- derkha 21d agoNo, comparator does check the entire closure
- Smaug123 21d agoI think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.