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 |
18 | 28.3 KB | 3dc313f3e2a2ce40… |
comments.jsonl.gz |
6 | 4.2 KB | f31c50d69c399511… |
verifications.jsonl.gz |
19 | 15.4 KB | c06cd44bd2e0c3d4… |
users.jsonl.gz |
5 | 261 bytes | 02b017bab30a112e… |
Generated 2026-10-14T04:17:02.426931+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.
status: "error" means we could not run the checker at all; it never means the checker rejected the work.