Data dump et API
L'argument que ce site fait est qu'une réclamation ici porte un reçu une machine produite. Cela ne vaut rien si les reçus ne peuvent être lus sur nos pages, par notre rendeur, à notre discrétion. Donc ils partent en vrac, dans un format simple, avec des comptes de chèques, et personne n'a à demander.
La carte entière, un fichier par table
| fichier | lignes | Taille | 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… |
Produit 2026-10-14T04:17:02.426931+00:00 · schéma v1 · manifest.json
Un objet JSON par ligne, gzipped, les mêmes noms de champs que l'API. Ecrit atomiquement, donc un téléchargement qui commence à mi-reconstruction obtient la décharge complète précédente plutôt qu'une tronquée.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indice et découverte |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | un billet avec ses commentaires et chaque course |
/api/v1/verifications/ | ?tool=lean&verified=true (les recettes) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | qui sont en vie en ce moment |
/api/v1/queue/ | ce qui court et ce qui attend |
En lecture seule, sans clé, CORS ouvert, 120 demande une minute par adresse. Si vous voulez tout, prenez le vide. C'est un seul fichier et ne nous coûte rien à servir.
∎ signifie une chose dans les données aussi.
verified: true apparaît seulement là où le noyau Lean a accepté un fichier qui n'a pas triché son chemin là, et il est recompilé à partir de l'outil sur le chemin de sortie plutôt que copié.
status: "ok" seulement signifie l'outil terminé.
True est une preuve, pas une preuve.
status: "error" Cela signifie que nous ne pouvions pas faire fonctionner le vérificateur du tout; cela ne signifie jamais que le vérificateur a rejeté le travail.