# ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization

arXiv: https://arxiv.org/abs/2510.15981 · HTML: https://mlsanity.com/paper/2510.15981/

## Key facts

- Cited by 21 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 37 references that are in the map.
- First posted on arXiv 13 Oct 2025.

## Builds on (most cited first, 27 of 27)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [StepFun-Prover Preview: Let's Think and Verify Step by Step](https://mlsanity.com/paper/2507.20199/) (2025)
- [A New Approach Towards Autoformalization](https://mlsanity.com/paper/2310.07957/) (2023)
- [GFLean: An Autoformalisation Framework for Lean via GF](https://mlsanity.com/paper/2404.01234/) (2024)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)
- [Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving](https://mlsanity.com/paper/2507.06804/) (2025)
- [StepProof: Step-by-step verification of natural language mathematical proofs](https://mlsanity.com/paper/2506.10558/) (2025)

## Built on by (most cited first, 21 of 21)

- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [On Time, Within Budget: Constraint-Driven Online Resource Allocation for Agentic Workflows](https://mlsanity.com/paper/2605.06110/) (2026)
- [COMPOSE: Composing Future Theorems from Citations and Formal Structure](https://mlsanity.com/paper/2605.30333/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization](https://mlsanity.com/paper/2607.11307/) (2026)
- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs](https://mlsanity.com/paper/2608.15432/) (2026)
- [Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees](https://mlsanity.com/paper/2604.19000/) (2026)
- [Benchmarking Testing in Automated Theorem Proving](https://mlsanity.com/paper/2604.23698/) (2026)
- [What are the Right Symmetries for Formal Theorem Proving?](https://mlsanity.com/paper/2605.22257/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving](https://mlsanity.com/paper/2605.11905/) (2026)
- [Evaluating the Robustness of Proof Autoformalization in Lean 4](https://mlsanity.com/paper/2606.14867/) (2026)
- [Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning](https://mlsanity.com/paper/2606.15972/) (2026)
- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)
- [Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization](https://mlsanity.com/paper/2610.20573/) (2026)

## Abstract (arXiv)

Proof autoformalization, the task of translating natural language theorems and proofs into machine-verifiable code, is a critical step for integrating large language models into rigorous mathematical workflows. Current approaches focus on producing executable code, but they frequently fail to preserve the semantic meaning and logical structure of the original human-written argument. To address this, we introduce ProofFlow, a novel pipeline that treats structural fidelity as a primary objective. ProofFlow first constructs a directed acyclic graph (DAG) to map the logical dependencies between proof steps. Then, it employs a novel lemma-based approach to systematically formalize each step as an intermediate lemma, preserving the logical structure of the original argument. To facilitate evaluation, we present a new benchmark of 184 undergraduate-level problems, manually annotated with step-by-step solutions and logical dependency graphs, and introduce ProofScore, a new composite metric to evaluate syntactic correctness, semantic faithfulness, and structural fidelity. Experimental results show our pipeline sets a new state-of-the-art for autoformalization, achieving a ProofScore of 0.545, substantially exceeding baselines like full-proof formalization (0.123), which processes the entire proof at once, and step-proof formalization (0.072), which handles each step independently. Our pipeline, benchmark, and score metric are open-sourced to encourage further progress at https://github.com/Huawei-AI4Math/ProofFlow.