sorrydb 0.1.0

Build a continously updating database of sorry statments in public Lean4 repositories

Lean4 SorryDB

The SorryDB project aims to help bridge the gap between automated (formal) theorem proving "in the lab" and adoption by mathematicians. It provides tools and infrastructure to facilitate developing, testing, and ultimately using AI proof agents against "real world" mathematical propositions in Lean.

At its core, it provides a continuously updating dataset of sorry statements in public Lean 4 repositories. It also provides template agents that attempt to prove such statements, and a verifier that checks the correctness of proposed proofs.

Eventually, we hope to host a continuously running sorry-filling competition, with a public leaderboard. For a detailed explanation of the project's motivation, philosophy, and long-term goals, see ABOUT.md.

Components

The nightly SorryDB dataset

The main instance of a SorryDB database is hosted at sorrydb-data. It is updated nightly, by crawling Lean 4 repositories listed on Reservoir for sorried (Prop-valued) statements.

For each such statement, it contains all information needed to locally reproduce it. This includes repository information (remote url, branch, commit hash), the Lean 4 version used, and coordinates of the sorry within the repository (path, line, column).

See DATABASE.md for more detailed information on the database format.

The sorry crawler

The dataset is updated nightly using a crawler which uses git and lake build to clone and build the repository locally, and then uses the Lean REPL to locate and analyze sorries in the repository.

The sorry-proving agents

We treat each entry of the database as a theorem-proving challenge, where the precise task is to replace the "sorry" string with a string of tactics that fills the proof. The input to an agent is an item of the dataset, and the agent is asked to clone and build the repository, and attempt to find a proof of the given sorry.

We provide two sample agents:

1. rfl_agent which checks if the tactic rfl completes the sorried proof
2. llm_agent which polls an LLM to make a one-shot attempt at filling the proof.

These are deliberately primitive (and hence weak), and not meant for consumption. Rather, we hope they are helpful as templates on which one can base stronger sorry-proving agents.

See AGENTS.md for the specification of input and output of an agent, and more information on the sample agents.

Getting started

SorryDB uses Poetry for dependency management and packaging. To get started

1. Install Poetry if you haven't already

2. Clone the repository and install dependencies:

   git clone https://github.com/SorryDB/SorryDB.git
   cd SorryDB
   poetry install
   

3. Activate the virtual environment:

   eval $(poetry env activate)
   

The command line scripts in sorrydb/cli can now be run from poetry's virtual environment by running:

poetry run <script name> <options>.

See the documents in doc/ for more information on the various scripts provided.

Setting up your own database

We provide various tools to create and manage your own database. See DATABASE-SCRIPTS.md for instructions in setting up your own database (e.g. to scrape your own repository).

Contributing

See CONTRIBUTING.md for contribution guidelines.