# Formalized Hopfield Networks and Boltzmann Machines

arXiv: https://arxiv.org/abs/2512.07766 · HTML: https://mlsanity.com/paper/2512.07766/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 71 references that are in the map.
- First posted on arXiv 8 Dec 2025.

## Builds on (most cited first, 22 of 22)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Hopfield Networks is All You Need](https://mlsanity.com/paper/2008.02217/) (2020)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Ising formulations of many NP problems](https://mlsanity.com/paper/1302.5843/) (2013)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Training Deep Boltzmann Networks with Sparse Ising Machines](https://mlsanity.com/paper/2303.10728/) (2023)
- [Developing Bug-Free Machine Learning Systems With Formal Mathematics](https://mlsanity.com/paper/1706.08605/) (2017)
- [HepLean: Digitalising high energy physics](https://mlsanity.com/paper/2405.08863/) (2024)
- [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020)
- [Formalizing Chemical Physics using the Lean Theorem Prover](https://mlsanity.com/paper/2210.12150/) (2022)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [A Formalization of the Generalized Quantum Stein's Lemma in Lean](https://mlsanity.com/paper/2510.08672/) (2025)
- [A formally verified proof of the Central Limit Theorem](https://mlsanity.com/paper/1405.7012/) (2014)
- [Formalization of a Stochastic Approximation Theorem](https://mlsanity.com/paper/2202.05959/) (2022)
- [Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq](https://mlsanity.com/paper/2301.12893/) (2023)
- [A Separation Logic for Concurrent Randomized Programs](https://mlsanity.com/paper/1802.02951/) (2018)
- [Verification of ML Systems via Reparameterization](https://mlsanity.com/paper/2007.06776/) (2020)
- [A Formalization of Doob's Martingale Convergence Theorems in mathlib](https://mlsanity.com/paper/2212.05578/) (2022)
- [Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL](https://mlsanity.com/paper/2108.10868/) (2021)
- [Digitalizing Wick's theorem](https://mlsanity.com/paper/2505.07939/) (2025)

## Built on by (most cited first, 2 of 2)

- [TorchLean: Formalizing Neural Networks in Lean](https://mlsanity.com/paper/2602.22631/) (2026)
- [Benign Loss Landscapes Can Coexist with Worst-Case Hardness](https://mlsanity.com/paper/2609.13057/) (2026)

## Abstract (arXiv)

Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean~4 formalization covering both deterministic and stochastic models. We first formalize Hopfield networks -- recurrent networks that store patterns as stable states -- and prove their convergence, and the correctness of Hebbian learning, the rule that updates parameters to encode patterns. We then turn to stochastic networks, whose probabilistic updates converge to a stationary distribution: we formalize the dynamics and learning of Boltzmann machines and prove their ergodicity -- convergence to a unique stationary distribution -- via a new formalization of the Perron--Frobenius theorem.