We publish because the technology depends on it. Axiomatic Intelligence has to verify and validate against real observations, so we study formal methods for physics and engineering, and how AI can take part in experiments directly. The papers below are where that work is tested against the field, with posts from the team alongside them.
Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund, Frank H.L. Koppens
Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring this standard of rigor to physics, where theoretical arguments carry idealizations that are rarely stated fully, and any logical gaps could have a cascading effect on interdependent results. Recognizing the need to evaluate autoformalization systems for physics, we release AxQM, 1,019 kernel-checkable proof-synthesis tasks over 479 items drawn from the textbook Quantum Computation and Quantum Information by Nielsen and Chuang. The tasks are stated in a custom Lean library of finite-dimensional quantum mechanics. By task count, it is the largest proof-synthesis benchmark in physics by a factor of four. AxQM is derived from a near-complete formalization of the formal portions of the textbook, so every task is guaranteed a solution, which we keep private. Grading of the benchmark is done deterministically by the Lean kernel, which checks that the proof compiles, that no sorry appears in it or in any declaration it depends on, and that it introduces no new axioms.
Marco Del Tredici
Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas, Lenny Taelman
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, more usable by mathematicians, and more capable of understanding complex dependencies. Moreover, by providing a continuously updated stream of tasks, SorryDB mitigates test-set contamination and offers a robust metric for an agent's ability to contribute to novel formal mathematics projects. We evaluate a collection of approaches, including generalist large language models, agentic approaches, and specialized symbolic provers, over a selected snapshot of 1000 tasks from SorryDB. We show that current approaches are complementary: even though an agentic approach based on Gemini Flash is the most performant, it is not strictly better than other off-the-shelf large-language models, specialized provers, or even a curated list of Lean tactics.
Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate this agentic approach using qualitatively different benchmarks and compare various frontier language models and design choices. Our results show competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture. Additionally, we demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.
Marco Del Tredici, Jacob McCarran, Benjamin Breen, Javier Aspuru Mijares, Weichen Winston Yin, Jacob M. Taylor, Frank Koppens, Dirk Englund
We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperform them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.
Ankita Sharma, YuQi Fu, Vahid Ansari, Rishabh Iyer, Fiona Kuang, Kashish Mistry, Raisa Islam Aishy, Sara Ahmad, Joaquin Matres, Dirk R. Englund, Joyce K.S. Poon
The paper presents "Photonics Intelligent Design and Optimization (PhIDO)", a multi-agent framework that converts natural-language photonic integrated circuit (PIC) design requests into layout mask files. The researchers compared 7 reasoning large language models using a testbench of 102 design descriptions, achieving up to 91% success rate for single-device designs and approximately 57% success rate for designs with up to 15 components.
Findings, methods, and commentary from our R&D teams, written to accompany the papers above and the products we build.
Our commitment to the scientists using Lemma: we will not front run your work. Axiomatic AI does not use your private work to race you to publication or patenting, or train capabilities for others without your permission.
Our new paper releases AxQM, a benchmark of 1,019 machine-checkable proof tasks drawn from a near-complete Lean formalization of Quantum Computation and Quantum Information by Nielsen and Chuang. Our system read the textbook and produced a verified proof for every labeled statement in it, showing that autonomous formalization can bring the rigor of formal mathematics to physics at textbook scale.
A digital twin of the Taillaert 2004 grating coupler, built end to end by our AI agent and held to the paper's own quantitative claims at a verification and validation gate.
How do AI provers handle the messy reality of open-source math? We worked on SorryDB, a community-maintained dynamic benchmark, to measure their performance on real-world Lean formalization projects. Recently presented at ICML.
Our ICML workshop paper introduces Skill-Synthesizer, a query-aware long-term memory system that enables AI agents to synthesize new skills from past experience instead of simply retrieving previous solutions, improving scientific reasoning on challenging physics benchmarks.
We study agentic code generation in Dafny. AxDafny turns code generation into a verifier-guided loop: the model writes Dafny code plus proof annotations, then repairs them using formal verification errors. This work shows large gains in verified correctness, but also a key limitation: proving functional correctness does not guarantee the generated code is efficient.
Our ICML paper introduces AxProverBase, a simple, reproducible, open-source agent that automates theorem proving in Lean — matching far more complex systems while using up to 100× fewer resources.