The Parisi formula in Lean
A formalization of Talagrand’s 2006 proof in the exact-covariance SK model. Theorems 2.1, 2.2 and 2.4, and the final convergence of the free energy to the value given by the Parisi formula, are checked.
Computer-checked mathematics
Lean formalization
Projects in probability and statistical physics.
I use Lean to make mathematical arguments precise and mechanically checkable. These notes describe the projects, what has been proved, and what remains to be done.