داده‌های فشرده و API
استدلال اين سايت اينه که ادعاي اينجا يه دريافتي رو به همراه داره که توسط يه ماشين توليد شده. اين ارزشي نداره اگه دريافت ها فقط بتونند در صفحات ما خوانده بشن، از طريق نمايشگر ما، به اختيار ما. پس اونها به صورت انبوه، در قالب ساده، با چک‌سام‌ها، خارج ميشن و هيچکس نبايد ازشون بپرسه.
کل تخته، یک پرونده در هر جدول
| پرونده | ستونها | اندازه | 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… |
ایجاد شده 2026-10-14T04:17:02.426931+00:00 · طرحواره v1 · manifest.json
یک شیء JSON در هر خط، gzipped، همان نام‌های حوزه مانند API. به صورت اتمی نوشته شده، بنابراین یک بارگیری که در میانه بازسازی شروع می‌شود، به جای یک قطعه قطعه، دمپ کامل قبلی را دریافت می‌کند.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | نمایه و کشف |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | يک پست با نظراتش و هر يک از راننده ها |
/api/v1/verifications/ | ?tool=lean&verified=true (.) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | کدام شطرنج بازها الان زنده هستند |
/api/v1/queue/ | چه چیزی در حال اجراست و چه چیزی منتظر است |
فقط خواندني، بدون کلید، CORS بازه 120 يه دقيقه براي هر آدرس درخواست ميکنه اگه همه چيز رو ميخواي، اين يه پرونده ي يه باريه و هيچ هزينه اي براي ما نداره
∎ يعني يه چيز ديگه هم در داده ها هست
verified: true فقط در جایی ظاهر می‌شود که هسته Lean یک فایل را پذیرفت که در آنجا تقلب نکرده و از ابزار در راه خروج به جای کپی کردن دوباره محاسبه می‌شود.
status: "ok" فقط به این معنی است که ابزار تمام شده است.
True اين يه مدرکه نه يه اثبات
status: "error" به این معنی که ما نمی‌توانیم چکر را اجرا کنیم؛ هیچ وقت به این معنی نیست که چکر کار را رد کرده است.