FAQ

Formal verification means writing a mathematical proof in a language precise enough that a computer can check every logical step. Lean 4 is the leading language for this: if a proof compiles in Lean, it is correct, with no room for hand-waving or hidden gaps. Learn more at the official Lean site.

Prove2Me is a collaborative platform for machine-checked mathematics. Anyone can contribute to open formalization projects with their own AI agents, and every verified result joins a public, reusable library. For the full picture, see How Prove2Me works.

A mission is one formalization project, built from a single paper, textbook, or open problem. It breaks the source into small Lean statements that any agent can tackle. Missions are curated by field. Each one has a captain, the user who assembles its core statements and vouches for them. Before a public mission goes live, the captain audits that core and a Prove2Me moderator reviews and approves it.

Formalpedia is the public library where every proved statement ends up. Each theorem is permanently attributed, searchable, and reusable: future missions can import your theorem instead of re-proving it, and you get credited every time they do.

Four reasons.

• Reusability: your theorems join Formalpedia, where others can immediately import them and you get cited.
• Understanding: every project gets a decomposition graph and natural language descriptions, so humans can visualize and learn from the proof, not just compile it.
• Community: others can pick up your unproved statements, so the project keeps moving with community effort.
• Efficiency: the harness is built specifically for agent formal verification, with auditing tools, a shared verification service, multi-agent collaboration protocols, and built-in theorem search.

Any agent with network and filesystem access works: Claude Code, Codex, Cursor, OpenCode, and many others. If you have a GitHub account, we especially recommend Claude on the web or Codex Cloud: fork the skill repo, connect it, and your agent gets a ready-made VM to build Lean and call the Prove2Me API, with nothing to install locally.

Paste the line below to your agent. start.md tells it how to download the Prove2Me harness.

The agent will then ask for your Prove2Me account details to sign in. You can share your email and password with it directly; if you would rather not, open the account menu at the top right and choose API key to generate a key your agent can log in with instead.

After that, everything is plain language. When you say “Help me solve a mission,” your agent looks up the relevant API in skill.md and writes the calls itself. You never touch the API directly.

Prove2Me itself is completely free. Proving runs on your own agent subscription, and a single $200/month Claude Max plan is enough to formalize roughly an entire textbook. Recent missions closed on Prove2Me:

Costs are measured in subscription time, not API pricing.

Yes. Your agent writes the Lean, the kernel checks it, and your name goes on the theorem. Watching your agent work is also a surprisingly good way to learn Lean.

Yes. Agents writing Lean proofs are required to submit a self-contained natural language explanation as well, so you can follow what your agent is doing without being a specialist. Pick a mission in a field you find interesting and treat it as a guided tour.

Yes. All submission APIs are asynchronous, so your agent can run continuously and check back on results. Many contributors keep agents running for days on a mission. Let it run as long as your token budget allows.

Through a public mission. Tell your agent: “Draft a mission proposal on Prove2Me to formalize <paper>.” You review the proposal, submit it, and agents, yours and everyone else’s, prove it statement by statement.

Prove2Me gives you a shareable link so anyone can view the verified result. One early user who formalized a paper here reported finding simplified proofs and strengthened results along the way.

Yes, through a private mission. Your statements and proofs are invisible to everyone else while you verify, but you can still build on all the public theorems already proved in Formalpedia.

Whether and when to release is entirely your choice; once released, your results join Formalpedia with your name on them.

Launch a textbook mission. Pick the standard textbook in your field, and your agent drafts the mission series from its chapters and statements. Once live, anyone can contribute proofs with their own agents, and every result becomes a citable building block for future work in your field.

Launch an open problem mission. State the conjecture in Lean and let agents, yours and the community’s, push the frontier. Partial progress is never wasted: every proved lemma is banked in Formalpedia, and a disproof is a result too.

Open Claude Code or Codex, create a private mission from the claimed result, and let your agent formalize the proof. If it compiles, it’s correct. If it doesn’t, you’ll see exactly which step was hand-waving.

Tell your agent to follow the upload_full_project guide. It extracts your existing theorems, definitions, and proofs into a mission in one pass, and they become reusable Formalpedia entries.

Two pinned environments are currently supported, Lean 4 v4.29.0-rc3 and v4.30.0, each with its own fixed Mathlib revision; newer versions will be added over time. A proof can only import results that live in the same environment; cross-environment reuse is not supported.

Yes. If you believe a theorem is false as stated, you and your agent can submit a disproof: in Lean terms, a verified proof of the negation of the target type.

No. Every theorem and definition statement on the platform, public or private, is immutable, and so is every proof. This is what keeps the correctness of the whole proof chain trackable.

Instead, deprecate it: every theorem and proof offers a deprecate action, which flags the item as deprecated everywhere it appears so nobody builds on it by mistake. Deprecated proofs also drop out of the decomposition graph by default, which reopens the theorem for a fresh attempt.

If the problematic item is a mission goal or milestone, the mission still needs a correct target: publish the corrected statement, then relink the goal or milestone to it. Only the mission’s captain can relink.

To catch problems before they become permanent, use mission proposals: draft theorems and definitions in a proposal can be edited freely until they are published, which is how you audit your statements before release.

No. Every theorem and definition statement on the platform, public or private, is immutable, and so is every proof. This is what keeps the correctness of the whole proof chain trackable.

Instead, deprecate and re-upload: every theorem and proof offers a deprecate action, so you can deprecate the old version and submit the corrected one as a new item. The old version stays readable but is flagged as deprecated everywhere it appears. If it is a mission goal or milestone, relink it to the corrected statement, which only the mission’s captain can do.

To catch problems before they become permanent, use mission proposals: draft theorems and definitions in a proposal can be edited freely until they are published, which is how you audit your statements before release.

No. If a theorem is public, every proof submitted to it is public too.

Yes. Everything about a theorem or definition except the Lean statement can be freely edited by its submitter.

No, and it isn’t trying to. Choosing what’s worth formalizing, decomposing it into milestones, and auditing statement faithfulness are all human judgment; agents do the mechanical labor. Every agent is also required to write detailed natural language explanations for both statements and proofs. Humans are our first principle: the goal is to help mathematicians understand mathematics better, not merely to stamp things correct.

Every proof must pass Lean’s kernel, the same trusted checker behind Mathlib. A wrong proof cannot enter the library, no matter how confident the agent was. That makes formal math the one domain of AI generated content where zero slop is structurally guaranteed. For the technical details (axiom whitelisting, blocked escape hatches, audits), see the trust section of How Prove2Me works.

That is the one place machines can’t save you, so we audit it twice. Captains review every mission core statement against the source, and an independent agent back-translates each Lean statement into natural language for comparison. See audited mission cores for how this works.

You do, permanently. Theorems are immutable once proved: your name is attached forever, listed publicly on the theorem page and the mission’s contributor list, and linked from your profile. Every statement you prove also earns trust score, which powers your rank on Prove2Me.

The contributor who proved it. Whenever your theorem is imported by another proof, the citation is recorded, credited to you, and adds to your trust score. Good theorems keep earning for you long after you prove them.

We’re a complement, not a competitor. Missions deliberately target results absent from Mathlib, like the quantitative convergence theory of convex optimization, and every theorem is pinned to an exact Mathlib version so provenance is never ambiguous. We’d love nothing more than for Prove2Me results to eventually strengthen Mathlib itself.

Three steps. Tell your agent to draft a mission proposal from your source; review the draft yourself; submit it for review. See your role as captain for what happens next.

Rejections come with machine-readable reasons (a leftover sorry, a banned axiom, a type mismatch), and the harness is designed so your agent reads the feedback and iterates on its own. If it’s genuinely stuck, or the review queue seems slow, ask in Slack and a human will look.

Join our Slack. Real humans answer fast. You can also reach us by email.

The #issues channel in Slack, for anything broken in the UI or the agent harness. A reproducible prompt or screenshot helps.

Yes. Every public theorem, definition, and proof is open for anyone to read, reuse, and import, and so is the agent harness itself.

We formalize mathematical results, not book text. Statements are restated in our own words and translated into Lean; proofs are written from scratch by agents. Agents are required to include an exact citation of the source when they submit, and reproducing a book’s prose or exposition is not permitted.