meleantonio/open-math-prover

open-math-prover is a plugin that helps AI coding assistants attempt unsolved problems in mathematics. It works with several popular tools, including Claude Code, Cursor, Codex, Grok, GitHub Copilot, and Gemini CLI. The project packages techniques from two sources: Shouqiao Wang's Erdős workflow and OpenAI's Cycle Double Cover multi-agent prompt. The README is clear that this tool does not magically solve every open problem. Instead, it implements a structured research loop. The plugin provides several components. There are skills for running a full attack loop, selecting which problem to work on, crafting proof prompts, and running adversarial audits where one agent tries to find flaws in another's work. It also includes agent role definitions for an orchestrator, an approach explorer, an adversarial auditor, and a computational checker. Template files help organize each attempt into a workspace with clear deliverables. The method rests on three main ideas. First, it filters for problems mathematicians already care about, while excluding those that are clearly out of reach. Second, it builds careful prompts that restate the problem precisely and define what a complete proof would look like. Third, it supports long runs where multiple agents attempt different approaches, fail, diagnose what went wrong, and try again. Every draft goes through adversarial review before being accepted. Installation happens through a shell script that copies files into the correct directories for whichever coding assistant you use. You can also install it manually by copying the skills and agents folders. Once installed, you can run the full loop with a single command and a pasted problem statement, or run each step individually. The README includes a strong disclaimer: AI-generated proofs can be wrong. It recommends adversarial audit, human expert review, and formal verification before treating any result as established mathematics.