3 papers
cs.AI2026
Human agency in initial human-AI proof formalization workflows
Katherine M. Collins, Simon Frieder, Jonas Bayer +14
For centuries, human mathematicians have written proofs to substantiate their mathematical arguments; yet, the ability to automatically verify the validity of proofs has long been…
cs.LG2025
No LLM Solved Yu Tsumura's 554th Problem
Simon Frieder, William Hart
We show, contrary to the optimism about LLM's problem-solving abilities, fueled by the recent gold medals that were attained, that a problem exists -- Yu Tsumura's 554th problem --…
cs.GR2024
Newclid: A User-Friendly Replacement for AlphaGeometry
Vladmir Sicca, Tianxiang Xia, Mathïs Fédérico +3
We introduce a new symbolic solver for geometry, called Newclid, which is based on AlphaGeometry. Newclid contains a symbolic solver called DDARN (derived from DDAR-Newclid), which…