Skip to content

README.md

Latest commit

 

History

History
38 lines (21 loc) · 1.25 KB

README.md

File metadata and controls

38 lines (21 loc) · 1.25 KB

SorryDB Agent development checklist

This is an artificial lean 4 project containing a number of sorried statements. It intends to help with the development of SorryDB agents.

The sorries in this project are easy from the point of view of automated theorem proving, but represent individual engineering issues that may occur when attempting to automatically fill sorries 'in the wild'.

See Checklist.lean for the list of sorries.

Branches

The repository contains two branches:

  • main: including comments with the "solutions", as well as some explanation
  • checklist: stripped of comments, so that agents do not have access to them

The checklist branch is automatically generated by a CI workflow.

Contributing

Contributions are welcome. If you encounter (recurring) engineering issues that in using automation to fill Lean sorries in real-world projects, feel free to make a PR.

Requirements:

  1. Only Prop-valued sorries without metavariables (holes)
  2. Please submit minimal working examples, so that each sorry represents a unique difficulty; ideally the 'proving' itself should be as easy as possible
  3. Please include a proof string in the comments (replacing "sorry" with this string should close the sorry)