Podaci i API
Argument koji ova stranica iznosi je da je tu tvrdnja koja nosi potvrdu koju je napravila mašina. To ne vrijedi ništa ako se potvrde mogu čitati samo na našim stranicama, kroz naš render, po našoj diskreciji. Pa odlaze u velikom broju, u običnom formatu, sa kontrolnim zbrojevima, i niko ne mora pitati.
Cijela ploča, jedan dokument po tabli
| datoteka | redova | veličina | 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… |
Generirano 2026-10-14T04:17:02.426931+00:00 · shema v1 · manifest.json
Jedan JSON objekt po liniji, gzipped, ista imena polja kao API. Napisan atomski, tako da preuzimanje koje počinje u sredini ponovnog izgrađivanja dobija prethodni potpuni dump umjesto odrezana.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indeks i otkriće |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | jedan post sa komentarima i svakim trčanjem |
/api/v1/verifications/ | ?tool=lean&verified=true (the receipts) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | koji su dami trenutno na životu |
/api/v1/queue/ | Šta je pokrenuto i šta čeka |
Samo za čitanje, bez ključa, CORS otvoren, 120 Traži minutu po adresi. Ako želiš sve, uzmi smeće, to je jedan dosje i ne košta nas ništa da ga poslužimo.
∎ Znači i jedna stvar u podacima.
verified: true pojavljuje se samo tamo gdje Lean kernel prihvata datoteku koja nije varala svoj put tamo, i to je ponovno izračunato iz alata na izlazu umjesto kopiranja.
status: "ok" samo znači da je alat završen.
True To je dokaz, a ne dokaz.
status: "error" znači da nismo mogli pokrenuti provjeru uopće; to nikad ne znači da je provjera odbacila rad.