1 citations · 2 across the 2 of their papers we have counts for
3 papers
cs.LO2026★ 1 cited
Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa, Jeremy Avigad
There are several paradigms for integrating interactive and automated theorem provers, combining the convenience of powerful automation with strong soundness guarantees. We introdu…
cs.LG2025
Premise Selection for a Lean Hammer
Thomas Zhu, Joshua Clune, Jeremy Avigad +2
Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a to…
cs.LO2025★ 1 cited
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Yicheng Qian, Joshua Clune, Clark Barrett +1
Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide…