Lean 4 programming language and theorem prover

Cosette is an automated SQL solver.

A project to digitalise results from physics into Lean.

The Lean Computer Science Library (CSLib)

Scientific computing in Lean 4

Bug-free machine learning on stochastic computation graphs

Metamath Zero specification language

White-box automation for Lean 4

Simple verification of Rust programs via functional purification in Lean 2(!)

Lean documentation authoring tool

💧 Liquid Tensor Experiment

A minimal development of SSA theory

A verifier for automated and interactive proofs about transition systems.

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

LLMs + Lean, on your laptop or in the cloud

Helper toolkit for creating your own Lean 4 UserWidgets

A simple REPL for Lean 4, returning information about errors and sorries.

Experiments on automation for Lean

Document Generator for Lean 4

Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.

Interactive neural theorem proving in Lean

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

A static analysis tool for Lean 4.

Tools based on AI for helping with Lean 4

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.