This repository contains the Lean formalization of the Proposition 3 of Global optimization of Lipschitz functions, Malherbe C. and Vayatis N., 2017 and is associated the the paper A Unifying Framework for Global Optimization: From Theory to Formalization. It uses LeanGO for a formal definition of global optimization algorithms.

Install Lean 4. Then, clone the repository and run the following command in the root directory:

lake exe cache get
lake build

Now you can explore the proof using your favorite editor with Lean support, such as VSCode with the Lean 4 extension.

The documentation is available here. To build it, clone the repository and run the following command in the root directory:

lake exe cache get
lake build
cd doc
./build_manual.sh

The documentation will be generated in the html directory. You will need a local web server to view the documentation. You can use Python's built-in HTTP server:

cd doc/html
python3 -m http.server

and open your web browser at http://localhost:8000.