Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

Published in ACL 2026, 2026

DAP separates answer discovery from formal proof construction to enable harder and more realistic automated theorem proving.