A Lean 4 + mathlib project for formalizing theorems about the Ising model.
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 started ising-model as a personal hobby project to become
proficient in Lean 4 by formalizing results around the Ising model.
The intended scope is limited to finite-volume results such as correlation inequalities and the infinite volume limit of correlation functions. 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.
For the complete list of formalized theorems, axioms, and the Glimm–Jaffe chapter-by-chapter progress table, see the project page.
- Project page: https://phasetr.github.io/ising-model/
- API documentation (doc-gen4): temporarily unavailable (automatic publication paused). See note below.
Note: automatic publication of the doc-gen4 API reference to GitHub Pages is currently paused because each main-push run of the
docsjob was taking roughly an hour and queuing up behind every merge. Thedocsjob in.github/workflows/lean_action_ci.ymlis commented out until we accelerate the docgen step (caching, a scheduled run, or an alternative pipeline). To build the API reference locally, runlake -R -Kenv=dev build IsingModel:docsand open.lake/build/doc/index.html.
Mathematical documentation for the formalized proofs is in tex/ as
LaTeX source files. To compile:
cd tex
latexmk -lualatex -f -interaction=nonstopmode proof-guide.texRequires a TeX Live installation with LuaLaTeX. PDFs are not committed to the repository.
| File | Description |
|---|---|
tex/proof-guide.tex |
Mathematical walkthrough of the formalized proofs |
- Glimm, J. and Jaffe, A., Quantum Physics: A Functional Integral Point of View — Springer
- 田崎晴明, 原隆, 『相転移と臨界現象の数理』 — 共立出版
- 江沢洋, 新井朝雄, 『場の量子論と統計力学』 — 日本評論社
- YaelDillies/gibbs-measure — Lean 4 formalization project on Gibbs measures
- leanprover-community/physlib — A physics library in Lean 4
- Friedli, S. and Velenik, Y., Statistical Mechanics of Lattice Systems: A Concrete Mathematical Introduction — Cambridge UP
- Simon, B., The Statistical Mechanics of Lattice Gases, Vol. I — Princeton UP
- Ellis, R.S., Entropy, Large Deviations, and Statistical Mechanics — Springer
- Dembo, A. and Zeitouni, O., Large Deviations Techniques and Applications — Springer
- The Mechanics of Proof (Math 2001) by Heather Macbeth
- Mathematics in Lean