Is Mathematics a Truth Built into the Universe, or a Set of Rules Humans Made Up?

*A deep-dive essay on mathematical ontology, told in a Feynman-style narrative: from the Banach–Tarski paradox down to the foundations of mathematics, and back to the present — where AI and the Lean proof assistant are re-checking human proofs.*

1. How Can One Ball Become Two?

In 1924, Stefan Banach and Alfred Tarski proved a theorem so strange it seems impossible:

> A solid ball in 3D space can be decomposed into finitely many disjoint pieces (as few as five), which — using only rotations and translations, adding or removing nothing — can be reassembled into two balls identical to the original.

The stronger form: any two bounded solids with interior points (a pea and the Sun) can be mutually decomposed and reassembled.

The trick is not geometry but infinity. The pieces are non-measurable sets — point sets with no well-defined volume, so "volume conservation" simply doesn't apply. The construction relies on the free-group structure hidden in rotation groups (in 3D and above) and on the Axiom of Choice (AC) to select unnameable points. Historically, Banach and Tarski actually intended the result as an argument *against* AC — but the math community accepted it instead as a counterintuitive consequence of the axiom, which survived.

The essay includes an interactive switch demonstrating: with AC off (Solovay's model), all subsets of 3D space are measurable, the non-measurable fragments vanish, and the paradox evaporates.

2. 0.999… = 1: When Infinity First Makes You Uneasy

0.999… is not "approaching 1 but always falling short" — it is *defined* as the limit of 0.9, 0.99, 0.999, …, and that limit is exactly 1. In the dense order of the reals, no number fits between 0.999… and 1.

Deeper point: the real numbers themselves were only rigorously constructed in 1872, independently by Dedekind (cuts) and Cantor (Cauchy sequences). The identity holds because of the construction we chose — a hint of the essay's central question.

3. Leibniz's Infinitesimals and Their Two-Century Exile

Newton and Leibniz built calculus on dubious infinitesimals — Berkeley mocked them as "ghosts of departed quantities." By the mid-19th century, Weierstrass's ε–δ limit language expelled them.

Then around 1960, Abraham Robinson used model theory to construct the **hyperreal numbers *R* — containing genuine infinitesimals ε and infinities 1/ε — with a Transfer Principle**: any first-order statement true of ℝ is true of *R*, and vice versa (book: *Non-Standard Analysis*, 1966). Non-standard analysis remains legitimate but outside the mainstream.

4. The Foundations: ZFC and the Axiom of Choice

Modern mathematics rests on ZFC (Zermelo–Fraenkel set theory + Choice, ~10 axioms). AC is non-constructive: it guarantees a choice function exists without saying how to pick. Its non-constructiveness was suspected by Borel and Lebesgue early on; Banach–Tarski gave that suspicion a concrete target.

5. The Ceiling: Gödel's Incompleteness Theorems

In 1931, Kurt Gödel proved:

• First incompleteness theorem: any consistent formal system capable of arithmetic contains true but unprovable statements.
• Second incompleteness theorem: such a system cannot prove its own consistency.

The dream of deriving all mathematical truth from a few axioms is impossible. Gödel himself was a Platonist — for him, "unprovable" does not mean "untrue."

6. The Continuum Hypothesis: A Question ZFC Cannot Answer

Cantor asked (1878) whether an infinity lies strictly between ℵ₀ and 2^ℵ₀. The Continuum Hypothesis (CH) says no.

• 1940: Gödel showed CH (and AC) cannot be *refuted* in ZF (they hold in the constructible universe L).
• 1963: Paul Cohen invented forcing and showed CH cannot be *proved* either, winning the 1966 Fields Medal.

CH is thus independent of ZFC. Most set theorists do not read this as "CH has no answer" — rather, ZFC's ruler is too short, and new axioms (large cardinals, determinacy) may be needed. Which raises the sharper question: are new axioms *discovered* or *invented*?

7. Contemporary Echoes: Lean and AI Re-checking Human Proofs

Lean, a proof assistant initiated by Leonardo de Moura at Microsoft Research (Lean 4 stable: September 2023), machine-verifies every step of a proof via a tiny trusted kernel, backed by the community library mathlib (200,000+ theorems). Milestones:

• Liquid Tensor Experiment (July 2022): Peter Scholze's challenge to formalize his hardest theorem in condensed mathematics, completed by a community led by Johan Commelin.
• Polynomial Freiman–Ruzsa conjecture (2023): Tao and collaborators formalized the fresh proof in Lean 4 within three weeks.
• Fermat's Last Theorem formalization (2024–2029, in progress): Kevin Buzzard's team at Imperial College.
• AlphaProof (DeepMind, July 2024): achieved silver-medal level at the 2024 IMO (4 of 6 problems, 28/42), including the hardest problem solved by only 5 human contestants — combining LLM-proposed guesses with the Lean kernel as judge.

8. Conclusion: Discovered, or Invented?

Three classical positions:

• Platonism (Gödel): mathematical objects exist objectively; we survey a pre-existing landscape.
• Formalism (Hilbert): mathematics is a symbol game; CH's independence shows we can pick whichever axioms we like.
• Intuitionism (Brouwer): truth exists only in constructive proof; the law of excluded middle is questionable.

The author's view: mathematics is a collaboration between discovered structure and invented language. The universe does not write our axioms or choose our notation — yet when we try to speak precisely about infinity, continuity, and proof, it stubbornly accepts only certain kinds of statements. We invent tools to reach truths that were already there, yet can never be fully grasped.

---

*Source note: the original essay is written in a Feynman-voice narrative with mixed classical/vernacular Chinese; historical facts are multi-source verified, and the Feynman persona is inferred from his public remarks, not his own words.*