| name | obtain-immediate-conclusions |
| description | Derive immediate mathematical consequences from a theorem statement or subgoal. Use when starting a new problem, branch, or subgoal, or when cheap progress or a cleaner reformulation is needed before deeper proof search. |
Obtain Immediate Conclusions
Extract direct implications before speculative reasoning.
Input Contract
Read from memory and current context:
problem_id- current theorem/subgoal statement
- memory
Procedure
- Normalize notation and restate the claim in equivalent forms.
- List direct consequences that follow from definitions and basic algebraic/logical manipulations.
- Split consequences into necessary conditions and candidate sufficient conditions.
- Mark each consequence with confidence and justification type.
- For every conclusion, explicitly decide whether it is likely fragile and should be stress-tested by counterexample.
- If a conclusion is fragile, record why it is fragile and indicate that
$construct-counterexamples should be considered next.
Output Contract
Append each conclusion to immediate_conclusions with JSON object payload:
{
"statement": "...",
"justification_type": "by_definition|calculation|known_fact|logical_equivalence",
"confidence": 0.0,
"is_fragile": false,
"fragility_reason": "",
"suggested_followup": "none|construct-counterexamples",
"scope": "global|branch|subgoal",
"branch_id": "optional",
"subgoal_id": "optional"
}
Rules:
is_fragile must always be present.- If
is_fragile=true, then fragility_reason must explain the risk and suggested_followup should be construct-counterexamples.
- If
is_fragile=false, use fragility_reason="" and suggested_followup="none".
MCP Tools
memory_appendmemory_searchsearch_arxiv_theorems for nontrivial consequences- Codex built-in web search for background definitions/terminology
Failure Logging
If no meaningful consequence is found, append an events entry with:
event_type="immediate_conclusions_stalled"- missing assumptions and suspected blockers
