This project was initiated at the Machine-Checked Mathematics Workshop at the Lorentz Center, 10-14 July 2023.
Developed with @mseri, @marcolenci and Guillaume Dubach, under the support and supervision of Sébastien Gouëzel.
Make sure that Lean 4 is installed, if not, start here.
Clone this repo
git clone https://github.com/mseri/birkhoff.git
then enter the folder
cd birkhoff
download mathlib's cache
lake exe cache get
and open the folder in vscode to view and edit the Lean code.
Contribution guidelines for this project.