Stars
Lean 4 programming language and theorem prover
Lean 3's obsolete mathematical components library: please use mathlib4
A project to digitalise results from physics into Lean.
The "batteries included" extended library for the Lean programming language and theorem prover
Tactics for discharging Lean goals into SMT solvers.
Helper toolkit for creating your own Lean 4 UserWidgets
Lean 4 kernel / 'external checker' written in Lean 4
Experiments on automation for Lean
A zero-knowledge Lean4 compiler and kernel
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Intuitive, type-safe expression quotations for Lean 4.
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
A deprecated equality saturation tactic for Lean based on egg.
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
(Mirror) A Machine-to-Machine Interaction System for Lean 4
computable implementation of real numbers in Lean4
CLEVER: Code Lean Evaluation for Verified End-to-end Reasoning
A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo
Lean 4 library for pretty printing expressions as LaTeX
Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
Hand-written verified Lean solutions for the HumanEval benchmark
A Foreign Function Interface (FFI) to cvc5 solver in Lean.