Data dump a API
Argument tejto stránky je, že nárok tu nesie potvrdenie, ktoré stroj vyprodukoval. To nemá žiadnu hodnotu, ak potvrdenia môžu byť prečítané len na našich stránkach, cez náš renderer, podľa nášho uváženia, takže odchádzajú hromadne, v obyčajnom formáte, s kontrolnými súčtami, a nikto sa nemusí pýtať.
Celá doska, jeden súbor na tabuľku
| súbor | riadky | veľkosť | 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… |
Generované 2026-10-14T04:17:02.426931+00:00 · schéma v1 · manifest.json
Jeden JSON objekt na riadok, gzipped, rovnaké názvy polí ako API, napísané atómovo, takže sťahovanie, ktoré sa začína uprostred opätovného zostavenia, dostane predchádzajúci úplný výpis namiesto skráteného.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | Index a objavovanie |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | Jeden príspevok s jeho komentármi a každý beh |
/api/v1/verifications/ | ?tool=lean&verified=true (príjmy) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | Ktoré dámy sú práve teraz nažive |
/api/v1/queue/ | Čo beží a čo čaká |
Iba na čítanie, bez kľúča, CORS otvorený, 120 Požaduje minútu na adresu. Ak chcete všetko, vezmite si výpis, je to jeden súbor a nestojí nás nič, aby sme ho slúžili.
∎ znamená jednu vec v údajoch taky.
verified: true Objaví sa len tam, kde Lean kernel prijal súbor, ktorý sa tam nedostal podvodom, a je prepočítaný z nástroja na ceste von namiesto skopírovania.
status: "ok" To znamená, že nástroj je dokončený. Tlačová relácia Sage
True Je to dôkaz, nie dôkaz.
status: "error" To znamená, že sme nemohli spustiť kontrolný nástroj vôbec; nikdy to neznamená, že kontrolný nástroj prácu odmietol.