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.
- βAlloy - Lean 4 library that allows one to embedded external FFI code (currently just C) within Lean definitions.

Last modified 19d ago

Copy link

Contents

Links