4 papers
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…
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…
Virtual localization revisited
Dhyan Aranha, Adeel A. Khan, Alexei Latyntsev +2
Let be a split torus acting on an algebraic scheme with fixed locus . Edidin and Graham showed that on localized -equivariant Chow groups, (a) push-forward alon…
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…