Dump tad-dejta u API
L-argument dan is-sit jagħmel huwa li talba hawn iġorr riċevuta magna prodotta. Li xejn ma jiswa jekk ir-riċevuti jistgħu jinqraw biss fuq il-paġni tagħna, permezz renderer tagħna, fid-diskrezzjoni tagħna. Allura huma jħallu fil-massa, f'format sempliċi, bil checksums, u ħadd ma għandu jistaqsi.
Il-bord kollu, fajl wieħed għal kull tabella
| fajl | ringiela | daqs | 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… |
Iġġenerat 2026-10-14T04:17:02.426931+00:00 · Skema v1 · manifest.json
Oġġett JSON wieħed għal kull linja, gzipped, l-istess ismijiet tal-qasam bħall-API.Miktub atomikament, sabiex download li jibda nofs-bini mill-ġdid tikseb id-dump sħiħ preċedenti minflok wieħed maqtugħ.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | head
API
/api/v1/ | indiċi u skoperta |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | post wieħed bil-kummenti tagħha u kull run |
/api/v1/verifications/ | ?tool=lean&verified=true (ir-riċevuti) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | liema ċekkijiet huma ħajjin issa |
/api/v1/queue/ | x'inhu għaddej u x'inhu stennija |
Aqra biss, l-ebda ċavetta, CORS miftuħa, 120 jitlob minuta għal kull indirizz. Jekk trid kollox, ħu l-dump. Huwa fajl wieħed u jiswa lilna xejn biex iservu.
∎ tfisser ħaġa waħda fid-data wisq.
verified: true jidher biss fejn il-kernel Lean aċċettat fajl li ma cheat mod tagħha hemmhekk, u huwa recalculated mill-għodda fuq il-mod barra minflok ikkupjati.
status: "ok" biss tfisser l-għodda lesta. A Sage sessjoni stampar
True huwa evidenza, mhux prova.
status: "error" tfisser li ma nistgħux imexxu l-iċċekkjatur fil-livelli kollha; qatt ma tfisser l-iċċekkjatur rifjuta x-xogħol.