alt Hacker NewsCompletely misleading.
This is all you need to read and understand for Anthropic's FLT formalization:
import Mathlib
import Theorems.Thm_fermat_last_theorem
/-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/
theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n :=
fermat_last_theorem n hn a b c ha hb hc
/-- Mathlib's named proposition, by the one-line bridge from the elementary statement
(the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/
theorem FLT_mathlib_for_comparator : FermatLastTheorem :=
fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)
Replies
u1hcw9nx • today at 8:04 AM
Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms.
Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.
➕ show 1 reply
First of all, that is Fermat's Last Theorem, not Navier-Stokes.
Second of all, you did not read the link.
> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).
Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.