LeanGO is a Lean 4 library dedicated to the formalization of global optimization algorithms and is associated the the paper A Unifying Framework for Global Optimization: From Theory to Formalization.
For more details on the theoretical background, specifically the consistency of stochastic iterative algorithms, please refer to the documentation.
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).
Some examples of how to use LeanGO can be found in the Examples directory. In particular, the file PRS.lean contains the formalization of the Pure Random Search algorithm, which is the simplest global optimization algorithm.
To see a more complex example of how to use LeanGO, check out LipoCons : the formalization of the equivalence between consistency and convergence in probability for Lipschitz functions.