| name | unsorry-proof-authoring |
| description | Workflow for adding, repairing, or reviewing Unsorry Lean proofs. Use when working with goals/*.lean, goals/*.aisp, library/Unsorry/*.lean, library/index/*.aisp, proof-runs, content-addressed statements, mathlib imports, or any task that proves, decomposes, or preserves an Unsorry theorem. |
Unsorry Proof Authoring
Purpose
Use this skill to move from an Unsorry goal to a kernel-checked proof while preserving the queue metadata that makes the swarm safe. The Lean kernel is the proof authority; AISP records explain the queue state and provenance.
Access Pattern
Start at the goal, then follow the artifacts outward:
- Read
goals/<id>.aisp for phase, status, difficulty, source path, dependencies, artifact path, and current SHA.
- Read
goals/<id>.lean for the exact statement. Existing goal statements are create-only; do not edit them to make a proof easier.
- Search
library/Unsorry/ and library/index/ for reusable proved lemmas before inventing new support lemmas.
- If the goal is proved, put the reusable theorem in
library/Unsorry/*.lean, update the matching index record under library/index/, and keep the goal metadata consistent.
- If the goal cannot be proved within budget, prefer a decomposition record or affinity/difficulty update over weakening the statement.
Useful discovery commands:
rg -n "<goal-id>|<theorem_name>|<source phrase>" goals library library/index backlog docs
find library/Unsorry -maxdepth 1 -name '*.lean' | sort
find library/index -maxdepth 1 -name '*.aisp' | sort
For deeper orientation, read references/repo-map.md. For exact artifact relationships and mutation rules, read references/proof-artifacts.md.
Lean Proof Rules
- Keep
library/ at the zero-sorry bar. Do not add sorry, admit, new axioms, unsafe, native_decide, implemented_by, extern, or local options that relax elaboration.
- Keep
autoImplicit = false behavior intact. If a theorem needs binders, write them explicitly.
- Prefer mathlib lemmas and existing
Unsorry lemmas over custom proof machinery.
- Keep imports narrow and ordinary. Import
Mathlib... or existing Unsorry... modules as needed; do not create hidden trust paths.
- Do not treat a passing Gate B result as proof correctness. Gate B only validates coordination records.
Metadata Rules
goals/*.aisp is the work queue. For prove-phase goals, lean should point to the Lean goal file and status should match reality.library/index/<sha>.aisp is the content-addressed proof index. Use nearby records as the schema pattern and run Gate B after editing.proof-runs/*.aisp records terminal coordinated runs for analytics. It is not proof admission and should not be fabricated for local-only experiments.claims/ on main must contain only README.md; live claim files belong on the claims branch.- Source and absence evidence live in
backlog/, docs/targets.md, and sourcing metadata. Preserve source paths rather than replacing them with prose.
Validation
Choose the lightest checks that cover the touched surface, then expand if the change is proof-bearing:
lake build UnsorryLibrary --wfail
lake build UnsorryGoals
python3 -m tools.gate_b validate .
python3 -m tools.sourcing.targets_board --check .
python3 -m tools.leaderboard --check .
For full local confidence before a proof PR, also run:
python3 -m tools.gate_a.check_statement_binding generate .
python3 -m tools.gate_a.check_library_options library
python3 -m tools.gate_a.parallel_modules audit --jobs 1 --output axiom-report.json
Use lake exe cache get if dependencies are missing. Do not build mathlib from source unless the repository policy changes.
For command selection and failure interpretation, read references/proof-validation.md.
Pack Resources
Load these only when the task needs the extra detail:
Reusable templates live in assets/:
