SorryDB: Can AI Provers Complete Real-World Lean Theorems?
A dynamically-updating benchmark of open Lean tasks drawn from real-world formalization projects, designed to measure how well AI provers can contribute to novel formal mathematics.
ICML · arXiv · Code · Leaderboard
A Minimal Agent for Automated Theorem Proving
A minimal agentic framework for automated theorem proving in Lean 4, built around a propose–compile–review loop with memory of failed attempts.
ICML · arXiv · Code · Try now