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.