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.

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

DeonticBench

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

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.

CTA-Bench: research benchmark and toolkit for studying how well systems turn problem descriptions and reference code into Lean 4 proof obligations, and how faithful those obligations are to the intended algorithm.

A curated list of resources for Autoformalization (Lean 4, Isabelle, etc.)

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).

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

Experimental Lean 4 proof automation system using LLM-guided aesop tactic based strategies and logging successful hints for future annotations.

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

Audited, Corrected, and Verified ProofNet Benchmark in Lean 4

Fully autonomous Lean formalizations of mathematical papers generated by the LeanFlow agent harness.