FormalScience: Human-in-the-Loop Autoformalisation for Scientific Proofs in Lean

Researchers have introduced FormalScience, a domain-agnostic human-in-the-loop agentic pipeline designed to autoformalise informal mathematical reasoning into formally verifiable code using the Lean4 theorem prover. The system targets scientific fields like physics, where domain-specific notation (e.g., Dirac notation, vector calculus) poses additional formalisation challenges that current LLMs and agentic approaches have not addressed. FormalScience enables a single domain expert without deep formal language experience to produce syntactically correct and semantically aligned formal proofs at low economic cost. Applied to physics, the pipeline generated FormalPhysics, a dataset of 200 university-level LaTeX physics problems and solutions—primarily in quantum mechanics and electromagnetism—along with their Lean4 formal representations. This work addresses the scalability of autoformalisation in scientific domains.