lean4

Tool for data extraction and interacting with Lean programmatically.

Lean Theorem Prover MCP

Topological Fixed-Point Theory: a machine-checked discrete compiler for the Standard Model, α⁻¹, and cosmology from two axioms. Papers, verification suite (Python/Wolfram/Lean), experiments & website.

Retrieval-Augmented Theorem Provers for Lean

AI-assisted Lean project automation with DAG blueprints, proof orchestration, and multi-agent coding/proving workflows.

Kimina Lean server (+ client SDK)

UlamAI is an open-source Lean theorem prover and formalizer.

llmstep: [L]LM proofstep suggestions in Lean 4.

A Machine-to-Machine Interaction System for Lean 4.

LeanInteract: A Python Interface for Lean 4

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.

ChatGPT plugin for theorem proving in Lean

A template for blueprint-driven formalization projects in Lean.

A universal, atomic library of mathematics and tools for agents to compose them.

A "code intepreter" for Lean

Framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.

LeanAgent is a novel lifelong learning framework for formal theorem proving that continuously generalizes to and improves on ever-expanding mathematical knowledge without forgetting previously learned knowledge.

MOTO is an automated theorem generator for science. It's a creative novelty-seeking researcher with autonomous Lean 4 proof generation. Run for days at a time once pressing start - no interaction needed! Agents working in parallel from either local host LM studio, OpenRouter, OAuth or all 3. No internet required. Star us for more!

A search engine for Lean 4 declarations

Tiny theorem prover with syntax like Lean 4 in <1K LOC