Tool for data extraction and interacting with Lean programmatically.

Retrieval-Augmented Theorem Provers for Lean

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

ChatGPT plugin for theorem proving in Lean

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

Kimina Lean server (+ client SDK)

Lean Theorem Prover MCP

A "code intepreter" for Lean

A template for blueprint-driven formalization projects in Lean.

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

LeanInteract: A Python Interface for 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.

A search engine for Lean 4 declarations

Python client to interact with the lean4 language server.

List of the output of #help command of mathlib4, including list of all tactics, commands...etc

Implementation and subsequent optimization for "Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models"

Lean coding problem solving challenge website with proof verification

Deploying High-Performance Lean 4 Server in One Click

A work-in-progress Lean 4 binding to GiNaC

A Lean (4) type checker written in RPython