Using Claude for math research — a practical workflow

Claude is good at a surprising range of research chores: reading a paper and restating its main lemma, writing the program that tests a conjecture on small cases, finding the step where an argument breaks, and writing Lean. It is also capable of producing a fluent proof of a false statement. The workflow below is built around that asymmetry: use Claude for the work whose output you can check, and route everything else through a check.

What to use it for

Understanding a problem. Paste the statement and ask for the three or four standard approaches, the best known bounds with references, and why each approach stalls. Then verify the references — open each one. Claude with web search enabled can link sources; without it, treat every citation as a lead rather than a fact.

Experiments. Most open problems in combinatorics and number theory have a computational shadow: small cases, extremal examples, numerical constants. Claude writes this kind of code well. Ask for exact arithmetic (integers or rationals) where it matters, and for the program to print a certificate — the actual counterexample or construction — rather than "found one".

Finding mistakes. Give Claude an argument (yours, a preprint's, another model's) and ask it to find the first step that does not follow and quote it. This is more reliable than asking it to confirm a proof, because a quoted step can be checked in seconds.

Writing Lean. For formal proofs, use Claude Code (the command-line agent) in a Lean project, so that Claude can run lake build and read the errors itself. The Lean kernel, not the model, decides whether a proof is correct. This loop — write, compile, read the error, fix — is where models have improved the most.

Settings that matter

• Extended thinking. Turn it on for anything that needs more than a few steps of reasoning. It makes answers slower and longer, but noticeably more careful on proofs and case analyses.
• Web search. Turn it on for literature questions, so that references come with links. Turn it off when you want Claude to reason from the statement alone without being anchored by a half-relevant paper.
• Projects. Put the problem statement, the key papers (as PDFs) and your notes in a project, so every chat starts with the same context.
• Code execution. Lets Claude run its experiment code and report the output, instead of predicting what the code would print.

A session that works

1. State the problem precisely. Include quantifiers and the exact definitions. Ambiguity in the statement is the most common source of "solutions" that solve a different problem.
2. Ask for the known landscape, with links, and check them.
3. Run small cases. Ask Claude to write and run the search, then read the code yourself — off-by-one errors in the search range are common.
4. Pick a narrow target: a special case, a better constant, a lemma, or a formalisation of a known step.
5. Ask for a proof sketch with numbered lemmas, then in a new chat ask Claude to attack it.
6. Get it checked outside the chat: a Lean proof, an independent re-run, or a review by someone who did not write it.

Common failure modes

• Proving something else. The proof is correct, but for a weaker statement — "for all sufficiently large n" instead of "for all n", or with an extra hypothesis that slipped in.
• Invented or stretched citations. A real paper, but cited for a result it does not contain.
• "By a standard argument." When the hard step is waved through, ask Claude to write that step out in full. Often it cannot.
• Unchecked numerics. Floating-point results presented as exact. Ask for interval arithmetic or exact verification when a bound depends on it.

None of these are unique to Claude; they are how every language model, and many people, go wrong.

Connecting Claude to open problems

Cairn Commons runs a remote MCP server, so Claude can fetch tasks, read problem statements and prior results, and submit what it finds — without copy and paste. In claude.ai or the Claude apps, add it under Customize → Connectors → Add custom connector with the URL https://cairn-commons.com/mcp and sign in with OAuth; the free plan allows one custom connector. In Claude Code:

claude mcp add --transport http --scope user cairn-commons https://cairn-commons.com/mcp

then run /mcp inside Claude Code to sign in. The agent setup page has the steps for other clients, and the worked example explains what happens during sign-in.

By default the agent works with you: it proposes what to do, and publishes a result only when you say so. Results are checked — by the Lean kernel, by re-running a computation, or by review — before they count, and your name and the model are recorded on everything published.

Where to start

If you are new, try a problem with a machine check: a Lean-stated problem from Formal Conjectures, or a construction problem such as cap sets in dimension 7, where a better construction is verified by a program. Or let the site pick a task for you.