Elamur Research⌕
☰
home / papers / 2026 / FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

Paper · 2026 · Jordan Meadows, Lan Zhang and Andre Freitas

Summary

Turning informal scientific derivations into machine-checkable code is difficult. Physics adds notation such as Dirac brackets and vector calculus, which Lean's Mathlib barely supports. The authors introduce FormalScience, a domain-agnostic pipeline in which LLM agents generate statements, expand proofs, and repair Lean4 code using compiler feedback. A single domain expert acts as a binary judge of semantic alignment. Using GPT-5.1 and Claude-Opus-4.5, one physicist built FormalPhysics in about a month for roughly 50 USD. It contains 200 university-level problems, mostly quantum mechanics and electromagnetism, each with LaTeX solutions and Lean4 proofs. Every formal proof compiles, and the statements are more complex than those in standard math benchmarks. Fully automatic baselines lag far behind. The authors also classify how meaning drifts during formalisation. Their key conclusion is that compiling code is not enough: verified proofs may only cover simplified surrogates of the original physics. This makes the dataset a useful benchmark for scientific autoformalisation and alignment metrics.

Key points

  • FormalPhysics: 200 examples. Each has a natural-language statement, an informal proof, a formal statement and a formal proof. Formal validity is 100%. LLM-judged alignment is about 72–72.5%, which is lower than in math benchmarks.

  • Complexity: each statement mentions about 6.4 objects and 6.2 formulae on average. This is roughly twice the figures for miniF2F and ProofNet, and comparable to Herald-Proof.

  • Automatic baselines: the authors tested three approaches on statement autoformalisation:

    • zero-shot prompting;
    • self-refinement with error feedback;
    • a multi-stage ReAct-style agent.

    Open-source models up to 30B ran on a consumer GPU. The best system, a GPT-OSS-20B agent, compiled 31% of statements.

  • Drift taxonomy:

    • Notational collapse, found in most QM proofs, replaces physics objects with simple math surrogates.
    • Abstraction elevation reduces derivations to trivial or overly general algebra.
    • Implicit premise selection can actually enrich proofs.

  • Release and limitations: the code and an interactive UI are available at github.com/jmeadows17/formal-science. The main limitations are Mathlib's missing physics support, reliance on LLM judges, and the narrow subdomain coverage.

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

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksInformation Systems · 1,437 worksComputational Theory and Mathematics · 252 works

🧭 Topics 1Research subjects and languages the work is about.Code & programming languages · 129 works

Cite

Cite as Jordan Meadows, Lan Zhang and Andre Freitas. 2026. FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.acl-long.1057

@inproceedings{meadows2026formalscience,
  title = {{FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean}},
  author = {Jordan Meadows, Lan Zhang and Andre Freitas},
  booktitle = {Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2026},
  doi = {10.18653/v1/2026.acl-long.1057},
  url = {https://doi.org/10.18653/v1/2026.acl-long.1057}
}

References

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

  1. Yagub N Aliyev. 2024. Set theory and elementary algebra in lean 4 theorem prover. In 2024 IEEE 18th International Conference on Application of Information and Communication Technologies (AICT), pages 1–6. IEEE. find
  2. Anthropic. 2025a. Introducing claude opus 4.5. https://www.anthropic.com/news/claude-opus-4-5. Accessed: 2026-01-01. ↗
  3. Anthropic. 2025b. Introducing claude sonnet 4.5. https://www.anthropic.com/news/ claude-sonnet-4-5. Accessed: 2026-01-01. ↗
  4. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023a. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. Preprint, arXiv:2302.12433.
  5. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2023b. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631.
  6. Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, and Tyler R. Josephson. 2023. Formalizing chemical physics using the lean theorem prover. Preprint, arXiv:2210.12150. — [arXiv:2210.12150](https://arxiv.org/abs/2210.12150) find
  7. Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, and Vipin Chaudhary. 2025. Grammars of formal uncertainty: When to trust llms in automated reasoning tasks. arXiv preprint arXiv:2505.20047. find
  8. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. 2025. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations. find
  9. Binyuan Hui, Jian Yang, Zeyu Cui, Jiaxi Yang, Dayiheng Liu, Lei Zhang, Tianyu Liu, Jiajun Zhang, Bowen Yu, Keming Lu, Kai Dang, Yang Fan, Yichang Zhang, An Yang, Rui Men, Fei Huang, Bo Zheng, Yibo Miao, Shanghaoran Quan, and 5 others. 2024. Qwen2.5-coder technical report. Preprint, arXiv:2409.12186.
  10. Mihnea Iancu and Florian Rabe. 2011. Formalising foundations of mathematics. Mathematical Structures in Computer Science, 21(4):883–911. find
  11. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. 2024. Multi-language diversity benefits autoformalization. In Advances in Neural Information Processing Systems, volume 37, pages 83600–83626. Curran Associates, Inc. find
  12. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations.
  13. Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan-Afshar, Cvetan Dunchev, and Sofiene Tahar. 2015. Formalizing physics: automation, presentation and foundation issues. In International Conference on Intelligent Computer Mathematics, pages 288– 295. Springer. find
  14. Sirui Li, Wangyue Lu, Xiaorui Shi, Ke Weng, Haozhe Sun, Minghe Yu, Tiancheng Zhang, Ge Yu, Hengyu Liu, and Lun Du. 2025. Msc-180: A benchmark for automated formal theorem proving from mathematical subject classification. arXiv preprint arXiv:2512.18256. — [arXiv:2512.18256](https://arxiv.org/abs/2512.18256) find
  15. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. 2024. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems. find
  16. Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. 2025a. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations. find
  17. Qi Liu, Xinhao Zheng, Renqiu Xia, Qinxiang Cao, and Junchi Yan. 2025b. Bootstrapping hierarchical autoregressive formal reasoner with chain-of-proxy-autoformalization. In The Thirty-ninth Annual Conference on Neural Information Processing Systems. find
  18. Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. 2025c. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. Preprint, arXiv:2502.05567.
  19. Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune, and David Ha. 2024a. The ai scientist: Towards fully automated open-ended scientific discovery. arXiv preprint arXiv:2408.06292.
  20. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. 2024b. Process-driven autoformalization in lean 4. Preprint, arXiv:2406.01940. find
  21. John McCarthy. 2022. Artificial intelligence, logic, and formalising common sense. Machine Learning and the City: Applications in Architecture and Urban Design, pages 69–90. find
  22. Jordan Meadows and André Freitas. 2021. Similarity-based equational inference in physics. Physical Review Research, 3(4):L042010. find
  23. Jordan Meadows, Tamsin Emily James, and Andre Freitas. 2024. Exploring the limits of fine-grained LLM-based physics inference via premise removal interventions. In Findings of the Association for Computational Linguistics: EMNLP 2024, pages 6487–6502, Miami, Florida, USA. Association for Computation… find
  24. Jordan Meadows, Marco Valentino, and André Freitas. 2025. Controlling equational reasoning in large language models with prompt interventions. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 39, pages 24858–24866. find
  25. Agnieszka Mensfelt, David Tena Cucala, Santiago Franco, Angeliki Koutsoukou-Argyraki, Vince Trenc-senyi, and Kostas Stathis. 2025. Towards a common framework for autoformalization. Preprint, arXiv:2509.09810. — [arXiv:2509.09810](https://arxiv.org/abs/2509.09810) find
  26. Andreas Opedal, Haruki Shirakami, Bernhard Schölkopf, Abulhair Saparov, and Mrinmaya Sachan. 2024. Mathgap: Out-of-distribution evaluation on problems with arbitrarily complex proofs. arXiv preprint arXiv:2410.13502. — [arXiv:2410.13502](https://arxiv.org/abs/2410.13502) find
  27. OpenAI, :, Sandhini Agarwal, Lama Ahmad, Jason Ai, Sam Altman, Andy Applebaum, Edwin Arbus, Rahul K. Arora, Yu Bai, Bowen Baker, Haiming Bao, Boaz Barak, Ally Bennett, Tyler Bertao, Nivedita Brett, Eugene Brevdo, Greg Brockman, Sebastien Bubeck, and 108 others. 2025. gpt-oss-120b & gpt-oss-20b model…
  28. OpenAI. 2025. Gpt-5.1: A smarter, more conversational chatgpt. Large language model. find
  29. Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. 2025. Reliable evaluation and benchmarks for statement autoformalization. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 17958–17980, Suzhou, China. Association for Computational Ling… find
  30. Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. 2024a. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), p… find
  31. Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2024b. Verification and refinement of natural language explanations through LLM-symbolic theorem proving. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 2933–2958, Miami, Florida, USA. A…
  32. 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. 2025. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinfo…
  33. Alessandro Stolfo, Zhijing Jin, Kumar Shridhar, Bernhard Schölkopf, and Mrinmaya Sachan. 2022. A causal framework to quantify the robustness of mathematical reasoning with language models. arXiv preprint arXiv:2210.12023.
  34. Guillem Tarrach, Albert Q. Jiang, Daniel Raggi, Wenda Li, and Mateja Jamnik. 2024. More details, please: Improving autoformalization with more detailed proofs. In AI for Math Workshop @ ICML 2024. find
  35. TeichAI / Liontix. 2025. TeichAI/Qwen3-14B-Claude-Sonnet-4.5-Reasoning-Distill-GGUF. Model page on Hugging Face. Accessed: 2026-01-01. find
  36. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. 2024. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datase… find
  37. 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, and 21 others. 2025a. find
  38. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. Preprint, arXiv:2504.11354. find
  39. Shaoqi Wang, Lu Yu, Siwei Lou, Feng Yan, Chunjie Yang, Qing Cui, and Jun Zhou. 2025b. Improving autoformalization using direct dependency retrieval. Preprint, arXiv:2511.11990. find
  40. Xingyao Wang, Yangyi Chen, Lifan Yuan, Yizhe Zhang, Yunzhu Li, Hao Peng, and Heng Ji. 2024. Executable code actions elicit better llm agents. In Forty-first International Conference on Machine Learning.
  41. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. In Advances in Neural Information Processing Systems.
  42. Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, and Wenda Li. 2025. Ape-bench i: Towards file-level automated proof engineering of formal math libraries. Preprint, arXiv:2504.19110. find
  43. Yutaro Yamada, Robert Tjarko Lange, Cong Lu, Shengran Hu, Chris Lu, Jakob Foerster, Jeff Clune, and David Ha. 2025. The ai scientist-v2: Workshop-level automated scientific discovery via agentic tree search. arXiv preprint arXiv:2504.08066.
  44. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, and 41 others. 2025a. Qwen3 technical report. Preprint, arXiv:2505.09388.
  45. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri, and Dawn Song. 2025b. Position: Formal mathematical reasoning—a new frontier in AI. In Forty-second International Conference on Machine Learning Position Paper Track. find
  46. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023a. Leandojo: Theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems, volume 36, pages 21573–21612. Curran As…
  47. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023b. Leandojo: Theorem proving with retrieval-augmented language models. Preprint, arXiv:2306.15626.
  48. Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik R Narasimhan, and Yuan Cao. 2022. React: Synergizing reasoning and acting in language models. In The eleventh international conference on learning representations.
  49. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean workbook: A large-scale lean problem set formalized from natural language math problems. In Advances in Neural Information Processing Systems, volume 37, pages 105848–105863. Curran Associates, Inc. find
  50. Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. 2025. Formalmath: Benchmarking formal mathematical reasoning of large language models. Preprint, arXiv:2505.02735. find
  51. Lan Zhang, Xin Quan, and Andre Freitas. 2024. Consistent autoformalization for constructing mathematical libraries. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020–4033, Miami, Florida, USA. Association for Computational Linguistics. find
  52. Lan Zhang, Marco Valentino, and Andre Freitas. 2025a. Autoformalization in the wild: Assessing LLMs on real-world mathematical definitions. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 1720–1738, Suzhou, China. Association for Computational Linguis… find
  53. Lan Zhang, Marco Valentino, and Andre Freitas. 2025b. Beyond gold standards: Epistemic ensemble of llm judges for formal mathematical reasoning. Preprint, arXiv:2506.10903.
  54. Lan Zhang, Marco Valentino, and Andre Freitas. 2025c. MASA: LLM-driven multi-agent systems for autoformalization. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pages 615–624, Suzhou, China. Association for Computational Linguistics.
  55. Meiru Zhang, Philipp Borchert, Milan Gritta, and Gerasimos Lampouras. 2025d. Drift: Decompose, retrieve, illustrate, then formalize theorems. Preprint, arXiv:2510.10815. — [arXiv:2510.10815](https://arxiv.org/abs/2510.10815) find
  56. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/meadows-2026-formalscience-scalable-human-loop-autoformalisation/