# open-math-prover
**Multi-agent plugin for attacking open problems in mathematics** — works with Claude Code, Cursor, Codex, Grok, GitHub Copilot, and Gemini CLI.
It packages the techniques from [Shouqiao Wang’s Erdős workflow](https://x.com/Qiaoqiao2001/status/2080003441821163958) and [OpenAI’s Cycle Double Cover multi-agent prompt](https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf) into installable skills, agents, and workspace templates.
> This does **not** magically solve every open problem. It implements a disciplined research loop: careful problem selection, exact success criteria, diverse proof search, and adversarial audit.
## What you get
| Component | Role |
|-----------|------|
| **`/open-math-prover`** | Full end-to-end attack loop |
| **`/select-open-problem`** | Score and filter candidates |
| **`/craft-proof-prompt`** | Build CDC-style problem-specific prompts |
| **`/adversarial-audit`** | Hostile independent review of drafts |
| **Agents** | orchestrator, approach-explorer, adversarial-auditor, computational-checker |
| **Templates** | `PROBLEM.md`, `PROMPT.md`, `APPROACHES.md`, proof + audit files |
| **`AGENTS.md`** | Universal instructions for any coding agent |
## The method (three secrets)
1. **Problem selection** — Prefer problems mathematicians already care about; filter out items tied to major open conjectures or clearly out of reach.
2. **Prompt construction** — Restate precisely; define what complete proof/disproof means; list non-counting partial results; list traps; require adversarial agents; manage multi-approach search (diverse portfolio, blocked weak reductions, keep incompatible routes alive).
3. **Long multi-agent runs** — Strong reasoning model + patient coding agent with local files; loop: attempt → failure → diagnosis → new approach → draft → adversarial audit → repair.
Details: [`references/workflow.md`](references/workflow.md).
## Install
### Option A — Installer (recommended)
```bash
git clone https://github.com/meleantonio/open-math-prover.git
cd open-math-prover
chmod +x scripts/install.sh
./scripts/install.sh user # ~/.claude, ~/.cursor, ~/.grok, ~/.codex, ~/.gemini, ~/.agents
# or into a research repo:
./scripts/install.sh project /path/to/your/project
```
### Option B — Claude Code plugin marketplace
If you maintain a marketplace repo, point it at this repository’s `.claude-plugin/plugin.json`. Locally you can also copy or symlink:
```bash
ln -s /path/to/open-math-prover ~/.claude/plugins/open-math-prover
# or add as a project plugin depending on your Claude Code version
```
### Option C — Manual skill copy
Copy `skills/*` into any of:
| Agent | Skills path |
|-------|-------------|
| Claude Code | `.claude/skills/` or `~/.claude/skills/` |
| Cursor | `.cursor/skills/` or `~/.cursor/skills/` |
| Grok | `.grok/skills/` or `~/.grok/skills/` |
| Codex | `.agents/skills/` or `~/.codex/skills/` |
| Gemini CLI | `.gemini/skills/` |
| GitHub Copilot | `.github/` plugin manifest + `skills/` |
Copy `agents/*` into `.claude/agents/` (and equivalents). Copy or merge root [`AGENTS.md`](AGENTS.md) for universal behavior.
## Quick start
```text
/open-math-prover
Attack this problem: [paste exact statement]
```
Or stepwise:
```text
/select-open-problem
/craft-proof-prompt
/open-math-prover
/adversarial-audit
```
Each serious attempt should use a workspace under `problems/<slug>/` (templates in `templates/problem-workspace/`).
## Repository layout
```text
open-math-prover/
├── AGENTS.md # universal agent instructions
├── skills/ # SKILL.md packages (all major agents)
│ ├── open-math-prover/
│ ├── select-open-problem/
│ ├── craft-proof-prompt/
│ └── adversarial-audit/
├── agents/ # role definitions
├── references/ # workflow, CDC heuristics, templates docs
├── templates/problem-workspace/
├── scripts/install.sh
├── .claude-plugin/plugin.json
└── .github/plugin.json
```
## Design principles
- **Exact statement** — never silent strengthen/weaken
- **Complete resolution only** — partial progress is not success
- **Diverse search** — many independent approach families
- **Adversarial audit** — every candidate is attacked
- **Block weak reductions** — comparable-strength missing lemmas mark a route blocked
- **Concrete deliverables** — lemmas, constructions, counterexamples; no vague optimism
- **Checkpointable** — state lives in markdown files for multi-hour / multi-session runs
## Credits & sources
- Workflow inspiration: [Shouqiao Wang (@Qiaoqiao2001)](https://x.com/Qiaoqiao2001/status/2080003441821163958) and [ShouqiaoW/erdos](https://github.com/ShouqiaoW/erdos)
- Multi-agent prompt structure: [OpenAI CDC prompt PDF](https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf)
- Packaging: [meleantonio/open-math-prover](https://github.com/meleantonio/open-math-prover)
This repository is an independent agent plugin. It does not claim authorship of the original Erdős proofs or OpenAI’s CDC work.
## License
MIT — see [LICENSE](LICENSE).
## Disclaimer
AI-generated proofs can be wrong. Always require adversarial audit, human expert review, and ideally formal verification (e.g. Lean) before treating a result as established mathematics.