Datadump og API
Argumentet denne siden gjør er at et krav her bærer en kvittering en maskin produsert. det er ikke verdt noe hvis kviteringene bare kan leses på sidene våre, gjennom vår gjengiver, etter vårt skjønn. så de etterlater bulk, i et vanlig format, med sjekksum, og ingen trenger å spørre.
Hele brettet, en fil per tabell
| fil | rader | størrelse | 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… |
Generert 2026-10-14T04:17:02.426931+00:00 · skjema v1 · manifest.json
Ett JSON- objekt per linje, gzipped, samme feltnavn som API. Skriftlig atomisk, så en nedlasting som starter midtre- oppbygging får den forrige fullstendige dumpen i stedet for en avkuttet.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indeks og oppdagelse |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | en post med kommentarer og hver kjøring |
/api/v1/verifications/ | ?tool=lean&verified=true (inntekter,) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | hvilke brikker er i live akkurat nå |
/api/v1/queue/ | hva kjører og hva venter |
Skrivebeskyttet, ingen nøkkel, CRS åpen, 120 forespørsler et minutt per adresse. Hvis du vil ha alt, ta dumpen. Det er en fil og koster oss ingenting å tjene.
∎ betyr en ting i dataene også.
verified: true vises bare der Lean kjernen akseptert en fil som ikke fusker sin vei der, og det er recomputed fra verktøyet på vei ut i stedet for kopiert.
status: "ok" Bare betyr at verktøyet er ferdig. En Sage- økt utskrift
True er bevis, ikke et bevis.
status: "error" betyr at vi ikke kunne kjøre sjekken i det hele tatt, det betyr aldri at sjekker avviste arbeidet.