autoformalization

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

LeanInteract: A Python Interface for Lean 4

[ICML2026] The first, fully verified, sorry-free, large-scale Lean 4 library for statistical learning theory, covering infrastructures for mordern statistics and learning theory.

Workspace-first orchestration for long-horizon Lean 4 formalization agents.

A graph-engineering agent harness for long-horizon, research-level autoformalization.

DeonticBench

A repo to document candidate solutions for Erdős problems produced via LLM-driven proof search

A calibrated faithfulness screen for informal↔Lean 4 pairs, on the command line and over MCP. Screens only, never certifies.

[ICLR 2026] Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning

The AI mathematician that breaks conjectures before proving them, discharges every step inside a proof assistant, and hands you a proof you can check yourself.

A selected list of Autoformalization papers, projects, frameworks, libraries, tools, and other resources.

Mathlib is the library of mathematics. This is the library of everything else that's provable - kernel-checked Lean 4 proofs of the mechanisms that run markets and institutions, formalized autonomously from plain-English blueprints.

Levee autoformalizes your rulebook (business logic, domain constraints, policy docs) into Lean 4 specs, then enforces them against AI agents at runtime. Formal verification for agentic AI: rules an LLM agent can’t talk its way around.

Companion page for "Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery." A curated four-axis index covering MWPs, LLMs and reasoning models, multimodal geometry, Lean theorem proving, and verified discovery (FunSearch, AlphaEvolve, Erdős problems).

Official implementation of FormalEvolve, accepted to Findings of EMNLP 2026. Neuro-symbolic Lean 4 autoformalization.

Content from my bachelor thesis at UnB (in progress...)

An AI proof pipeline whose only judge is the Lean compiler. A file whose proof is 'sorry' compiles and exits 0 - so certification here means: compiles, no cheat rules, kernel axiom report clean, statement untouched by the model.

AI math workspace where the Lean 4 compiler is the oracle — natural-language questions become machine-verified proofs, and hard theorems become claim graphs proved node by node.

Typed text-to-AST parsing, symbolic verification, and selective prediction for executable quantitative clinical constraints.

Lean formalization of how behavioral equivalence checking can be generalized through abstract intrepretation