3 papers
cs.AI2026
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Austin Letson, Leopoldo Sarra, Auguste Poiroux +9
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…
math.HO2026
Shaping the Future of Mathematics in the Age of AI
Johan Commelin, Mateja Jamnik, Rodrigo Ochigame +2
Artificial intelligence is transforming mathematics at a speed and scale that demand active engagement from the mathematical community. We examine five areas where this transformat…
math.AG2025
Deformations and Lifts of Calabi-Yau Varieties in Characteristic
Lukas Brantner, Lenny Taelman
We study deformations of Calabi-Yau varieties in characteristic using techniques from derived algebraic geometry. We prove a mixed characteristic analogue of the Bogomolov-Tian…