Skip to content
/ BET Public

Project for "Machine-Checked Mathematics" at the Lorentz Center

License

Notifications You must be signed in to change notification settings

mseri/BET

Repository files navigation

Birkhoff's ergodic theorem in Lean 4

Lean build

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.

About

Project for "Machine-Checked Mathematics" at the Lorentz Center

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages