Fermat's Last Theorem – how it’s going

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.