Lean 4 programming language and theorem prover

Scientific computing in Lean 4

A project to digitalise results from physics into Lean.

Bug-free machine learning on stochastic computation graphs

Metamath Zero specification language

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

White-box automation for Lean 4

💧 Liquid Tensor Experiment

The Lean Computer Science Library (CSLib)

A minimal development of SSA theory

LLMs + Lean, on your laptop or in the cloud

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

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

A verifier for automated and interactive proofs about transition systems.

Helper toolkit for creating your own Lean 4 UserWidgets

Experiments on automation for Lean

Interactive neural theorem proving in Lean

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

Document Generator for Lean 4

Tools based on AI for helping with 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.

Intuitive, type-safe expression quotations for Lean 4.

A static analysis tool for Lean 4.

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

Armv8 Native Code Symbolic Simulator in Lean