Submit a proof

Got a proof — solved or a serious attempt — in Coq, Lean, Isabelle, or any system? Drop it here as a .zip and let Claude verify it and publish it to the library. No pull-request wrangling required.

How it works

1

Zip your submission

Bundle your proof files together with a problem.json describing the problem (schema below). Name the zip after your problem, e.g. collatz-attempt.zip.

collatz-attempt.zip └── collatz-attempt/ ├── problem.json ← metadata (see schema) ├── proof.v ← your Coq proof (optional) ├── Proof.lean ← your Lean proof (optional) └── notes.md ← anything else (optional)
2

Drop it into math/new/submissions/ on GitHub

On GitHub, open the math/new/submissions/ folder → Add file → Upload files → drag your zip in → commit. That's the entire "upload" — no local tooling needed.

3

Ask Claude to process it

Start a Claude Code session on the repo and paste the prompt below. Claude will unzip it, try to compile/verify the proof, add the problem to the catalog, file the proof under math/submissions/, and commit.

Extract the newest zip in math/new/submissions/, read its problem.json, and: 1. Verify each proof file if a verifier is available (e.g. run coqc on .v files, lake/lean on .lean files); note the result. 2. Append a new problem object to math/assets/js/data.js using the metadata (set status/verified honestly based on step 1). 3. Move the proof sources into math/submissions/<id>/ and link them from the problem. 4. Delete the processed zip, then commit with a clear message.

problem.json schema

Mirrors the objects in math/assets/js/data.js. Only the first few fields are required.

idrequired — short kebab-case slug, unique. e.g. "my-lemma"
titlerequired — display name.
statusrequired — "solved", "open", or "partial".
categoryrequired — e.g. "Number Theory", "Logic".
statementrequired — plain-language statement of the problem.
latexoptional — a formula (LaTeX-ish; rendered to Unicode).
storyoptional — background / why it's interesting.
by / year / oeisoptional — attribution, date, OEIS A-number.
tagsoptional — array of strings for search.
sourceoptional — { "name": "...", "url": "..." }.
proofsarray of { system, code, verified, runnable?, note? }. system ∈ coq | lean | isabelle | hol-light | agda | builtin | note. Set runnable:true on self-contained Coq to make it live-checkable.
playgroundoptional — { "kind": "coq", "code": "..." } for an editable proof, or { "kind": "logic", "formula": "..." } for the propositional verifier.
Tip: if your proof is a self-contained Coq script, set "runnable": true so visitors can press ▶ Run in Coq and check it in their own browser.

A ready-to-edit example lives at math/new/submissions/EXAMPLE-submission/problem.json. See math/new/README.md for the full contributor + agent guide.

← Back to the problems