Trending Lean Projects

Top 35 Trending Lean Projects

1. verity

   1 134 29.1%

   Formally verified smart contracts gives mathematical certainty across all inputs and execution paths. We bet that agents will make full formal verification practical.

   

2. physlib

   2 640 8.9%

   A project to digitalise results from physics into Lean.

   

3. talos

   3 141 8.5%

   Wasm interpreter in lean, designed for reasoning (by cajal-technologies)

   

4. mathlib4

   4 3,578 6.3%

   The math library of Lean 4

   

5. verso

   5 360 5.8%

   Lean documentation authoring tool (by leanprover)

   

6. NNG4

   6 346 5.8%

   Natural Number Game

   

7. superhuman

   7 772 4.8%

   

8. formal-conjectures

   8 1,039 4.4%

   A collection of formalized statements of conjectures in Lean.

   

9. batteries

   9 404 4.2%

   The "batteries included" extended library for the Lean programming language and theorem prover (by leanprover-community)

   

10. lean4

    10 8,461 4.0%

    Lean 4 programming language and theorem prover

    

11. FLT

    11 935 3.9%

    Ongoing Lean formalisation of the proof of Fermat's Last Theorem

    

12. cedar-spec

    12 189 3.7%

    Definitional implementation of Cedar language and utilities for DRT

    

13. analysis

    13 1,814 3.4%

    A Lean companion to Analysis I

    

14. ProofWidgets4

    14 214 2.8%

    Helper toolkit for creating your own Lean 4 UserWidgets

    

15. equational_theories

    15 536 2.8%

    A project to map out the relations between different equational theories of Magmas.

    

16. SciLean

    16 517 2.1%

    Scientific computing in Lean 4

    

17. concrete

    17 330 2.1%

    Concrete is a simple programming language specifically crafted for creating highly scalable systems that are reliable, efficient, and easy to maintain. (by lambdaclass)

    

18. lean-smt

    18 296 2.0%

    Tactics for discharging Lean goals into SMT solvers.

    

19. PutnamBench

    19 242 1.7%

    An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

    

20. M40001_lean

    20 163 1.2%

    Lean 3 material related to Imperial College's "Introduction to University Mathematics" course

    

21. mm0

    21 400 0.8%

    Metamath Zero specification language

    

22. principia

    22 138 0.7%

    Rewriting Principia Mathematica in Lean (by ndrwnaguib)

    

23. Seed-Prover

    23 435 0.7%

    

24. natural_number_game

    24 304 0.3%

    Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

    

25. formalising-mathematics

    25 315 0.3%

    Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

    

26. logical_verification_2025

    26 105 0.0%

    The Hitchhiker's Guide to Logical Verification (2025 edition) and associated materials

    

27. logical_verification_2023

    27 115 0.0%

    Hitchhiker's Guide to Logical Verification (2023 Edition)

    

28. flypitch

    28 146 0.0%

    A formal proof of the independence of the continuum hypothesis

    

29. lean4-raytracer

    29 144 0.0%

    A simple raytracer written in Lean 4

    

30. formalising-mathematics-2022

    30 121 0.0%

    Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

    

31. lean4-metaprogramming-book

    31 291 0.0%

    

32. lean-liquid

    32 231 0.0%

    💧 Liquid Tensor Experiment

    

33. smalltt

    33 590 -0.3%

    Demo for high-performance type theory elaboration

    

34. functorio

    34 292 -0.3%

    

35. lean-gptf

    35 132 -0.8%

    Interactive neural theorem proving in Lean

    

Index