check-referenced-state…
Validate externally referenced theorems by querying arXiv theorem search first and Codex's…
Find program-conditioned math results, constructions, examples, counterexamples, analogies, and background references. Use when the current active program needs repair, mutation, analogy, a program shift, or carefully gated obstruction search.
$ npx -y skills add frenzymath/Danus --skill search-math-results --agent claude-codeHow it fires
How this skill gets triggered: by you, by Claude, or both.
/search-math-resultsContext preview
The summary Claude sees to decide when to auto-load this skill.
Find program-conditioned math results, constructions, examples, counterexamples, analogies, and background references. Use when the current active program needs repair, mutation, analogy, a program shift, or carefully gated obstruction search.
name: search-math-results description: Find program-conditioned math results, constructions, examples, counterexamples, analogies, and background references. Use when the current active program needs repair, mutation, analogy, a program shift, or carefully gated obstruction search.
Use this skill as the default retrieval workflow for mathematical background and related results, conditioned on the live research program currently being pursued.
Read:
If the prompt explicitly declares the `program_stage`, `active_program`, `missing_mechanism`, or blocker policy, obey those declarations. If the prompt does not declare the stage, default to `fresh_orientation` for a new problem, first-pass search, or no mature program yet; use `active_program` when the run already has a live named program, branch, or missing mechanism; and use `mature_subproblem` only when the run is already narrowed to a repeatedly failed mature subproblem or mature active program.
`theorem_level_blocker` is not a default mode. It is disallowed by default in `fresh_orientation`. It is allowed in `mature_subproblem` when the blocker search targets that narrowed mature subproblem or mature active program rather than the whole original goal. It is also allowed whenever the prompt explicitly asks for obstructions, impossibility results, blocker theorems, or negative evidence. If blocker mode is not allowed, downgrade to `repair`, `mutation`, `analogy`, or `program_shift`.
Broad and creative search is allowed. Do not restrict yourself to the surface vocabulary of the current problem or only the literal keywords in the prompt. Cross-field and apparently unrelated analogy search is acceptable when it targets the same missing mechanism. Theorem-level, proof-level, theory-level, and more abstract analogy search are all allowed when tied to a plausible transfer idea.
1. Identify the current `program_stage`, `active_program`, `missing_mechanism`, and `search_mode` before searching. 2. For non-blocker modes, usually generate searches in multiple layers. In `fresh_orientation`, allow broad object-level, theorem-level, proof-pattern, and theory-pattern queries. In `active_program` and `mature_subproblem`, still allow broad queries, but tie them to the active program or a plausible program shift. 3. Start with `search_arxiv_theorems`. 4. When using `search_arxiv_theorems`, phrase the query as a complete mathematical statement whenever possible, but also issue mechanism- and analogy-driven queries when they better target the missing mechanism. Each hit carries `title`, the full verbatim `theorem` text, `arxiv_id`, and the in-paper `theorem_id`; use `arxiv_id` to pull the exact paper. 5. Inspect the returned items and decide whether they are useful for the current active program. 6. Do not use broad recursive scans of `downloads/` as a theorem-search engine. If an exact local paper/file is already known or prompt-recommended, read that exact path. Otherwise search externally first. If relevant long-term papers already exist in `downloads/common`, prefer those exact files before re-downloading. 7. If a genuinely new technical branch is opened (a new class of objects, a new construction regime, or a new body of machinery), then before killing that branch normally do at least one of the following: download and read at least one exact paper about that direction; read an exact local paper already present in `downloads/common` or another exact prompt-recommended path; or explicitly justify why no extra literature layer is needed because the branch has already reduced to a previously audited regime. 8. External search first is still the default, but once a genuinely new direction is chosen, exact paper download/read is expected before final branch rejection. This rule is about depth of engagement with a new direction: use a small number of exact relevant papers, not no papers and not many-paper rummaging. 9. Keep all downloaded PDFs and extracted text files organized inside `downloads/` in the current working directory. 10. If a useful theorem/example/counterexample is found and it comes from a paper, download that paper into the workspace, extract its text, and read the extracted text before relying on the result. 11. If a useful theorem is found, do not stop at the statement alone. Read the proof of that theorem as well and extract any techniques, constructions, r
🚀✨ 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…