Birkhoff's ergodic theorem in Lean 4

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.

How to use

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.