| name | search-math-results |
| description | Find relevant math results, constructions, examples, counterexamples, and background references for a statement. Use when you need context for a new problem, supporting references for constructing examples or counterexamples, or external results while proving subgoals. |
Search Math Results
Use this skill as the default retrieval workflow for mathematical background and related results.
Input Contract
Read:
- the current target statement, subgoal, lemma, or claim
- the search intent:
theorem
construction
example
counterexample
background
- relevant branch/subgoal context from memory
Procedure
- Start with
search_arxiv_theorems.
- When using
search_arxiv_theorems, phrase the query as a complete mathematical statement whenever possible.
- Inspect the returned items and decide whether they are useful for the current need.
- 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.
- 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, reductions, or proof patterns that may help with the current target statement.
- Expand the definitions and concepts appearing in that theorem using the surrounding context of the paper, and check carefully whether the theorem is actually applicable to the current situation. Be explicit about terminology that may shift across contexts.
- If the theorem is only a partial result for the current problem, analyze why its method does not immediately prove the full target statement. If it assumes extra hypotheses, do not merely try to force the current object to satisfy them; instead record why those hypotheses are used, where the proof breaks without them, and what obstruction or difficulty this reveals.
- Keep all downloaded PDFs and extracted text files inside
downloads/ in the current working directory.
- Record not only what the theorem says, but also what its proof suggests for the current problem.
- If the theorem search returns no useful information, switch to Codex's built-in web search.
- Use the built-in web search either to look for specific math results or to gather background information, terminology, standard references, and canonical constructions/examples/counterexamples.
- If the built-in web search reveals a useful paper, again download it, extract its text, and read the relevant extracted text before using it in reasoning.
- If the built-in web search reveals a useful theorem, also read its proof, expand its local definitions from the paper context, and extract the techniques that look adaptable to the current statement.
- If the built-in web search reveals only a partial result, perform the same partial-result analysis: extra hypotheses, why the method needs them, why the method does not solve the full current problem, and what real difficulty is exposed.
- Summarize the most useful findings and explain why they matter for the current proof state.
- If a result may later be used in a proof, preserve its full statement and source identifiers so downstream proof steps can cite it explicitly.
Usefulness Test
Treat theorem-search results as useful only if they do at least one of the following:
- provide a theorem/lemma/definition close to the target statement
- provide a construction/example/counterexample that can be adapted
- suggest a standard technique or reformulation relevant to the current branch
- expose a meaningful obstruction or extra hypothesis in a partial result that clarifies why the full problem is harder
If the results are vague, off-topic, or too weak to guide the next step, fall back to the built-in web search.
Output Contract
Append a summary record to events:
{
"event_type": "search_math_results",
"query": "...",
"search_intent": "theorem|construction|example|counterexample|background",
"primary_tool": "search_arxiv_theorems",
"fallback_used": false,
"results_summary": ["..."],
"useful_references": [
{
"title": "...",
"complete_statement": "...",
"url_or_id": "...",
"paper_id": "...",
"arxiv_id": "...",
"theorem_id": "...",
"local_pdf_path": "optional",
"local_text_path": "optional",
"expanded_definitions": ["paper-context expansions of terms/concepts used in the statement"],
"applicability_check": ["why the statement does or does not apply in the current setting"],
"partial_result_analysis": ["extra hypotheses, where the method fails for the full problem, and what difficulty this reveals"],
"proof_insights": ["optional extracted techniques or ideas from the proof"],
"why_useful": "..."
}
],
"branch_id": "optional",
"subgoal_id": "optional"
}
MCP Tools
search_arxiv_theorems
memory_append
memory_search
Failure Logging
If neither theorem search nor web search yields useful information, append an events record with:
event_type="search_math_results_stalled"
- the attempted queries
- the reason the results were not useful