1 citations · 1 across the 2 of their papers we have counts for
3 papers · 1 filter
Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
Leni Aniva, Iori Oikawa, David Dill +1
In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a statement in a proof assistant. In this work, we in…
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…
Lean-SMT: An SMT tactic for discharging proof goals in Lean
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan +5
Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof ass…