Lean 4 programming language and theorem prover

Lean 3's obsolete mathematical components library: please use mathlib4

The math library of Lean 4

Demo for high-performance type theory elaboration

White-box automation for Lean 4

Document Generator for Lean 4

A formal consistency proof of Quine's set theory New Foundations

Experiments with SAT solvers with proofs in Lean 4

Natural language tactics to teach mathematics using Lean 4

A Testing Framework for Lean

Ground Zero: Lean 4 HoTT Library

LeanSSR: an SSReflect-Like Tactic Language for Lean

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

Lean 4 port of Megaparsec

Interactive holes for Lean 4

Lean implementations of things found in Certified Programming with Dependent Types

Parser combinators for Lean

A demo implementation of a simple bidirectional type-checker in Lean 4.

Total parser combinators library for Lean4

Implementation of different type theories in Lean4

Typechecker for simpty typed lambda calculus in Lean4