1 citations · 1 across the 5 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
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…