collaborators

1 paper

cs.LO2026

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…