autoformalization

MathForm introduces a framework for mathematical autoformalization using knowledge retrieval and verification-guided refinement, yielding the FormalVerse dataset and an 8B model that outperforms specialized baselines.

LeanFlow is an LLM agent system for translating mathematical papers into formalized Lean projects, evaluated through case studies and benchmarks with Kimi-K2.6 and GPT-5.5, achieving high completion rates within budget constraints.

This position paper argues for theory-level autoformalization, which formalizes entire theories including axioms, definitions, and lemmas as coherent libraries, rather than isolated statements. It discusses the significance, alternative views, open challenges, and proposes paths forward for this shift in formalization research.

Presents an agentic framework using general coding LLMs to autoformalize research-level mathematics into Lean 4 code, evaluated on Putnam problems and STOC conference papers.

Mistral AI releases Leanstral 1.5, an updated Lean 4 formal proof engineering model optimized for automated theorem proving and autoformalization, with 119B total parameters and 6.5B active parameters.

This paper introduces SD-GPS, a solver-driven framework for geometry problem solving that uses autoformalization guided by solver feedback and verified theorem proposing to overcome bottlenecks in neuro-symbolic systems.

This paper introduces a signal-coverage matrix that decomposes type-correctness gains in autoformalization into four strata, revealing the mechanisms behind LLM refinements and showing that headline metrics can obscure which errors are actually resolved.

This paper presents an autoformalization pipeline that translates agent prompts, MCP tool descriptions, and natural language policy documents into formally verified policies using an LLM-based generator-critic loop, achieving better coverage than hand-coded enforcement on MedAgentBench.

This paper presents an architecture that uses formally verified law as a reward signal for training legal AI, adaptively autoformalizing legal rules into a formal calculus and employing a verifier to ensure provable correctness, demonstrated on German and US law examples.

This paper evaluates the robustness of proof autoformalization models in Lean 4 under global and local perturbations, finding that current LLM-based models are sensitive to perturbations and often fail to faithfully reflect local changes.

Introduces PrologMCP, an open-source server that exposes Prolog as a stateful tool via the Model Context Protocol, enabling LLM agents to delegate reasoning to a symbolic solver. Evaluation shows competitive or superior accuracy on deductive reasoning tasks compared to frontier reasoning LLMs.

This paper presents an agent pipeline for formalizing a numerical analysis textbook in Lean 4 and introduces a quality audit framework that evaluates semantic correctness and library reuse beyond kernel acceptance, revealing common unfaithful formalization patterns.

This paper presents a case study of using a large language model (Claude Code) to formalize Grothendieck's vanishing theorem in the Lean theorem prover. It finds that while agents can produce verified code, they struggle with definitions and API design, emphasizing the need for expert review beyond mere compilation.

Researchers from Oxford, Cambridge, MIT, CMU and other institutions conduct a mixed-methods study examining how people integrate AI tools into mathematical proof formalization workflows, finding that participants generally achieve higher formalization accuracy with AI assistance while preferring to maintain high-level human control over the proof discovery process.

ATLAS is a large-scale Lean 4 library of textbook mathematics autoformalized by LLMs, covering 26 books with over 46,000 declarations. It provides reusable formal building blocks for human and machine-driven formalization.

MathAtlas is a large-scale benchmark for autoformalization of graduate-level mathematics, containing ~52k theorems and definitions extracted from 103 textbooks, with a mathematical dependency graph of ~178k relations. Experiments show state-of-the-art models achieve at most 9.8% correctness, highlighting the difficulty.