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.
The repository contains two branches:
main: including comments with the "solutions", as well as some explanationchecklist: stripped of comments, so that agents do not have access to them
The checklist branch is automatically generated by a CI workflow.
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:
- Only
Prop-valued sorries without metavariables (holes) - Please submit minimal working examples, so that each sorry represents a unique difficulty; ideally the 'proving' itself should be as easy as possible
- Please include a proof string in the comments (replacing "sorry" with this string should close the sorry)