---
title: "ProofFlow — paper by Cabral et al. (2025) — summary and ideas"
description: "The pipeline first builds a directed acyclic graph of the proof's steps and the logical dependencies… 40 references, cited by 5 papers here."
authors: ["Rafael Cabral", "Tuan Manh Do", "Xuejun Yu", "Wai Ming Tai", "Zijin Feng", "Xin Shen"]
year: 2025
venue: "arXiv:2510.15981"
source: "https://arxiv.org/abs/2510.15981"
doi: "10.48550/arxiv.2510.15981"
arxiv: "2510.15981"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/cabral-2025-proofflow-dependency-graph-approach-faithful/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/cabral-2025-proofflow-dependency-graph-approach-faithful/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/14/) / ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization

# ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization

**Authors:** Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, [Zijin Feng](https://md.research.elamur.ai/free/en/authors/zijin-feng/) and Xin Shen · **Year:** 2025 · **Venue:** arXiv:2510.15981 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2510.15981) · [PDF](https://arxiv.org/pdf/2510.15981) · [DOI 10.48550/arxiv.2510.15981](https://doi.org/10.48550/arxiv.2510.15981) · [arXiv 2510.15981](https://arxiv.org/abs/2510.15981) · [OpenAlex](https://openalex.org/W4415948562)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · 5 in our library, of the 149,439 papers whose bibliographies we read

## Summary
Translating human-written mathematical proofs into code that a proof assistant can check is usually judged by whether the output compiles. Compiled code, however, often drifts from the author's actual reasoning: tactics merge several steps, skip others, or rely on premises the original argument never used. ProofFlow, from Huawei's Celia Team and Noah's Ark Lab, makes preserving proof structure an explicit goal. The pipeline first builds a directed acyclic graph of the proof's steps and the logical dependencies among them. It then writes each step as a separate Lean 4 lemma whose hypotheses are only that step's predecessors in the graph.

For evaluation, the authors created ProofFlowBench, a hand-annotated set of undergraduate problems with step-level solutions and dependency graphs. They also proposed ProofScore, a combined measure of compilation, meaning preservation and structural agreement. ProofFlow clearly outperforms baselines that translate the whole proof at once or each step in isolation. This matters because faithful formalization lets mathematicians check their own arguments and locate gaps or mistakes in them.

## Key points
- ProofFlow reaches a ProofScore of 0.545. The full-proof baseline scores 0.123 and the independent step-proof baseline scores 0.072.
- ProofFlowBench contains 184 undergraduate-level problems. Annotators labeled each one by hand, breaking its solution into individual steps and recording the graph of how those steps depend on one another.
- ProofScore jointly assesses syntactic correctness, semantic faithfulness and structural fidelity. Earlier work relied on compilation success or BLEU alone.
- In case studies, the ablation ProofFlow noDAG performed poorly. In this variant, each step sees all previous steps, and it produced fewer correct proofs and less faithful ones, sometimes proving intermediate lemmas that were never used.
- When a step fails, the pipeline traces the cause to formalization, tactic completion or the original NL statement. It surfaced real flaws in benchmark proofs, such as algebra errors, ambiguity and missing assumptions. The code, benchmark and metric are released on GitHub (Huawei-AI4Math/ProofFlow).

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng and Xin Shen. 2025. ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization. arXiv:2510.15981.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{cabral2025proofflow,
  title = {{ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization}},
  author = {Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng and Xin Shen},
  year = {2025},
  doi = {10.48550/arxiv.2510.15981},
  eprint = {2510.15981},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2510.15981}
}
```

- [← previous Premise Selection for a Lean Hammer](https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/)
- [next → Recitation over Reasoning: How Cutting-Edge Language Models Can Fail on Elementary School-Level Reasoning Problems?](https://md.research.elamur.ai/free/en/papers/yan-2025-recitation-over-reasoning-how-cutting/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/14/)

## References

40 references, 27 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. [Prover agent: An agent-based framework for formal mathematical proofs](https://md.research.elamur.ai/free/en/papers/baba-2025-prover-agent-agent-based-framework/). arXiv preprint arXiv:2506.19923, 2025.
2. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Héctor Herbelin, Gérard Mohring, Amokrane Saı̈bi, and Benjamin Werner. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report RT-0203, INRIA, 1997. [find](https://scholar.google.com/scholar?q=Bruno+Barras%2C+Samuel+Boutin%2C+Cristina+Cornes%2C+Judicae%CC%88l+Courant%2C+Jean%2DChristophe+Fillia%CC%82tre%2C+Eduardo+Gime%CC%81nez%2C+He%CC%81ctor+Herbelin%2C+Ge%CC%81rard+Mohring%2C+Amokrane+Sa%C4%B1%CC%88bi%2C+and+Benjamin+Werner%2E+The+Coq+Proof+As)
3. Kevin Buzzard and Richard Taylor. A Lean proof of Fermat’s Last Theorem. Technical report, Technical report, Imperial College of London, 2024. https . . . , 2025. [find](https://scholar.google.com/scholar?q=Kevin+Buzzard+and+Richard+Taylor%2E+A+Lean+proof+of+Fermat%E2%80%99s+Last+Theorem%2E+Technical+report%2C+Technical+report%2C+Imperial+College+of+London%2C+2024%2E+https+%2E+%2E+%2E+%2C+2025%2E)
4. Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://md.research.elamur.ai/free/en/papers/cao-2025-reviving-dsp-advanced-theorem-proving/). arXiv preprint arXiv:2506.11487, 2025.
5. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. [Seed-prover: Deep and broad reasoning for automated theorem proving](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-deep-broad-reasoning/). arXiv preprint arXiv:2507.23726, 2025.
6. Garett Cunningham, Razvan C Bunescu, and David Juedes. [Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs](https://md.research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/). arXiv preprint arXiv:2301.02195, 2023.
7. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. [Herald: A natural language annotated lean 4 dataset](https://md.research.elamur.ai/free/en/papers/gao-2024-herald-natural-language-annotated-lean/). arXiv preprint arXiv:2410.10878, 2024.
8. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al. A machine-checked proof of the Odd Order Theorem. Lecture Notes in Computer Science, 8332:163–179, 2013. [find](https://scholar.google.com/scholar?q=Georges+Gonthier%2C+Andrea+Asperti%2C+Jeremy+Avigad%2C+Yves+Bertot%2C+Cyril+Cohen%2C+Franc%CC%A7ois+Garillot%2C+Ste%CC%81phane+Le+Roux%2C+Assia+Mahboubi%2C+Russell+O%E2%80%99Connor%2C+Sidi+Ould+Biha%2C+et+al%2E+A+machine%2Dchecked+proof+of+th)
9. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. [A formal proof of the Kepler conjecture](https://md.research.elamur.ai/free/en/papers/hales-2015-formal-proof-kepler-conjecture/). Forum of Mathematics, Pi, 5, 2017.
10. Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, and Ivan Y. Tyukin. Stepproof: Step-by-step verification of natural language mathematical proofs, 2025. URL https://arxiv.org/abs/ 2506.10558. [↗](https://arxiv.org/abs/)
11. Yanxing Huang, Xinling Jin, Sijie Liang, Peng Li, and Yang Liu. Formarl: Enhancing autoformalization with no labeled data. arXiv preprint arXiv:2508.18914, 2025. [find](https://scholar.google.com/scholar?q=Yanxing+Huang%2C+Xinling+Jin%2C+Sijie+Liang%2C+Peng+Li%2C+and+Yang+Liu%2E+Formarl%3A+Enhancing+autoformalization+with+no+labeled+data%2E+arXiv+preprint+arXiv%3A2508%2E18914%2C+2025%2E)
12. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/), 2023. URL https://arxiv.org/abs/2210.12283. [↗](https://arxiv.org/abs/2210.12283)
13. Albert Q. Jiang, Wenda Li, Mateja Jamnik, Sean B. Holden, and Lawrence C. Paulson. [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In The Twelfth International Conference on Learning Representations (ICLR), 2024. URL [https://openreview.net/](https://openreview.net/) forum?id=Vp0Zz0w2V1. [↗](https://openreview.net/)
14. Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. Towards solving more challenging imo problems via decoupled reasoning and proving. arXiv preprint arXiv:2507.06804, 2025. — [arXiv:2507.06804](https://arxiv.org/abs/2507.06804) [find](https://scholar.google.com/scholar?q=Zhenwen+Liang%2C+Linfeng+Song%2C+Yang+Li%2C+Tao+Yang%2C+Feng+Zhang%2C+Haitao+Mi%2C+and+Dong+Yu%2E+Towards+solving+more+challenging+imo+problems+via+decoupled+reasoning+and+proving%2E+arXiv+preprint+arXiv%3A2507%2E06804%2C+)
15. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with sc… — [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-v2-scaling-formal/)
16. Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. [Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data](https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/). arXiv preprint arXiv:2502.05567, 2025.
17. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. [Process-driven autoformalization in lean 4](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/). arXiv preprint arXiv:2406.01940, 2024.
18. Math Inc. The strong prime number theorem. strongpnt, 2025. Accessed: 2025-09-11. [https://github.com/math-inc/](https://github.com/math-inc/) [↗](https://github.com/math-inc/)
19. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pp. 625–635. Springer, 2021. — [The Lean 4 Theorem Prover and Programming Language (System Description)](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
20. Nilay Patel, Rahul Saha, and Jeffrey Flanigan. [A new approach towards autoformalization](https://md.research.elamur.ai/free/en/papers/patel-2023-new-approach-towards-autoformalization/). arXiv preprint arXiv:2310.07957, 2023.
21. Shashank Pathak. [GFLean: An autoformalisation framework for lean via GF](https://md.research.elamur.ai/free/en/papers/pathak-2024-gflean-autoformalisation-framework-lean-gf/). arXiv preprint arXiv:2404.01234, 2024.
22. Lawrence C. Paulson. Isabelle: A generic theorem prover. In Alan Bundy (ed.), Proceedings of the 12th International Conference on Automated Deduction (CADE-12), volume 814 of Lecture Notes in Computer Science, pp. 37–41. Springer, 1994. [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson%2E+Isabelle%3A+A+generic+theorem+prover%2E+In+Alan+Bundy+%28ed%2E%29%2C+Proceedings+of+the+12th+International+Conference+on+Automated+Deduction+%28CADE%2D12%29%2C+volume+814+of+Lecture+Notes+in+Computer)
23. Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving autoformalization using type checking. arXiv preprint arXiv:2406.07222, 2024. [find](https://scholar.google.com/scholar?q=Auguste+Poiroux%2C+Gail+Weiss%2C+Viktor+Kunc%CC%8Cak%2C+and+Antoine+Bosselut%2E+Improving+autoformalization+using+type+checking%2E+arXiv+preprint+arXiv%3A2406%2E07222%2C+2024%2E)
24. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcemen… — [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)
25. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. [Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/). arXiv preprint arXiv:2504.21801, 2025b.
26. Marco Dos Santos, Haiming Wang, Hugues de Saxcé, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu, and Jia Li. Kimina Lean Server: Technical Report, 2025. [URL https://arxiv.org/abs/2504.21230](https://md.research.elamur.ai/free/en/papers/santos-2025-kimina-lean-server-high-performance/). [↗](https://arxiv.org/abs/2504.21230)
27. Peter Scholze. The Liquid Tensor Experiment. Xena Blog, 2021. Available at: [https://xenaproject.wordpress.com/2021/05/18/](https://xenaproject.wordpress.com/2021/05/18/) the-liquid-tensor-experiment/. [↗](https://xenaproject.wordpress.com/2021/05/18/)
28. Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hui Chen, Jie Yan, and Xiangyu Zhang. Stepfun-prover preview: Let’s think and verify step by step. arXiv preprint arXiv:2507.[20199, 2025](https://md.research.elamur.ai/free/en/papers/shang-2025-stepfun-prover-preview-let-s/).
29. Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. Solving inequality proofs with large language models. arXiv preprint arXiv:2506.07927, 2025. — [arXiv:2506.07927](https://arxiv.org/abs/2506.07927) [find](https://scholar.google.com/scholar?q=Jiayi+Sheng%2C+Luna+Lyu%2C+Jikai+Jin%2C+Tony+Xia%2C+Alex+Gu%2C+James+Zou%2C+and+Pan+Lu%2E+Solving+inequality+proofs+with+large+language+models%2E+arXiv+preprint+arXiv%3A2506%2E07927%2C+2025%2E+%E2%80%94+%5BarXiv%3A2506%2E07927%5D%28https%3A%2F%2Far)
30. Michio Sugeno. Theory of fuzzy integrals and its applications. Doctoral Thesis, Tokyo Institute of Technology, 1974. [find](https://scholar.google.com/scholar?q=Michio+Sugeno%2E+Theory+of+fuzzy+integrals+and+its+applications%2E+Doctoral+Thesis%2C+Tokyo+Institute+of+Technology%2C+1974%2E)
31. Terence Tao. Formalizing the proof of PFR in Lean4 using blueprint: a short tour. What’s new Blog, 2023. Available at: [https://terrytao.wordpress.com/2023/11/18/](https://terrytao.wordpress.com/2023/11/18/) formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/. [↗](https://terrytao.wordpress.com/2023/11/18/)
32. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, L… — [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/)
33. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. [Kimina-prover preview: Towards large formal reasoning models with reinforcement learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/). arXiv preprint arXiv:2504.11354, 2025b.
34. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. [Naturalproofs: Mathematical theorem proving in natural language](https://md.research.elamur.ai/free/en/papers/welleck-2021-naturalproofs-mathematical-theorem-proving-natural/), 2021. URL https://arxiv.org/abs/2104.01112. [↗](https://arxiv.org/abs/2104.01112)
35. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in neural information processing systems, 35:32353–32368, 2022.
36. Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, et al. [Stepfun-formalizer: Unlocking the autoformalization potential of llms through knowledge-reasoning fusion](https://md.research.elamur.ai/free/en/papers/wu-2025-stepfun-formalizer-unlocking-autoformalization/). arXiv preprint arXiv:2508.04440, 2025.
37. Xuejun Yu, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, et al. [Mathesis: Towards formal theorem proving from natural languages](https://md.research.elamur.ai/free/en/papers/xuejun-2025-mathesis-towards-formal-theorem-proving/). arXiv preprint arXiv:2506.07047, 2025a.
38. Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. [Formalmath: Benchmarking formal mathematical reasoning of large language models](https://md.research.elamur.ai/free/en/papers/yu-2025-formalmath-benchmarking-formal-mathematical-reasoning/). arXiv preprint arXiv:2505.02735, 2025b.
39. Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. Don’t trust: Verify – grounding llm quantitative reasoning with autoformalization, 2024. [URL https://arxiv.org/abs/2403.18120](https://md.research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/). [↗](https://arxiv.org/abs/2403.18120)
40. Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, et al. [Solving formal math problems by decomposition and iterative reflection](https://md.research.elamur.ai/free/en/papers/zhou-2025-solving-formal-math-problems-decomposition/). arXiv preprint arXiv:2507.15225, 2025.

*Updated 3 November 2026*