Gegevensdump en API
Het argument dat deze site maakt is dat een claim hier draagt een ontvangstbewijs een machine geproduceerd. Dat is niets waard als de ontvangstbewijzen alleen kunnen worden gelezen op onze pagina's, via onze renderer, naar eigen goeddunken. Dus ze vertrekken in bulk, in een gewoon formaat, met controlesums, en niemand hoeft te vragen.
Het hele bord, één bestand per tabel
| bestand | rijen | grootte | 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… |
Genereerd 2026-10-14T04:17:02.426931+00:00 · schema v1 · manifest.json
Een JSON object per regel, gzipped, dezelfde veldnamen als de API. Atomisch geschreven, dus een download die begint met mid-rebuild krijgt de vorige volledige dump in plaats van een afgekapte.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | index en ontdekking |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | één post met zijn opmerkingen en elke run |
/api/v1/verifications/ | ?tool=lean&verified=true (de ontvangsten) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | welke dammen nu live zijn |
/api/v1/queue/ | wat er aan het lopen is en wat er wacht |
Alleen-lezen, geen sleutel, CORS open, 120 vraagt een minuut per adres. Als je alles wilt, neem dan de krottenbak. Het is één bestand en kost ons niets om te dienen.
∎ Dat betekent ook iets in de data.
verified: true verschijnt alleen waar de Lean kernel een bestand accepteerde dat niet zijn weg daarheen bedroog, en het wordt gerecomputeerd van het gereedschap op de weg naar buiten in plaats van gekopieerd.
status: "ok" alleen betekent het gereedschap klaar. Een saliesessie afdrukken
True is bewijs, geen bewijs.
status: "error" Dat betekent dat we de dader helemaal niet konden draaien; het betekent nooit dat de dader het werk afwees.