LeanGO is a Lean 4 library dedicated to the formalization of global optimization algorithms.
For more details on the theoretical background, specifically the consistency of stochastic iterative algorithms, please refer to the documentation:
LipoCons — Stochastic iterative algorithm
To use LeanGO in your Lean 4 project, add the following dependency to your lakefile.lean:
require LeanGO from git "https://github.com/gaetanserre/LeanGO" @ "main"or to your lakefile.toml:
[[require]]
name = "leango"
git = "https://github.com/gaetanserre/LeanGO"Then, run lake update to fetch the package (or lake update leango if your project has already fetched other dependencies).
To see a complex example of how to use LeanGO, check out LipoCons : the formalization of the equivalence between consistency and convergence in probability for Lipschitz functions.