Eight focused agent skills for ambitious mathematical research, diverse proof search, constructive scrutiny, and optional Lean formalization.
Give your agent a precise problem and room to make progress. This plugin helps it develop genuinely different approaches, pursue the decisive proof step, use established lemmas immediately, and explain achievements with confidence and enthusiasm. Focused audits turn objections into concrete repairs. Optional Lean skills distinguish the intended theorem from the declaration a checker actually accepts.
Created by Leonard van Hemert. An original workflow informed by the published Cycle Double Cover research prompt and practical mathematical research; see sources and attribution. No particular model, fixed agent count, or mandatory computer proof is required.
Install · Examples · Skills · Lean · Releases · Validation
Use a Codex CLI with plugin marketplace support:
codex plugin marketplace add LeonardSEO/ambitious-math-research --ref main
codex plugin add ambitious-math-research@leonardseo-mathStart a new Codex session, then invoke the appropriate skill by name or select it in the skill picker. Installation registers the plugin in your Codex environment; it does not edit your research papers or install Lean.
For a reproducible snapshot, use --ref v0.2.0 instead of --ref main when registering a fresh marketplace. The release archive also provides a standalone Agent Plugins 1.0 package with a Codex compatibility manifest. Other hosts need their own supported plugin-import flow.
Create an ambitious brief without starting research
$research-brief Turn this conjecture and the supplied papers into an exact research
brief, a motivating launch prompt, and a one-paragraph goal draft.
Include the quantifiers, edge cases, and what would count as a complete resolution.
Do not activate the goal or start research yet.
Continue from proved results
$research-orchestration Resume from CHECKPOINT.md and use the established lemmas.
Develop genuinely different mechanisms for the remaining uniform estimate.
Pursue the strongest concrete next step and challenge its decisive inference.
Explain what each achievement enables, with enthusiasm grounded in the mathematics.
Challenge a candidate proof
$proof-audit Reconstruct the decisive step in this argument.
Check its actual hypotheses, parameter dependencies, and interchange of limits.
Return a concrete objection and repair obligation if it fails; state plainly
what is proved if it succeeds. Do not edit the manuscript.
Strengthen momentum
$research-momentum Write a short reinforcement prompt for the current agent.
Encourage confidence, persistence, and enthusiasm about the actual progress.
Keep the main theorem and its remaining proof obligation exact.
Pause with a useful handoff
$research-closeout Finish only the current bounded work, integrate complete results,
and preserve the exact next step. Assess whether this manuscript is ready to share,
would benefit from waiting, or needs substantive repair. Publish nothing.
| Your task | Skill | Result |
|---|---|---|
| Define the problem and launch instructions | research-brief | Exact target, motivating prompt, concise goal draft |
| Execute or resume mathematical work | research-orchestration | Diverse approaches, dynamic delegation, concrete proof steps |
| Maintain confidence and communicate progress | research-momentum | Enthusiastic, specific updates and reinforcement |
| Inspect a supplied mathematical argument | proof-audit | Decisive findings, scoped verdict, repair obligations |
| Assess originality and significance | contribution-review | Comparison with primary literature and precise contribution claims |
| Wind down or prepare a manuscript | research-closeout | Bounded completion, checkpoint, publication recommendation |
| Translate a theorem into Lean | lean-formalization | Statement mapping and a focused formal argument |
| Assess formal proof evidence | lean-verification | Actual target, diagnostics, transitive axioms, and verdict |
Skills are collaborators, rather than eight mandatory stages. The routing map explains when a handoff helps. Subagents use the host's native tools, available capacity, and current model defaults. If delegation is unavailable, the agent works sequentially and states that limit.
- Expect useful progress. Difficulty or a problem's open status is not a standalone reason to stop. Seek concrete mechanisms and proof obligations.
- Use proved results immediately. External acceptance and novelty assessment are separate from a complete mathematical argument.
- Keep approaches genuinely different. Preserve early independence and group routes by mathematical mechanism. An equivalent unproved conjecture remains a gap.
- Celebrate concrete achievements. Enthusiasm, including an occasional “Eureka,” belongs with a real discovery and its implications. The exact theorem still determines the claim.
- Check what matters. Audit load-bearing inferences. Reopen settled checks for changed hypotheses, new applications, or specific objections.
- Respect limits and pauses. Preserve the original target, user budget, and authorization. Goal drafts do not activate goals; publication advice does not publish anything.
The templates cover launch, reinforcement, restart, proof audit, closeout, and Lean handoffs. The state examples show compact route, claim, and checkpoint records. These workflows organize research; they do not guarantee a solution to an open problem.
Lean is useful for a requested formal proof or a decisive lemma where formal assurance adds value. It is optional for analytical research. A complete analytical proof can support subsequent work while its translation continues.
$lean-formalization Formalize the supplied bridge lemma in this existing Lean project.
Preserve the theorem's hypotheses and reuse matching library results.
Use the pinned toolchain; expose any remaining formal obligations.
$lean-verification Check whether Main.bridge proves the original stated theorem.
Compare its elaborated type and definitions, inspect build diagnostics, and record
its transitive axioms. Separate incomplete formalization from analytical proof status.
The skills use an available Lean/Lake project or an existing Lean-LSP-MCP connection. They do not install or upgrade Lean, mathlib, or a server automatically. A successful build with sorryAx, an assumed target, or a weaker statement does not establish the intended theorem. Standard logical axioms are not mistaken for missing mathematical lemmas. See Lean assurance for evidence levels and optional stronger checks.
Each release matches the version in plugin.json. Release assets include a standalone plugin ZIP and SHA256SUMS; compare the downloaded ZIP with its checksum before importing it.
For a marketplace following main:
codex plugin marketplace upgrade leonardseo-math
codex plugin add ambitious-math-research@leonardseo-mathStart a new session after updating. A pinned marketplace stays on its selected ref until you change it. Releases are published deliberately; there is no background upstream synchronization. The public GitHub package and any separately saved private account plugin have independent release states.
See CHANGELOG.md for versioned changes.
Package checks cover both manifests, eight skill declarations and UI metadata, the marketplace, local references, and release archive contents. Independent scenario exercises assess routing, immediate use of proved lemmas, concrete proof objections, contribution assessment, pauses, and Lean evidence interpretation. The validation report records the exercised scope and execution limits.
The repository itself contains research instructions, rather than a new mathematical theorem or a Lean proof corpus. Package validation and scenario exercises are not verification of future mathematical results. Lean compilation was not exercised for this release because a local toolchain was unavailable.
Use Python 3.11 or later in your preferred development environment:
python3 -m pip install -r requirements-dev.txt
python3 scripts/validate.py
python3 -m unittest discover -s tests -v
python3 scripts/package.py --output-dir ../amr-releaseGitHub Actions runs the package checks and tests on pushes and pull requests. The packager excludes repository administration, tests, development dependencies, and Git history; only the installable instructions, references, templates, assets, and public documentation enter the ZIP.
Open an issue with the plugin version, selected skill, expected behavior, and a small example that demonstrates the problem. Keep private manuscripts and credentials out of reports. Prefer a focused correction over adding a universal rule for one failed attempt.
Original instructions and design by Leonard van Hemert, released under the MIT license. Conceptual influences and optional upstream tools are credited in sources. No complete external skills or server implementations are bundled. This is an independent project, without an OpenAI or Lean endorsement.