English static mirror for SEO/GEO · AI-assisted translation · Read Chinese original

Is Mathematics Discovered or Invented? From the Banach–Tarski Paradox to Formal Verification

Forum topic · ✨步子哥 · 2026-08-24

Summary

This essay explores the ontological status of mathematics through eight perspectives: the Banach–Tarski paradox (a solid ball cut into non-measurable pieces and reassembled into two identical balls via rotations and translations), the identity 0.999… = 1, Leibniz's infinitesimals and Abraham Robinson's non-standard analysis, the ZFC axiom system and the Axiom of Choice, Gödel's incompleteness theorems, the independence of the Continuum Hypothesis (Gödel 1940, Cohen's forcing 1963), and modern formal verification using Lean, mathlib, and DeepMind's AlphaProof. It argues that mathematical truths depend on chosen axioms, while some structures resist arbitrary conventions. The piece frames Platonism, formalism, and intuitionism as complementary lenses rather than rivals, suggesting mathematics is a collaboration between discovered structures and invented language.

Key points

1. The Banach–Tarski Paradox

Published in 1924 by Stefan Banach and Alfred Tarski, the theorem states: a solid ball in 3D space can be decomposed into a finite number of non-overlapping pieces (minimum five), then reassembled by rotations and translations alone into two balls identical to the original. The strong form implies a pea could be rearranged into the sun. The "trick" is not geometry but infinity: the pieces are non-measurable point sets (no conventional volume), made possible because 3D rotation groups contain free-group structure (absent in 1D and 2D), combined with the Axiom of Choice. Originally the authors intended to refute AC; instead, the theorem became the canonical example of AC's counter-intuitive consequences.

2. Why 0.999… = 1

The equality holds because 0.999… is defined as the limit of the sequence 0.9, 0.99, 0.999, …, which equals 1. By the density of the reals, no real number exists strictly between 0.999… and 1. The rigorous construction of the reals (Dedekind cuts, Cauchy sequences) dates only to 1872; under a different construction, the result might differ, foreshadowing the core question of the essay.

3. Leibniz's Infinitesimals and Non-Standard Analysis

Newton and Leibniz used "ghosts of departed quantities" to build calculus, provoking Berkeley's mockery. In the mid-19th century, Weierstrass and others expelled infinitesimals via ε–δ limits. Around 1960, logician Abraham Robinson used model theory to rigorously construct the hyperreals *, containing true infinitesimals ε (0 < ε < 1/n for all positive n) and infinite numbers Ω = 1/ε. His 1966 book *Non-Standard Analysis* restored Leibniz's ghosts with formal justification via the Transfer Principle: any first-order statement true of ℝ is true of *ℝ. Non-standard analysis remains a minority tool—most mathematicians still prefer ε–δ.

4. Foundations: ZFC and the Axiom of Choice

Modern mathematics rests on ZFC (Zermelo–Fraenkel set theory + Choice), roughly ten axioms from which natural numbers, reals, functions, and spaces are built. AC allows selecting one element from each of infinitely many non-empty sets. It is non-constructive: existence is guaranteed, but the selector is not specified. Solovay later proved that if AC is disabled, every subset of 3D space becomes measurable, eliminating non-measurable sets and dissolving the Banach–Tarski paradox.

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

In 1931, Kurt Gödel proved:
  • First incompleteness: any consistent formal system capable of arithmetic contains true-but-unprovable statements.
  • Second incompleteness: such a system cannot prove its own consistency.
  • Gödel himself was a Platonist—he believed mathematical truths exist objectively even when axioms cannot reach them.

    6. The Continuum Hypothesis

    Cantor (1878) asked whether there is an infinity strictly between the countable naturals (ℵ₀) and the reals. The Continuum Hypothesis (CH) says no: 2^ℵ₀ = ℵ₁. Hilbert listed it as the first of his 23 problems in 1900. Gödel (1940) showed CH cannot be disproved in ZF; Paul Cohen (1963) invented forcing to show CH cannot be proved either, winning the 1966 Fields Medal. CH is independent of ZFC: the standard axioms cannot decide it.

    7. Modern Echoes: Lean and AI Verify Human Proofs

    Lean (Lean 4 released September 2023), with the community mathlib (200,000+ theorems), is a proof assistant that checks each step mechanically—impartial and tireless. Milestones:
  • Liquid Tensor Experiment (July 2022): Peter Scholze's condensation-mathematics theorem was fully formalized in Lean, ~1.5 years after challenge.
  • Polynomial Freiman–Ruzsa conjecture (2023): Tao and collaborators formalized a fresh proof in Lean in roughly three weeks.
  • Fermat's Last Theorem formalization (2024–2029 ongoing): Buzzard's team at Imperial College.
  • AlphaProof (DeepMind, July 2024): achieved IMO silver-medal level (28/42, 4 of 6 problems), including the hardest problem solved by only 5 human contestants.
  • 8. Conclusion: Discovery, Invention, or Both?

    Three positions:
  • Platonism (Gödel): mathematical objects exist objectively; we discover them.
  • Formalism (Hilbert): mathematics is symbol manipulation; axioms are arbitrary; CH's independence proves the point.
  • Intuitionism (Brouwer): truth exists only in constructive proofs; non-constructive results (via AC) are suspect.
The essay concludes mathematics is a collaboration between discovered structure and invented language: the universe does not write our axioms, but it stubbornly accepts only certain formulations when we try to describe infinity, continuity, and proof.

Sources verified

Banach–Tarski (1924, 5 pieces, AC, non-measurable sets); 0.999… = 1 via Dedekind/Cantor 1872; Robinson 1960/1966 non-standard analysis; Gödel 1940, Cohen 1963; Lean 4 / mathlib / AlphaProof 2024.

Tags

#mathematics#philosophy-of-mathematics#banach-tarski-paradox#axiom-of-choice#godel-incompleteness#continuum-hypothesis#lean-theorem-prover#non-standard-analysis

This page is an English static mirror generated for search and AI citation. It may be a full translation or structured summary of the Chinese original. Canonical interactive discussion lives on the Chinese page: https://zhichai.net/topic/178633935