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

• URL: http://arxiv.org/abs/2604.23002v1
• Date: Fri, 24 Apr 2026 20:47:22 GMT
• Title: FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
• Abstract summary: FormalScience is a human-in-the-loop agentic pipeline to produce textitsyntactically correct and textitsemantically aligned formal proofs of informal reasoning for low economic cost.<n>We construct FormalPhysics, a dataset of 200 physics problems and solutions (primarily quantum mechanics and electromagnetism) along with their Lean4 formal representations.<n>We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach.
• Score: 7.11696910077237
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. In scientific fields such as physics, domain-specific machinery (\textit{e.g.} Dirac notation, vector calculus) imposes additional formalisation challenges that modern LLMs and agentic approaches have yet to tackle. To aid autoformalisation in scientific domains, we present FormalScience; a domain-agnostic human-in-the-loop agentic pipeline that enables a single domain expert (without deep formal language experience) to produce \textit{syntactically correct} and \textit{semantically aligned} formal proofs of informal reasoning for low economic cost. Applying FormalScience to physics, we construct FormalPhysics, a dataset of 200 university-level (LaTeX) physics problems and solutions (primarily quantum mechanics and electromagnetism), along with their Lean4 formal representations. Compared to existing formal math benchmarks, FormalPhysics achieves perfect formal validity and exhibits greater statement complexity. We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach, and explore autoformalisation limitations in modern LLM-based approaches. We provide the first systematic characterisation of semantic drift in physics autoformalisation in terms of concepts such as notational collapse and abstraction elevation which reveals what formal language verifies when full semantic preservation is unattainable. We release the codebase together with an interactive UI-based FormalScience system which facilitates autoformalisation and theorem proving in scientific domains beyond physics.https://github.com/jmeadows17/formal-science

Related papers

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• Multi-agent Autoformalization of Tensor Network Theory [0.21847754147782886]
  We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics.<n>The agents coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously.<n>For some statements, the agents were able to explore new proof routes that are not part of the standard literature.
  arXiv  Detail & Related papers  (2026-07-08T18:43:33Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• MMFormalizer: Multimodal Autoformalization in the Wild [79.24853896733154]
  MMFormalizer extends autoformalization beyond text by integrating adaptive grounding with entities from real-world mathematical and physical domains.<n>We evaluate MMFormalizer on a new benchmark, PhyX-AF, comprising 115 curated samples from MathVerse, PhyX, Synthetic Geometry, and Analytic Geometry.<n>Results show GPT-5 and Gemini-3-Pro achieve the highest compile and semantic accuracy, with GPT-5 excelling in physical reasoning.
  arXiv  Detail & Related papers  (2026-01-06T13:42:51Z)
• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMF is a Concept-driven Retrieval-Augmented Mathematical Formalization framework.<n>We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4.<n>Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers.
  arXiv  Detail & Related papers  (2025-08-09T10:54:25Z)
• StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion [30.51794514312176]
  We identify two key abilities for effective autoformalization.<n>We introduce ThinkingF, a data synthesis and training pipeline that improves both abilities.<n>The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning.
  arXiv  Detail & Related papers  (2025-08-06T13:28:22Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Can Theoretical Physics Research Benefit from Language Agents? [50.57057488167844]
  Large Language Models (LLMs) are rapidly advancing across diverse domains, yet their application in theoretical physics research is not yet mature.<n>This position paper argues that LLM agents can potentially help accelerate theoretical, computational, and applied physics when properly integrated with domain knowledge and toolbox.<n>We envision future physics-specialized LLMs that could handle multimodal data, propose testable hypotheses, and design experiments.
  arXiv  Detail & Related papers  (2025-06-06T16:20:06Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• SciInstruct: a Self-Reflective Instruction Annotated Dataset for Training Scientific Language Models [57.96527452844273]
  We introduce SciInstruct, a suite of scientific instructions for training scientific language models capable of college-level scientific reasoning. We curated a diverse and high-quality dataset encompassing physics, chemistry, math, and formal proofs. To verify the effectiveness of SciInstruct, we fine-tuned different language models with SciInstruct, i.e., ChatGLM3 (6B and 32B), Llama3-8B-Instruct, and Mistral-7B: MetaMath.
  arXiv  Detail & Related papers  (2024-01-15T20:22:21Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  Autoformalization is the task of translating natural language mathematics into a formal language that can be verified by a program. Research paper mathematics requires large amounts of background and context. We propose an avenue towards tackling autoformalization for research-level mathematics, by breaking the task into easier and more approachable subtasks.
  arXiv  Detail & Related papers  (2023-10-12T00:50:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.