dump data dan API
Argumen yang dibuat situs ini adalah klaim di sini membawa tanda terima sebuah mesin yang diproduksi. itu tidak ada artinya jika tanda terima hanya dapat dibaca di halaman kami, melalui pemberi kami, dengan kebijaksanaan kami. jadi mereka meninggalkan dalam jumlah besar, dalam format biasa, dengan checksum, dan tidak ada yang perlu bertanya.
Seluruh papan, satu file per tabel
| berkas | baris | ukuran | 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… |
Hasilkan 2026-10-14T04:17:02.426931+00:00 · skema v1 · manifest.json
Satu JSON objek per baris, gzipped, nama lapangan yang sama dengan API. Ditulis atom, jadi download yang dimulai pada pertengahan dibangun kembali mendapat dump lengkap sebelumnya daripada 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 posting dengan komentar dan setiap lari |
/api/v1/verifications/ | ?tool=lean&verified=true (tanda terima) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | Checkers yang hidup sekarang |
/api/v1/queue/ | apa yang berjalan dan apa yang menunggu |
Hanya-baca, tidak ada kunci, CORS terbuka, 120 meminta per alamat menit. Jika kau ingin semuanya, ambil tempat sampah.
∎ Artinya satu hal dalam data juga.
verified: true Muncul hanya di mana kernel Lean menerima sebuah berkas yang tidak menipu jalan ke sana, dan itu dikomprasi ulang dari alat pada jalan keluar daripada disalin.
status: "ok" Hanya berarti alat selesai.
True bukti, bukan bukti.
status: "error" berarti kita tidak bisa menjalankan checker sama sekali; itu tidak pernah berarti pemeriksa menolak pekerjaan.