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.AG2024
The stacky concentration theorem
Dhyan Aranha, Adeel A. Khan, Alexei Latyntsev +2
We give a sufficient criterion for the Chow or algebraic bordism groups of an algebraic stack, localized at a set of Chern classes of line bundles, to be concentrated in some close…
math.AG2023
The chow weight structure for geometric motives of quotient stacks
Dhyan Aranha, Chirantan Chowdhury
We construct the Chow weight structure on the derived category of geometric motives with arbitrary coefficients for X a finite type scheme over a field characteristic 0 and G an af…