How to use AI for math research: a step-by-step workflow with prompts

AI models now take part in real results on open problems — and in many more claims that fall apart. The difference is almost never the model. It is whether the work was set up so that every output gets checked. This workflow does that. It works with any frontier chatbot, free or paid, and with agents such as Claude Code or Codex.

Each step has a prompt you can paste. Replace the parts in angle brackets.

1. Fix the statement

Most wrong "solutions" are correct proofs of a different statement. Write the problem with every quantifier, range and definition, and ask the model to attack the wording, not the problem.

Here is a problem statement: <statement>. Do not try to solve it. List every ambiguity: quantifiers, ranges, edge cases (n = 0, 1, small primes), definitions that have several standard versions. Then rewrite the statement so that it has exactly one meaning.

If the problem comes from a list (Erdős problems, Ben Green's 100, a paper's open questions), copy the original wording and its number, and keep both versions.

2. Search before you reason

On curated lists, the most common "AI solution" is a paper that already solved the problem. Finding it is a real contribution; inventing it is the most common failure.

Find published work on <statement>: full solutions, special cases, the best known bounds, and the standard approaches. For each item give authors, year, venue, the exact statement proved, and a link. Mark anything you are not sure exists.

Turn web search on, and open every link. A reference you cannot open is a lead, not a fact.

3. Run small cases

Almost every problem in combinatorics and number theory has a computational shadow. Use a model that runs code, and ask for the evidence, not a verdict.

Write a self-contained Python program that checks <statement> for all <parameters> up to <N>, using exact integer or rational arithmetic. Print every counterexample and the ten closest calls, and the time taken. Then run it and show me the output.

Read the code before trusting the output: search ranges and off-by-one errors are where experiments go silently wrong.

4. Pick a narrow target

"Solve the conjecture" is not a target. A special case, a better constant, an explicit construction, a lemma, or a formal statement is. Narrow targets are where AI models now succeed, and where a result can be checked.

Given what we found, list five sub-problems of <problem> that are (a) not already solved in the literature, (b) small enough to settle in a day, and (c) checkable by a computer or by a short proof. For each, say how a solution would be verified.

5. Attempt it

Use the strongest reasoning mode you have, and ask for structure you can check.

Prove <narrow target>. Structure the proof as numbered lemmas, each with a precise statement and a proof. Mark every step you are not sure of with [UNSURE]. Do not write "by a standard argument": write the argument.

For constructions, ask for the object itself in a file, not a description of it.

6. Attack it — in a new chat

The chat that wrote a proof is the worst judge of it. Open a new chat, or use a different model, and ask it to break the argument.

Here is a proof of <statement>. Find the first step that does not follow. Quote it exactly and explain why it fails. If every step holds, list the three steps that most need an independent check, and say why.

Repeat until the attacks come back empty, or until you find the gap. A documented gap is a result too.

7. Make it checkable by others

A result counts when someone else can check it without trusting you or the model:

• Constructions and counterexamples: publish the object and a short checker program.
• Proofs: a Lean formalisation against a statement agreed in advance (see How to check an AI proof with Lean), or a write-up a reviewer can follow.
• Literature finds: the paper, the page, and the exact statement it proves.

Record the model, the mode, the date and the prompts.

Doing this on Cairn Commons

Cairn Commons runs this workflow as small tasks: your chatbot gets one step on an open problem — a literature check, a small case, an attack on someone's argument — and the result is checked by Lean, by re-running code, or by blind review before it counts. It takes about ten minutes, needs no account to try, and a well-documented dead end counts. Start with a task for your chatbot, or beat a record a computer checks.

Which model to use for which step is covered in Best AI for math research; the model-specific details are in the Claude and ChatGPT guides.