MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +1

LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (I…