HopfieldNet | Reservoir

Hopfield Networks

This repository contains Lean formalizations related to Hopfield Networks written in the Lean theorem prover language.

Main web page for this project.
Web blueprint, containing a human-readable version of the project.
Dependency graph of the theorems in the projects.
PDF form of blueprint, a downloadable, human-readable version of the database stored as a single file.

Below is a brief overview of the key files:

HN.Core.lean – Formalization of general neural networks.
HN.Asym.lean – Formalization of asymmetric Hopfield networks.
HN.lean – Formalization of symmetric Hopfield networks.
Stochastic.lean – Formalization of stochastic algorithms.
HN.aux.lean – Auxiliary lemmas.
HN.test.lean – Computations and implementation of the Hebbian learning algorithm.
DetailedBalance.lean – Formalization of the detailed balance property for Hopfield networks.
HN.aux.lean – Markov Chain Framework.
BM.Core.lean – Formalization of Boltzmann Machines (BMs).
BM.Markov.lean – Formalization of probability distributions for Boltzmann Machines.

For more details, see the individual files.

Installing Lean can be done by following the leanprover community website. Our project uses Lean version 4.18.0.

This repository can then be cloned by following the instructions on this page.

See LICENSE.md