Mathematical Physics in Lean 4

From Groups to Gravitational Waves — a from-scratch formalization of the mathematical structures of physics in dependent type theory.

A single machine-checked development that builds the core language of mathematical physics — group, ring, module, Lie and Clifford algebra; topology, smooth manifolds, differential forms, fibre bundles, de Rham and Chern–Weil theory; and then general relativity — entirely in pure Lean 4, with no Mathlib dependency. Everything is dimension-parametric: Minkowski space, Lorentz groups, curvature, and the Einstein equations are stated for general n and specialized to 4.

A 30-chapter companion book (book/main.pdf) is generated alongside the formalization: Mathematical Physics in Lean 4 — From Groups to Gravitational Waves.

Honesty note (please read)

This is a formalization, and it is explicit about its trust surface:

• 0 sorry — nothing is left as an unfinished proof.

• 365 axioms — foundational results (standard analysis/topology facts that Mathlib would otherwise supply, plus the physical field equations themselves) are stated as named axioms, and everything else is derived from them with complete proofs. Because the library deliberately takes no Mathlib dependency, the analytic scaffolding is axiomatized rather than re-proved. Verify both numbers yourself:

  grep -rE '\bsorry\b' MathPhysics --include='*.lean' | grep -v 'no sorry'   # expect: nothing
  grep -rcE '^\s*axiom\b' MathPhysics --include='*.lean' | awk -F: '{s+=$2} END{print s}'  # 365

  and #print axioms <name> in any file shows exactly which axioms a given theorem depends on. The axioms concentrate in the geometry core (Curvature.lean, ChernWeil.lean), so that is where the trust surface actually lives.

Versus Mathlib-based formalizations. This library re-derives its own algebra → geometry tower and therefore axiomatizes the analytic scaffolding (limits, integration, topology) that Mathlib would supply as theorems. The payoff is a self-contained, dependency-free, sub-minute clean build; the cost is a larger trusted axiom base — which is precisely why every module documents its axioms.

So the claim is not "general relativity proved from the axioms of type theory." The claim is: a coherent, dimension-parametric, machine-checked framework in which the theorems of the subject are stated precisely and their derivations are gap-free above a clearly labelled axiom base. Each module documents the axioms it introduces.

The headline result: dimension and gravitational waves

The Einstein tensor behaves differently in different dimensions, and the library makes this precise (MathPhysics/Relativity/EinsteinN.lean):

Dimension	Statement	Declaration	Trust
n = 2	Einstein tensor vanishes identically → no gravitational dynamics	einstein_vanishes_2d_n	axiom
n = 3	vacuum ⇒ flat → no gravitational waves (Weyl vanishes)	vacuum_3d_implies_flat	axiom
n ≥ 4	vacuum admits non-flat solutions → gravitational waves exist	vacuum_nontrivial_4d	axiom

Read this honestly: these three dimensional facts are stated as axioms — they are the classical GR results, taken as premises. What is proven is the framework around them: the Einstein equations for general n (EinsteinEquationsN), the contracted-Bianchi ⇒ energy–momentum conservation chain, and the vacuum-plus-Λ reduction G = −Λg (vacuum_cosmological_reduces, a real ~15-line proof). So "four spacetime dimensions is the minimum in which gravitational waves can propagate" is here a precisely-stated, machine-checked framework built on a postulated dimensional threshold — not a derivation of that threshold from first principles.

What's inside

Area	Modules (selected)
Algebra	groups, rings, modules, ordered fields, Lie algebras & groups, quadratic forms, Clifford & super-algebras, representations
Topology & manifolds	topological spaces, charts, tangent spaces, geometric structures
Differential geometry	differential forms, de Rham, fibre & principal bundles, Chern–Weil
Algebraic topology / TDA	homology, cohomology, simplicial complexes
Relativity	Minkowski (4 and n), Lorentz & Poincaré groups, pseudo-Riemannian geometry, Levi-Civita connection, curvature, geodesics, Einstein equations (4 and n), Schwarzschild, cosmology, causal structure, singularity theorems, ADM, black-hole thermodynamics, Cartan formulation, spinor bundles
Foundations	type theory, homotopy type theory (HoTT), category theory

63 modules, ~1,370 declarations, ~21,400 lines of Lean.

Build

lake build          # builds the whole MathPhysics library (no external dependencies)
lake exe mathphysics

Requires the Lean toolchain pinned in lean-toolchain (leanprover/lean4:v4.26.0). Because there is no Mathlib dependency, a clean build is fast.

Continuous integration

Every push and pull request runs leanprover/lean-action on GitHub's ubuntu-latest, doing a full lake build — see .github/workflows/lean_action_ci.yml. Green CI means the entire library type-checks (0 sorry) against its axiom base.

The book

book/ contains the LaTeX source and the built PDF of the 30-chapter monograph that mirrors the formalization, from Chapter 1 (groups) to Chapter 30 (advanced topics), with Chapter 18 (Einstein equations) and Chapter 19 (dimension) covering the gravitational-wave threshold above.

Citation

@misc{tata2026mathphyslean,
  title  = {Mathematical Physics in Lean 4: From Groups to Gravitational Waves},
  author = {Tata, Satya Pratheek},
  year   = {2026},
  note   = {Pure Lean 4 formalization, no Mathlib; 63 modules, 0 sorry, 365 axioms},
  url    = {https://github.com/TataSatyaPratheek/mathematical-physics-lean}
}

Author

Satya Pratheek Tata — [email protected] · github.com/TataSatyaPratheek · LinkedIn

Personal research project.

License

MIT © 2026 Satya Pratheek Tata.