Showing 2026Show all
3 papers · 1 filter
math.MG2026
Progress in Formalizing Sphere Packing in Dimension 8
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee +4
In 2016, Viazovska famously solved the sphere packing problem in dimension , using modular forms to construct a 'magic' function satisfying optimality conditions determined by C…
cs.AI2026
Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
Kyuhee Kim, Auguste Poiroux, Antoine Bosselut
Formal verification guarantees proof validity but not formalization faithfulness. For natural-language logical reasoning, where models construct axiom systems from scratch without…
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…