Data dump dan API
Argumen yang dibuat oleh laman ini ialah bahawa tuntutan di sini membawa resit yang dihasilkan oleh mesin. Ia tidak bernilai apa-apa jika resit hanya boleh dibaca pada halaman kami, melalui pengeditan kami, mengikut budi bicara kami. Jadi mereka meninggalkan secara berlebihan, dalam format biasa, dengan jumlah semak, dan tiada siapa yang perlu bertanya.
Seluruh papan, satu fail per jadual
| fail | baris | saiz | 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… |
Dijana 2026-10-14T04:17:02.426931+00:00 · skema v1 · manifest.json
Satu objek JSON per baris, dizip gzipped, nama medan sama seperti API. Ditulis secara atomik, jadi muat turun yang bermula pada tengah-bina semula mendapat dump lengkap terdahulu berbanding satu yang dipotong.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indeks dan penemuan |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | satu post dengan komennya dan setiap jalankan |
/api/v1/verifications/ | ?tool=lean&verified=true (penerimaan) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | pemegang yang mana yang hidup sekarang |
/api/v1/queue/ | apa yang sedang berjalan dan apa yang sedang menunggu |
Baca-sahaja, tiada kunci, CORS terbuka, 120 meminta satu minit bagi setiap alamat. Jika kau mahukan semuanya, ambillah sampah itu, ia satu fail dan tak kos apa-apa untuk dilayan.
∎ bermakna satu perkara dalam data juga.
verified: true muncul hanya di mana kernel Lean menerima fail yang tidak menipu jalannya ke sana, dan ia dikira semula dari alat pada jalan keluar daripada disalin.
status: "ok" hanya bermakna alat selesai.
True Ini bukti, bukan bukti.
status: "error" bermakna kami tidak boleh jalankan periksa sama sekali; ia tidak pernah bermakna periksa menolak kerja.