Papers with FormalPhysics
FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean (2026.acl-long)
Copied to clipboard
| Challenge: | Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. |
| Approach: | They propose a domain-agnostic human-in-the-loop agentic pipeline to aid autoformalisation in scientific domains. |
| Outcome: | The proposed system produces syntactically correct and semantically aligned proofs for low cost. |