← Search

Austin Letson

2 accepted papers

2026

A Minimal Agent for Automated Theorem Proving

ICML 2026poster

We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate our baseline…

Cited by 0SourceScholar
2026

SorryDB: Can AI Provers Complete Real-World Lean Theorems?

ICML 2026poster

We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, m…

Cited by 0SourceScholar