logoalt Hacker News

seanhunter • today at 6:34 AM • 2 replies • view on HN

You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/

Replies

zone411 • today at 7:31 AM

Completely 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)
The actual proof is 13 million lines of Lean.
➕ show 2 replies
eru • today at 7:51 AM

You don't need to read the lean proof for that, only the statement.

➕ show 1 reply