We were pleased to participate as one of the five teams worldwide in First Proof Batch 3, with Jinzheng Li, Yidi Qi, Zeru Zhu and Matthew Kung.

This batch tested AI systems on ten research-level math problems. These problems had already been solved by human mathematicians, but their solutions had not yet been made public.

Using the MerLean harness, we solved four of the problems and gave partial results for five more. We congratulate the ETH Zurich-led ProofCouncil team for solving the most problems: nine out of ten.

Open full-size image ↗

There are several lessons from this evaluation that we hope will be useful to others working on AI4Math.

• Performance per dollar. A frontier model with maximum reasoning effort (max) gave the best result here: GPT-6 Astra solved seven out of ten problems for just $36 in total, on the order of 1/50 of the cost of the next cheapest team using a harness. Counterintuitively, the “expensive” model was the cheapest. It remains unclear how well this carries over to easier math tasks.

• The benefits and costs of a harness. A harness can help with some problems, but it can also significantly increase costs. MerLean cost more than twice as much as any other harness team and was the only one using formal reasoning and formal verification. Our takeaway is that, for academic researchers with limited time and token budgets, formal methods are not yet worth the additional cost for solving open math problems with today’s best models—unless absolute rigor is the priority and there is the patience to let AI work on a problem for days or weeks.

• The base model is key. Related to the first point, a harness cannot necessarily make up for a gap in the base model’s capabilities. Humanize was the only team to use an open-weight model, Kimi K3, and none of its solutions met the correctness threshold.

We thank the First Proof organizers for selecting and supporting us as the only student team participating in the Batch 3 AI4Math evaluation, including during our harness preparation.

More details are available on the official First Proof Batch 3 page, in the full benchmark report, and in the official results announcement.

How do you debug a quantum program when you cannot simply copy an unknown quantum state, and measuring it can change it?

In classical programming, we often inspect intermediate values or save a copy of the state to understand what went wrong. Quantum mechanics makes those familiar habits harder to carry over. Testing is still useful, but it becomes harder to establish exactly what a program guarantees.

This is one motivation behind our new paper, QEDIA: Quantum Program Verification in Lean.

The idea is to prove that a quantum program meets a precise specification. We formalize quantum Hoare logic QHL+ in Lean 4, connecting the underlying quantum mathematics to program semantics and proof rules. We also prove that those rules are sound.

A central challenge is that practical quantum programs mix classical and quantum computation. Classical variables select qubits, determine gate parameters and control loops. Measurement outcomes then influence what happens next. The specifications and proofs need to capture both directions.

Open full-size image ↗

We demonstrate this through eleven verified programs, including the quantum Fourier transform, phase estimation, repeat-until-success circuits and Hamiltonian simulation, with guarantees covering termination, success probabilities and approximation error.

There is an AI side to this work, too. LLM agents built the library and proofs under human supervision, with every proof checked by Lean’s kernel. Making sure the specifications capture the intended guarantees remains an important part of the human review.

We are pleased to share this work with coauthors Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi and Mingsheng Ying.

Read QEDIA: Quantum Program Verification in Lean on arXiv.

We welcome conversations with others working on quantum software, formal verification or AI-assisted theorem proving.