A Lean 4 + mathlib project for formalizing theorems about many-body
systems on graphs. Despite the name, the primary combinatorial
abstraction is a graph (Λ, E_Λ) — finite for finite-volume work
and infinite for the thermodynamic-limit / algebraic-formulation
work that is a major long-term goal — with concrete lattices
(1D chain, square / cubic grids, infinite chains, ℤ^d, …)
appearing as specific graph instances (SimpleGraph.pathGraph,
SimpleGraph.cycleGraph, products of these, infinite analogues, …).
This convention follows the standard mathematical-physics literature
on many-body systems on graphs.
The project subsumes and generalizes the earlier ising-model project, with the current focus on finite-volume quantum spin systems and the longer-term goal of covering Hubbard / BCS, CAR-algebraic fermion systems, the infinite-volume / thermodynamic limit (which intrinsically requires infinite graphs), and eventually lattice QCD.
This repository is written by a programmer without an academic
position, whose interests lie in non-relativistic quantum field theory
and rigorous statistical mechanics. Continuing a long-standing interest
in mathematical physics from my student days, and combined with the
goal of improving my technical skills as a programmer, I maintain
lattice-system as a personal hobby project to become proficient in
Lean 4 by formalizing results around lattice models.
The intended scope is finite-volume results in the first instance and, more gradually, the infinite-volume / algebraic formulations described in the project page. This project is not intended to interfere with the work of researchers in the field, and if any overlap arises I am happy to coordinate accordingly.
All theorems are formally proved with zero sorry, and
lake build produces zero linter warnings (Phase 4 milestone,
2026-04-23).
For the complete list of formalized theorems, the phase-by-phase progress table, and the primary textbook references used at each step, see the project page.
- Project page: https://phasetr.github.io/lattice-system/
- API documentation (doc-gen4): currently disabled because the
docs-generation CI job was consistently slow (often >1h per push
to
main). To build the API docs locally, runlake build +Mathlib:docs(or consult doc-gen4 directly). The CI job is commented out in.github/workflows/lean_action_ci.ymlwith a note on how to re-enable.
Mathematical documentation for the formalized proofs is in tex/ as
LaTeX source files. To compile:
cd tex
latexmk -pdf proof-guide.texRequires a TeX Live installation. The public proof guide currently uses
portable LaTeX packages and is verified with pdfLaTeX. LuaLaTeX remains
appropriate for documents that actually use LuaTeX/LuaTeX-ja features, but
TeX Live 2026 LuaHBTeX/luaotfload can mis-detect writable cache directories
on some sandboxed runs even when TEXMFCACHE points at a writable absolute
path. PDFs are not committed to the repository.
| File | Description |
|---|---|
tex/proof-guide.tex |
Mathematical walkthrough of the formalized proofs |
- Tasaki, H., Physics and Mathematics of Quantum Many-Body Systems — Springer
- Nielsen, M. A. and Chuang, I. L., Quantum Computation and Quantum Information — Cambridge UP
- Araki, H. and Moriya, H., Equilibrium Statistical Mechanics of Fermion Lattice Systems, Rev. Math. Phys. 15 (2003), 93-198 — World Scientific
- Bru, J.-B. and de Siqueira Pedra, W., C*-Algebras and Mathematical Foundations of Quantum Statistical Mechanics: An Introduction — Springer
- Tasaki, H., From Nagaoka's Ferromagnetism to Flat-Band Ferromagnetism and Beyond (1998) — arXiv:cond-mat/9712219
- Simon, B., The Statistical Mechanics of Lattice Gases, Vol. I — Princeton UP
- Friedli, S. and Velenik, Y., Statistical Mechanics of Lattice Systems: A Concrete Mathematical Introduction — Cambridge UP
- Glimm, J. and Jaffe, A., Quantum Physics: A Functional Integral Point of View — Springer
- Fernández, R., Fröhlich, J., and Sokal, A. D., Random Walks, Critical Phenomena, and Triviality in Quantum Field Theory — Springer
- Aarts, G., Introductory lectures on lattice QCD at nonzero baryon number (2015) — arXiv:1512.05145
- phasetr/ising-model — Upstream project; this repository reuses its conventions and infrastructure.
- leanprover-community/physlib — A physics library in Lean 4.
- YaelDillies/gibbs-measure — Lean 4 formalization project on Gibbs measures (classical).
- Lean by Example
- The Mechanics of Proof (Math 2001) by Heather Macbeth
- Mathematics in Lean
lake buildUses Lean 4.29.0 and Mathlib v4.29.0 (see lean-toolchain and
lakefile.toml).