Fermat's Last Theorem – how it’s going

Original Article ↗ Hacker News Discussion ↗

Efforts to formally verify the modern proof of Fermat’s Last Theorem in the Lean proof assistant are exposing gaps and errors in “well known” parts of the mathematical literature, especially in deep areas like crystalline cohomology. Commenters debate what this says about human-written proofs, the limits imposed by Gödel’s incompleteness theorems, and the blurry boundary between mathematics and computer science, while generally agreeing that mechanized proof systems will become essential for checking large, intricate theories. Many see this as both a quality-control tool and a cultural shift: moving from socially trusted, partially implicit arguments toward machine-checkable libraries of theorems that future mathematics can safely build on.

Role of theorem provers and Lean

  • Many see Lean and similar proof assistants as the future of serious mathematics, analogous to compilers and type checkers: formal proofs as “programs” and Lean as their checker.
  • The FLT project is cited as evidence that formalization can catch subtle issues in “standard” arguments that human experts gloss over.
  • Others stress that Lean is aimed at formal math, not at replacing human intuition or solving Hilbert’s original “complete decision procedure” dream.

State of mathematical literature and FLT formalization

  • Multiple commenters argue modern math papers often omit crucial details, rely on folklore, and are effectively unreadable without expert guidance.
  • The FLT formalization bumped into an incorrect or at least misstated lemma in crystalline cohomology, reinforcing concerns about the reliability of long, technical proof chains.
  • Some believe the surrounding theory is almost surely salvageable because it has been heavily used without contradictions; others distrust that heuristic.

Foundations, incompleteness, and math vs computer science

  • There is extended debate on whether “math is CS” or “CS is math,” with consensus that there is a large overlap.
  • Gödel and incompleteness are invoked: one side claims they show full formalization/AI math is fundamentally limited; others counter that:
    • Incompleteness applies to any sufficiently strong formal system, but does not prevent formalizing enormous swathes of existing math.
    • The obstruction is to complete decidability, not to writing down or checking proofs.
  • Technical side-thread on first- vs second-order Peano arithmetic, Z₂, and whether their axioms are computably enumerable, plus discussion of constructivism vs classical math.

Proof detail, documentation, and pedagogy

  • Many criticize “obvious,” “standard,” and “left to the reader” gaps, especially in advanced areas, calling it a kind of hazing that propagates opaque arguments.
  • Others argue that fully writing out every epsilon-delta and asymptotic estimate would make papers unusably long; details are better relegated to books, appendices, or later expositions.
  • Formalization is proposed as a way to separate high-level ideas (papers, talks) from fully rigorous details (machine-checked libraries).

Practical experience with Lean and formalization

  • Lean libraries (e.g., mathlib, FLT blueprint) are praised as “databases of theorems”; tactics can often fill in small steps, but automation is still limited.
  • Users report both satisfaction and frustration: formalizing even undergraduate complex analysis involves heavy boilerplate, tricky casts (ℕ→ℝ→ℂ), and typeclass inference issues.
  • Proof assistants still need “unit tests” (example lemmas, edge-case checks) and good meta-programming/tactics; some see room for a new “big idea” to make large-scale formalization less tedious.

Reliability and soundness of Lean

  • Lean has a small kernel that has been independently checked; soundness bugs have occurred but were quickly fixed.
  • Some note that soundness also depends on the underlying type theory being mathematically consistent, which is accepted folklore but not itself machine-verified.
  • Overall sentiment: a catastrophic kernel bug is possible but considered unlikely; more likely errors lie in particular formalized developments.

Scope and limits of formalization

  • Formalizing all existing math would take vast effort; requiring Lean proofs for every new result is seen by some as tantamount to halting new research for a generation.
  • Others argue for a gradual, high-value-target approach: big theorems, central theories, and heavily reused foundations should eventually be formalized.
  • Several expect a “chain reaction”: as libraries grow, new formalizations become easier and more attractive.

Cultural and educational reflections

  • Some engineers and non-specialists feel intimidated by the level of abstraction in FLT-related work; others point out similar “unwritten lore” and opacity in large software systems.
  • A recurring theme is that intuition, high-level perspective, and good exposition matter as much as raw technical manipulations; formalization is seen as a complement, not a replacement.
  • There is broad enthusiasm for using formal methods to restore confidence in large proofs, even among those skeptical about full, universal adoption.