Neurosymbolic Agentic AI for Automated Theorem Proving

ABSTRACT

Automated theorem proving requires a blend of creative intuition and rigorous logical deduction, a combination that eludes pure deep learning models. We propose a Neurosymbolic Agentic AI framework that marries the creative search capabilities of Large Language Models with the deterministic verification of formal proof assistants (e.g., Lean 4). Our system deploys an 'Intuition Agent' to propose proof steps and a 'Verifier Agent' to interface with the Lean environment. By treating mathematical reasoning as a multi-agent reinforcement learning environment, our system achieves a state-of-the-art pass rate on the miniF2F benchmark.