Prove2Me
Vintage: 2026-09. Primary evidence is Anthropic's Sep 4, 2026 Science Blog as hydrated in 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean, plus the blog-cited paper Prove2Me: An open collaborative platform for scaling math formalization (Chen, Marwaha, Lu, Yuen, Peng; arXiv:2608.28433). The paper body was not fetched this pass — cite the URL, do not invent abstract claims. This page is the named scaffold for claude-flt-lean-formalization, not a rewrite of agent-harness or claude-code.
Prove2Me
One-line summary: Named math-formalization platform Anthropic credits for Claude's Sep 4, 2026 Lean-checked Fermat's Last Theorem artifact — a DAG of theorem statements with statement/proof file separation and natural-language search/reuse.
What it is
A named harness / platform for scaling math formalization. From 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean (Anthropic Science Blog, Sep 4, 2026): Anthropic attributes the FLT success to switching to Prove2Me — a DAG of theorem statements, statement/proof file separation, and natural-language search/reuse — plus a claude-code multi-agent harness.
The scaffolding paper cited on that blog is Prove2Me: An open collaborative platform for scaling math formalization (Chen, Marwaha, Lu, Yuen, Peng; arXiv:2608.28433). URL present; paper body not fetched.
Why it matters to this thread
Harness design is in-scope (agent-harness). This is the first dated named math-formalization platform in the thread, and the blog treats the switch to it as the load-bearing change versus earlier failed runs. Distinct from the generic Claude Agent SDK / planner-generator-evaluator story already on claude-code.
Key facts (from 2026-09-04-anthropic-claude-formalizes-fermats-last-theorem-in-lean)
- Shape (blog): DAG of theorem statements; statement/proof file separation; natural-language search/reuse.
- Attribution: blog says success came from switching to Prove2Me plus a Claude Code multi-agent harness.
- Failed-run residue: early runs without Prove2Me contributed ~7% of non-boilerplate lines in the FLT artifact.
- Paper: arXiv:2608.28433 — cited on the blog; body not fetched.
- Not the FLT claim itself. The Lean-checked theorem, axiom guard, and verification story live on claude-flt-lean-formalization and the GitHub README.
What this source does not establish
- No fetched paper body. Do not invent abstract claims, benches, or author quotes beyond the blog's one-line description.
- Not a rewrite of agent-harness Anthropic/LangChain definitions or the official TB 2.0 harness-swing table.
- Not a Claude Code SKU. Multi-agent Claude Code is the companion harness; Prove2Me is the math DAG / statement-proof scaffold.
- No person pages for Chen / Marwaha / Lu / Yuen / Peng from the paper byline.
Open questions
- What does the unfetched arXiv body add (architecture, evals, collaboration model) that the blog's one-line description omits?
- How much of the FLT result is Prove2Me versus the Claude Code multi-agent loop versus the Fable-comparable internal model?