# open-problem-prover
**A plugin for every major coding agent that turns it into a disciplined mathematical
research machine for attacking open problems.**
It implements, in reusable form, the workflow
[Shouqiao Wang used in July 2026](https://x.com/Qiaoqiao2001/status/2080003441821163958)
to resolve **6 open Erdős problems in 5 days** (of ~13 attempted, with GPT-5.6 Sol at
Ultra reasoning inside Codex, 6–32 hours per problem), building on OpenAI's
cycle-double-cover experiment. Wang published his prompts, papers, verifiers, and Lean
formalizations at [ShouqiaoW/erdos](https://github.com/ShouqiaoW/erdos); this plugin
generalizes those techniques so any agent — Claude Code, Codex, Cursor, Copilot, Gemini
CLI, Windsurf, Cline, Aider, or anything that reads `AGENTS.md` — can run the same
playbook on new problems. See [docs/methodology.md](docs/methodology.md) for the full
technique-by-technique mapping.
> **Reality check.** An AI-generated proof is a *claim*, not a theorem. This workflow's
> entire design goal is making it hard for wrong proofs to survive — contract firewalls,
> adversarial audits, exact-arithmetic verifiers, Lean formalization, and a mandatory
> human gate before any public statement. Expect roughly half of well-chosen attempts to
> fail. That is the base rate of the method working as intended.
## The six techniques
1. **Problem selection** — attack problems experts actively discuss; discard anything
equivalent to or blocked by a major conjecture; prefer finite, computable,
formalizable structure.
2. **The proof contract** — before any proving, write a document that defines *exactly
what counts as a solution*: precise restatement, affirmative AND negative resolution
criteria, known background and what it does **not** imply, a long firewall of
insufficient near-misses, reformulation invariants, problem-specific traps, allowed
tools, exit criteria.
3. **Portfolio search** — many genuinely different routes explored *independently*
(explorers don't see each other's notes or the favored route), tracked in a route
ledger; routes blocked at theorem-strength gaps; both resolution directions kept
alive; artifacts required, status reports rejected.
4. **Computation as evidence** — counterexample-hunt your own lemmas first; SAT/ILP/
exact-cover encodings for finite subproblems; exact arithmetic (no floats) for
anything reported; "computation is evidence unless converted into rigorous proof or a
finite certificate".
5. **Adversarial audit** — every draft is refereed by a fresh hostile auditor that sees
only the contract and the draft, walks the trap lists item by item, expands every
"clearly", and recomputes load-bearing steps. Loop: *attempt → failure → diagnosis →
new approach → draft → audit → repair.*
6. **Verification and disclosure discipline** — LaTeX paper with explicit lemma
dependencies, companion exact-arithmetic verifier stating what it does NOT check,
Lean 4 formalization where feasible, and a human gate (plus community norms, e.g.
[erdosproblems.com](https://www.erdosproblems.com) forum policies) before any claim.
## Install
### Claude Code (plugin)
```bash
/plugin marketplace add meleantonio/open-problem-prover
/plugin install open-problem-prover@open-problem-prover
```
You get slash commands `/select-problem`, `/draft-contract`, `/prove`, `/audit`,
`/verify-numerics`, `/write-paper`; subagents `approach-explorer`,
`adversarial-auditor`, `computational-experimenter`, `literature-scout`; and the
`proof-contract` / `research-loop` skills.
### Everything else (one script)
```bash
git clone https://github.com/meleantonio/open-problem-prover
cd open-problem-prover
./install.sh --codex ~/my-math-project # or --cursor, --copilot, --gemini,
# --windsurf, --cline, --aider,
# --claude (file copy), --all
```
The installer copies the canonical methodology (`AGENTS.md` — read natively by Codex,
Cursor, Gemini, OpenCode, Amp, Jules, and others), the templates, and the per-agent
pieces: Codex custom prompts (`~/.codex/prompts/`), Cursor rules (`.cursor/rules/`),
Copilot instructions + prompt files (`.github/`), Gemini commands
(`.gemini/commands/*.toml`), Windsurf rules, Cline rules, or Aider conventions. Details
per agent in [adapters/](adapters/).
## Use
```text
/select-problem problems discussed on erdosproblems.com involving factorials
# pick one from the shortlist…
/draft-contract Erdős 390: is there a constant c with f(n) - 2n ~ c·n/log n?
# review the contract yourself — it caps the quality of everything downstream
/prove problems/erdos-390/contract.md # hours, not minutes
/audit problems/erdos-390/notes/route-3/draft-2.md problems/erdos-390/contract.md
/verify-numerics problems/erdos-390/paper.tex
/write-paper problems/erdos-390/
```
Run configuration matters: use the strongest model you have at the highest reasoning
setting, in a harness that can run long and keep files on disk. All state (contract,
route ledger, notes, experiments, audits) lives in `problems/<id>/`, so runs survive
interruption and even a mid-run switch to a different agent.
## Repository layout
```
AGENTS.md # canonical methodology (works standalone in any AGENTS.md-aware agent)
.claude-plugin/ # Claude Code plugin + marketplace manifests
commands/ agents/ skills/ # Claude Code slash commands, subagents, skills
templates/ # proof-contract.md, numerical_verifier.py
adapters/ # codex/, cursor/, copilot/, gemini/, windsurf/, cline/, aider/
docs/methodology.md # source thread → plugin mapping, with links
install.sh # per-agent installer
```
## Credits and sources
- Shouqiao Wang ([@Qiaoqiao2001](https://x.com/Qiaoqiao2001)) — the
[thread](https://x.com/Qiaoqiao2001/status/2080003441821163958) and
[ShouqiaoW/erdos](https://github.com/ShouqiaoW/erdos) (prompts, papers, verifiers,
Lean). The workflow implemented here is his; errors in the generalization are mine.
- OpenAI — the cycle-double-cover prompt that inspired Wang's contracts; see
[Early science acceleration experiments with GPT-5](https://arxiv.org/abs/2511.16072).
- [erdosproblems.com](https://www.erdosproblems.com) (Thomas Bloom) — the problem
database and forum where claims are discussed.
This repository contains no text from Wang's prompts or papers; it re-implements the
method from scratch. If you use this plugin and it works, cite the people above, not
this repo.
## License
MIT — see [LICENSE](LICENSE).