lean4

Lean 4 programming language and theorem prover

The math library of Lean 4

Formal verification for AI: a Lean 4 + Dafny proof checker that catches fake AI proofs (reward hacking), and verified recursive self-improvement (RSI) for coding agents. AI for math, physics and software engineering.

Plan, apply and roll back changes to a production ontology, with a blast radius report and a proof an auditor can re-check.

A collection of formalized statements of conjectures in Lean.

LLMs as Copilots for Theorem Proving in Lean

An Axum-based Rust web framework for building and verifying web apps with Lean 4, featuring optional GPU acceleration and integrated development infrastructure for red-teaming and CI/CD.

Tool for data extraction and interacting with Lean programmatically.

Observer Patch Holography is a mathematically explicit approach to reconstructing physics from observers. Its executable model connects local repair to quantum measurements, clocks, and smooth effective spacetime, bringing a unified account of physics within reach.

Neovim support for the Lean theorem prover

Server to host Lean games

Lean theorem proving interface which feels like pen-and-paper proofs.

Lean Theorem Prover MCP

Scientific computing in Lean 4

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.

The "batteries included" extended library for the Lean programming language and theorem prover

White-box automation for Lean 4

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

Natural Number Game

Composable mathematics tools for agents