construct-toy-examples - SKILL.md Agent Skill

name: construct-toy-examples description: Generate and analyze simpler examples that satisfy both the assumptions and the conclusion of a theorem statement or subgoal. Use when you are stuck in reasoning and need simpler examples to regain traction, when you need simpler examples that satisfy both assumptions and conclusion, or when you want to see where the assumptions take effect and gain intuition.

Construct Toy Examples

Use this skill when the agent is stuck in reasoning and needs simpler examples that satisfy both the assumptions and the conclusion in order to understand why the statement works.

Input Contract

Read:

current statement/subgoal
relevant immediate_conclusions
relevant counterexamples and failed branch notes
relevant background/results when available

Procedure

Construct simpler cases (low degree, small dimension, special forms, canonical objects).
Ensure the toy example satisfies all assumptions of the target statement or subgoal.
Check that the conclusion also holds in the toy example.
Study where each assumption takes effect and what mechanism makes the conclusion true.
Identify repeated patterns, invariants, or proof ideas suggested by the example.
Use search/reasoning/decomposition as needed to find examples or simplify the situation.

Output Contract

Append to toy_examples:

{
  "example": "...",
  "why_relevant": "...",
  "assumptions_satisfied": ["..."],
  "conclusion_verified": true,
  "where_assumptions_take_effect": "...",
  "observed_pattern": "...",
  "supports_branch_ids": ["optional"],
  "subgoal_id": "optional"
}

MCP Tools

memory_append
memory_search
search_arxiv_theorems for matching examples/known motifs
Codex built-in web search for known example families and standard constructions
use $search-math-results when broader retrieval is needed

Failure Logging

If generated examples are inconclusive, append an events record:

event_type="toy_examples_inconclusive"
include attempted example families