Videos

The SorryDB project

Presenter
April 25, 2025
Abstract
This talk reports on work-in-progress to build a continuously updating database of uncompleted ('sorry') proofs in public repositories. The aim is for this to form the basis for a continuous competition between automated provers. We intend to provide all tools necessary to make it as easy as possible to add new provers, and to make it as easy as possible for successful provers to be adopted in the real world.
Supplementary Materials