| name | sorry-checker |
| description | Check that no sorry placeholders exist in the codebase. Use after making changes or when asked to verify proof completeness. |
Verify No Sorry
This skill checks that the codebase contains no sorry placeholders, which is a critical requirement for this project.
Quick Check
Run this command to find any sorries:
grep -r "sorry" Metatheory/ --include="*.lean"
Expected output: No matches (empty output).
Full Verification
Build the project to verify all proofs compile:
lake build
A successful build with no warnings about sorry confirms the codebase is complete.
What to Do If Sorries Are Found
Option 1: Complete the Proof Manually
Look at similar proofs nearby and mirror their style.
Option 2: Use Aristotle
For difficult proofs, use the aristotle skill to get automated proof suggestions.
Option 3: Extract Helper Lemmas
If a proof is stuck, break it into smaller pieces:
-- Instead of one complex proof
theorem big_theorem : ... := by
sorry
-- Extract helpers
lemma helper1 : ... := by
...
lemma helper2 : ... := by
...
theorem big_theorem : ... := by
apply helper1
apply helper2
Project Policy
sorry is NEVER acceptable in commits to this codebase.
All theorems must be fully proven before merging.
