check-referenced-state…
Validate externally referenced theorems by querying arXiv theorem search first and Codex's…
Synthesize the common stuck points across failed decomposition plans. Use when the current batch of decomposition plans has failed — whether they failed already at direct proving or only after further attempts.
$ npx -y skills add frenzymath/Danus --skill identify-key-failures --agent claude-codeHow it fires
How this skill gets triggered: by you, by Claude, or both.
/identify-key-failuresContext preview
The summary Claude sees to decide when to auto-load this skill.
Synthesize the common stuck points across failed decomposition plans. Use when the current batch of decomposition plans has failed — whether they failed already at direct proving or only after further attempts.
name: identify-key-failures description: Synthesize the common stuck points across failed decomposition plans. Use when the current batch of decomposition plans has failed — whether they failed already at direct proving or only after further attempts.
Use this skill to turn many failed attempts into reusable guidance for the next planning round.
Read:
1. Gather the reports from all failed plans. If only direct proving has run so far, work directly from the direct-proving failures. 2. List the key stuck points for each plan. 3. Identify common points across those failures:
4. Summarize what the failures suggest for the next generation of decomposition plans. 5. When all current decomposition plans have failed and no pattern is leading anywhere, publish the synthesized `dead_end` (below): the main agent reasons or launches exploratory subagents, then delivers a fresh direction as `master_guidance`. 6. Save the synthesized failure knowledge to `failed_paths` so later planning skills can use it. 7. After recording the failure synthesis, return control to `$propose-subgoal-decomposition-plans`.
Publish the failure synthesis to global memory with `gm_add` (kind `dead_end`): `claim` = the common stuck points, `evidence` = the per-plan failures, so siblings skip these paths. Carry these fields:
{
"record_type": "key_failures_summary",
"failed_plan_ids": ["..."],
"plan_failures": [
{
"plan_id": "...",
"stuck_points": ["..."]
}
],
"common_failures": ["..."],
"implications_for_next_plans": ["..."]
}Also note in your local memory (`events`) that a new planning round is needed.
If the reports are too weak to identify meaningful common failures, note in local memory (`events`) `event_type="key_failures_inconclusive"` and state what information is still missing.
🚀✨ News: This branch is the version that solved YTD. 🎉 Danus orchestrates mathematical reasoning agents with fact-graph memory.
Validate externally referenced theorems by querying arXiv theorem search first and Codex's…
Aggregate all detected errors and gaps into the final verification report, apply strict…
Verify a markdown proof in the order it is written. Use when the task is to check local…
Construct candidate counterexamples to test a proposed conjecture, lemma, or intermediate…
Generate and analyze simpler examples that satisfy both the assumptions and the conclusion of…
Screen a decomposition plan by first trying to prove all of its subgoals directly, then…