Olympiad-level formal mathematical reasoning with reinforcement learning, Nature.
SorryDB: Can AI Provers Complete Real-World Lean Theorems?. ICML 2026 + ICLR 2026 VerifAI-2 Workshop.
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics, Preprint.
Non-Archimedean Polydisc Spaces and Applications to Optimisation. In collaboration with Anthea Monod, Yiannis Fam and Yue Ren. Preprint.
Tropical Expressivity of Neural Networks. In collaboration with Thomas Walker, Shiv Bhatia, Yueqi Cao and Anthea Monod. Preprint.
formal-conjectures. GitHub repository
AlphaProof. Blog post.
A Geometric Perspective on Adversarial Robustness in Deep Learning. In collaboration with Martin Lotz. Publication currently in preparation.
Stacks in Lean (joint with Calle Sönne)
GitHub repository
The Polynomial Freiman-Ruzsa Conjecture (formal mathematics project led by Terrence Tao, see the repository for a full list of participants).
GitHub repository Article about the PFR proof
The Kummer-Dedekind theorem in Lean, under the supervision of Damiano Testa.
Code now in mathlib4