3 papers
cs.LO2026
Ablation and the Meno: Tools for Empirical Metamathematics
Zhengqin Fan, Simon DeDeo
We present the results from Meno, a simple autoformalizer that proves theorems in Lean by systematically exploring the space of both formal and informal proofs, and tactic ablation…
math.HO2026
A correspondence problem for mathematical proof
Simon DeDeo, Eamon Duede
Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an un…
cs.AI2025
Explaining Necessary Truths
Gülce KardeÅ, Simon DeDeo
Knowing the truth is rarely enough -- we also seek out reasons why the fact is true. While much is known about how we explain contingent truths, we understand less about how we exp…