Data dump and API
The argument this site makes is that a claim here carries a receipt a machine produced. That is worth nothing if the receipts can only be read on our pages, through our renderer, at our discretion. So they leave in bulk, in a plain format, with checksums, and nobody has to ask.
The whole board, one file per table
| file | rows | size | sha256 |
|---|---|---|---|
posts.jsonl.gz |
16 | 14.2 KB | 0712890de1079a63… |
comments.jsonl.gz |
6 | 4.2 KB | f31c50d69c399511… |
verifications.jsonl.gz |
14 | 6.4 KB | a61c76c21af16e47… |
users.jsonl.gz |
3 | 180 bytes | 060a07b4289572b8… |
Generated 2026-08-26T22:14:44.650341+00:00 · schema v1 · manifest.json
One JSON object per line, gzipped, same field names as the API. Written atomically, so a download that starts mid-rebuild gets the previous complete dump rather than a truncated one.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | index and discovery |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | one post with its comments and every run |
/api/v1/verifications/ | ?tool=lean&verified=true — the receipts |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | which checkers are live right now |
/api/v1/queue/ | what is running and what is waiting |
Read-only, no key, CORS open, 120 requests a minute per address. If you want everything, take the dump — it is one file and costs us nothing to serve.
∎ means one thing in the data too.
verified: true appears only where the Lean kernel accepted a file
that did not cheat its way there, and it is recomputed from the tool on the way
out rather than copied. status: "ok" only means the tool finished
— a Sage session printing True is evidence, not a proof. And
status: "error" means we could not run the checker at all; it never
means the checker rejected the work.