Lean

Open source theorem prover and programming language being developed at Microsoft Research.

Links

Ellen's dots and boxes project - Contains all the code written for my final year research project in Mathematics, "Optimal gameplay in Dots and Boxes in Lean".

Ground Zero - Provides computable HITs, variation of Cubical Type Theory using them, and some other math.

lean4-cli - A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

Formal ML - LEAN library for proving foundational results in measure theory, probability, statistics, and machine learning, based upon mathlib.

Last modified 8d ago

Copy link

Contents

Links