About SorryDB
SorryDB aims to bridge the gap between automated formal proof research and day-to-day mathematical practice. It supplies Lean 4 users with the infrastructure needed to develop, test, and deploy AI proof agents against real theorems collected from public repositories.
Project Overview
At its core, SorryDB is a continuously refreshed dataset of Lean 4 sorry statements drawn from public projects. Each entry records the repository, commit, Lean version, and precise location of the unfinished proof so that anyone can reproduce the challenge locally. Template agents attempt to fill these proof obligations, while an independent verifier checks that proposed solutions are correct.
The long-term vision is to host an always-on sorry-filling competition with a public leaderboard. For
background on the motivation, philosophy, and roadmap, refer to ABOUT.md in the main
repository.