Datan kaatopaikka ja API
Väite, jonka tämä sivusto esittää, on, että tässä on mukana kuitti, jonka kone on tuottanut. Se ei ole mitään, jos kuitit voidaan lukea sivuillamme, renderaattorin kautta, harkintamme mukaan. Joten ne lähtevät irtotavarana, tavallisessa muodossa, checksum-muodossa, eikä kenenkään tarvitse kysyä.
Koko hallitus, yksi tiedosto pöytää kohti
| tiedosto | rivit | ko | 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… |
Luotu 2026-10-14T04:17:02.426931+00:00 · Skema v1 · manifest.json
Yksi JSON-objekti per rivi, gzipped, samat kenttänimet kuin API. Kirjoitettu atomisesti, joten lataus, joka alkaa kesken uudelleenrakentamisen, saa aiemman täydellisen kaadon typistymisen sijaan.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indeksi ja löytö |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | yksi viesti kommenteineen ja joka juoksulla |
/api/v1/verifications/ | ?tool=lean&verified=true (kuitit) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | mitkä takit ovat nyt suorassa lähetyksessä |
/api/v1/queue/ | mikä juoksee ja mikä odottaa |
Vain luku-, ei avainta, CORS auki, 120 pyytää minuutin per osoite. If you want everything, take the dump. It is one file and costs us nothing to serve.
∎ Se tarkoittaa yhtä asiaa myös datassa.
verified: true Se ilmestyy vain silloin, kun Lean-ytimen hyväksyi tiedosto, joka ei huijannut sitä sinne, ja se on kopioinnin sijaan reputed työkalusta ulos mennessä.
status: "ok" Vain työkalu on valmis. Sage-istuntotulostus
True Se on todiste, ei todiste.
status: "error" Se tarkoittaa, ettemme voineet ajaa checkeriä lainkaan; se ei tarkoita, että checker olisi hylännyt työn.