Research

Papers

• September 4, 2026 · arXiv preprint

  AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics

  Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund, Frank H.L. Koppens

  ▸ Abstract

  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.

  Read the paper ↗ Blog post →

  • Benchmark
  • Theorem proving
  • Quantum physics
  • Lean
• July 13, 2026 · ICML 2026 Workshop

  Skill-Synthesizer: Query-Aware Skill Synthesis for Scientific Reasoning

  Marco Del Tredici

  Read the paper ↗ Blog post →

  • Agent memory
  • Scientific reasoning
• July 6, 2026 · ICML 2026 AI4Math Workshop

  AxDafny: Agentic Verified Code Generation in Dafny

  Benjamin Breen

  Read the paper ↗ Blog post →

  • Verified code generation
  • Dafny
• March 3, 2026 · ICML 2026

  SorryDB: Can AI Provers Complete Real-World Lean Theorems?

  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

  ▸ Abstract

  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.

  Read the paper ↗ Blog post →

  • Theorem proving
  • Benchmark
  • Lean
• February 27, 2026 · ICML 2026

  A Minimal Agent for Automated Theorem Proving

  Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra

  ▸ Abstract

  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.

  Read the paper ↗ Blog post →

  • Theorem proving
  • Agents
  • Lean
• October 14, 2025 · arXiv preprint

  Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

  Marco Del Tredici, Jacob McCarran, Benjamin Breen, Javier Aspuru Mijares, Weichen Winston Yin, Jacob M. Taylor, Frank Koppens, Dirk Englund

  ▸ Abstract

  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.

  Read the paper ↗

  • Theorem proving
  • Agents
  • Quantum physics
• August 18, 2025 · arXiv preprint

  AI Agents for Photonic Integrated Circuit Design Automation

  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

  ▸ Abstract

  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.

  Read the paper ↗

  • Photonics
  • Design automation
  • Agents

Blog

Findings, methods, and commentary from our R&D teams, written to accompany the papers above and the products we build.