New Foundations is consistent – a difficult mathematical proof proved using Lean

Original Article ↗ Hacker News Discussion ↗

Getting into Lean and Collaborative Formalization

  • Commenters share enthusiasm for the Natural Numbers Game as an accessible way to start with Lean and proofs.
  • Some want “hands‑off” ways to stay involved; suggestions include learning via such games and contributing small lemmas.
  • There is mention of blueprint-style, GitHub-like collaborative proof projects where many people formalize large theorems together.

What is Special About New Foundations (NF)?

  • NF allows a universal set; the universe forms a Boolean algebra with complements.
  • Comprehension is restricted to “stratified” formulas, enforcing a lightweight type/level discipline that blocks Russell-style paradoxes.
  • Numbers can be defined à la Frege (e.g., 3 is the set of all 3‑element sets); cardinals and ordinals are equivalence classes of sets/well‑orderings.
  • Self-membership of sets is allowed; paradoxical constructions from naive set theory instead behave in “strange” but non-contradictory ways.
  • NFU (NF with urelements) is older and easier to show consistent; urelements are simply objects that are not sets, weakening extensionality.
  • Ordered-pair definitions matter: Kuratowski’s pair causes level issues in NF, so a “type-level” Quine ordered pair is preferred.
  • NF has essentially two axiom schemes (extensionality, stratified comprehension), contrasted with many more ad hoc axioms in ZF.

Significance and Limits of the Lean Consistency Result

  • The project formalizes the difficult part of an existing NF consistency proof in Lean.
  • The consensus: it shows “if Lean’s underlying theory is consistent, then NF is consistent”; no conflict with Gödel’s incompleteness.
  • NF is thereby “as safe” as a certain (stronger) fragment of classical set theory, but not promoted as a replacement for ZFC; NFU with Choice is seen as more practical.

Gödel, Incompleteness, and Large Cardinals

  • Multiple comments clarify: a theory cannot prove its own consistency if it is strong enough, but a stronger theory can.
  • Consistency proofs always assume some stronger metatheory; this is not a workaround but inherent to how such proofs work.
  • The NF proof rests on a relatively mild set-theoretic strength (e.g., existence of certain infinite cardinals), still stronger than NF itself.
  • Discussion notes subtle points: self-verifying weak theories exist, but not at the strength of Peano arithmetic / ZFC.

Trust, Kernels, and Bugs in Proof Assistants

  • One side argues Lean is just “another system with bugs and libraries,” so it’s not a magical gold standard.
  • Others respond that for soundness you only need to trust the small kernel; all libraries reduce to kernel-checked proof terms.
  • Libraries can be “wrong” only in the sense of definitions not matching intended mathematics, not in allowing false theorems if the kernel is correct.
  • There is acknowledgment of real-world kernel bugs in other provers and the possibility of subtle Lean bugs or hardware faults, but these are seen as far rarer than human proof errors.
  • Suggested mitigations: independent checkers, multiple implementations (as in Metamath), running proofs on different platforms.

Machine vs Human Proofs and Specification Risk

  • Many comments argue machine-checked proofs are superior at verification: they don’t get bored, and every step is formally checked.
  • The main remaining risk is specification: whether the formal statement and definitions actually capture the intended mathematics.
  • This risk exists equally in informal mathematics; test suites of basic lemmas and examples are proposed as partial safeguards.
  • Some emphasize that humans remain essential for mapping between natural-language mathematics and formal statements.

LLMs, Proof Search, and Advanced Mathematics

  • Debate over whether LLMs can help with deep, baroque theories (e.g., IUT/abc conjecture).
  • Skeptics say current LLMs only handle trivial lemmas; proponents note LLM-guided proof search has already modestly improved automated provers.
  • There is speculation that building an AI to understand very difficult work might be easier than humans understanding it, but others stress LLMs still mainly tackle proof-search, not high-level conceptual modeling.

Comparisons to Other Major Proofs

  • The NF result is contrasted with:
    • Computer-aided validations like the Four Color Theorem and the Kepler Conjecture.
    • The Liquid Tensor Experiment, where the original author already believed the proof but wanted computer confirmation.
    • Controversial long proofs such as the claimed abc-conjecture proof, which many experts find impenetrable; NF’s proof is described as complicated but comprehensible and thus more amenable to formalization.

Impact on Foundations and Future of NF

  • Some commenters like the aesthetics and intuitive appeal of a universal set and simple axioms.
  • Others find NF “odd” and prefer Zermelo-style foundations pragmatically, even if NF is philosophically attractive.
  • The result is seen less as “ZFC is dead” and more as: NF is now a fully respectable alternative foundation with verified consistency relative to mainstream set theory.