菜单
Use when multiple agents work in parallel, when PRs have merge conflicts from concurrent work, or when planning work that may overlap with other agents' in-flight PRs.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Use when deciding whether a formalized proof should delegate to Mathlib, when refactoring standalone proofs into Mathlib wrappers, or when reviewing delegation refactors for correctness.
Use when running Stage 3.4 (Proof Polishing) to bring sorry-free proofs to Mathlib quality. Use when assessing whether a proof needs cleanup, when working through proof-polish GitHub issues, or when deciding which tactic to prefer for a given goal.
Use when a Lean proof has failed 2-3 attempts and needs to be sent to Aristotle for automated proving, or when checking the status of a previously submitted Aristotle job.
Quantitative insights on formalization speed by item type and proof strategy. Use when estimating difficulty from textbook statements, planning batches, or predicting project timelines.
Use when filling sorry placeholders in Lean 4 proof files, when choosing between proof approaches for a FormalFrontier item, or when a proof attempt fails and you need an alternative strategy.
Use when searching for Mathlib declarations to fill a proof, when imports fail, when you need to find the right Mathlib module for a concept, or when exact? or apply? don't find what you need.
| name | parallel-agent-coordination |
| description | Use when multiple agents work in parallel, when PRs have merge conflicts from concurrent work, or when planning work that may overlap with other agents' in-flight PRs. |
| allowed-tools | Bash, Read, Grep, Glob |
Multiple pod agents run concurrently in separate worktrees. When two agents
modify the same files (especially progress/items.json, progress/ entries,
or dependencies/), their PRs will conflict. The first to merge wins; the
second gets merge conflicts.
These files are modified by many different tasks and are the most common source of merge conflicts between concurrent PRs:
| File | Why it conflicts | Mitigation |
|---|---|---|
progress/items.json | Multiple agents update item statuses | Use atomic field updates, not full rewrites |
progress/*.md | Timestamp collisions (rare) | Include session UUID prefix in filename |
dependencies/internal.json | Dependency graph changes | Coordinate via issue dependencies |
PROGRESS.md | Summary updates | Only summarize agents should touch this |
items.jsonprogress/<timestamp>_<UUID-prefix>.mdcoordination orient
Look at "Issues with open PRs" — if another agent has an open PR touching the same files you plan to modify, consider:
git fetch origin main
git rebase origin/main
This catches conflicts early. If conflicts exist, resolve them before creating the PR — a PR with conflicts will never auto-merge.
If coordination orient shows your PR has [CONFLICTS]:
git fetch origin maingit rebase origin/mainitems.json — then re-apply your specific changes on top)git push --force-with-leaseWhen creating issues, check what's already claimed or has open PRs. Don't create issues that would require modifying the same core files as in-flight work unless the issues have explicit dependencies.
The _<UUID-prefix> suffix on progress files was introduced specifically
to prevent merge conflicts. Always use it:
progress/2026-03-16T08-15-00Z_1d7941eb.md # good — unique per agent
progress/2026-03-16T08-15-00Z.md # bad — may collide
Early progress files without UUID suffixes predate this convention.