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.
In the meantime, another proof of the Birkhoff's ergodic theorem has been formalized in Lean 4: see https://github.com/lucasvreis/BirkhoffErgodicThm
Make sure that Lean 4 is installed, if not, start here.
Clone this repo
git clone https://github.com/mseri/BET.git
then enter the folder
cd BET
download mathlib's cache
lake exe cache get
and open the folder in your editor to view and edit the Lean code.
Contribution guidelines for this project.