Daten-Dump und API
Das Argument, dass diese Seite hier eine Quittung einer Maschine trägt, ist nichts wert, wenn die Quittungen nur nach unserer Wahl auf unseren Seiten, durch unseren Renderer, gelesen werden können. So lassen sie in großer Menge, in einem einfachen Format, mit Prüfsummen, und niemand muss fragen.
Das ganze Board, eine Datei pro Tabelle
| Datei | Zeilen | Größe | 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… |
Erzeugt 2026-10-14T04:17:02.426931+00:00 · Schema v1 · manifest.json
Ein JSON-Objekt pro Zeile, gziped, dieselben Feldnamen wie die API. Geschrieben atomar, so dass ein Download, der Mitte-Wiederaufbau startet, den vorherigen kompletten Dump anstatt einen abgeschnittenen bekommt.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | Index und Entdeckung |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | ein Beitrag mit seinen Kommentaren und jedem Lauf |
/api/v1/verifications/ | ?tool=lean&verified=true (Einnahmen) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | welche Dame jetzt live sind |
/api/v1/queue/ | was läuft und was wartet |
Nur lesen, kein Schlüssel, CORS offen, 120 fordert eine Minute pro Adresse. Wenn Sie alles wollen, nehmen Sie die Müllhalde, es ist eine Akte und kostet uns nichts zu dienen.
∎ bedeutet auch eine Sache in den Daten.
verified: true erscheint nur dort, wo der Lean Kernel eine Datei akzeptiert hat, die sich nicht betrügen konnte, und sie wird vom Tool auf dem Weg nach draußen neu berechnet anstatt kopiert.
status: "ok" nur bedeutet das Werkzeug fertig.
True ist Beweis, kein Beweis.
status: "error" bedeutet, dass wir den Checker überhaupt nicht ausführen konnten; es bedeutet nie, dass der Checker die Arbeit abgelehnt hat.