მონაცემთა გადატანა და API
The argument this site makes is that a claim here carries a receipt a machine produced. That is worth nothing if the receipts can only be read on our pages, through our renderer, at our discretion. So they leave in bulk, in a plain format, with checksums, and nobody has to ask.
მთელი მაგიდა, ერთი ფაილი თითო მაგიდაზე
| ფაილი | რიგი | ზომა | 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 (the receipts) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | რომელი ფიგურაა აქტიური ამ მომენტში |
/api/v1/queue/ | რა არის მოქმედებაში და რა ელოდება |
Read-only, no key, CORS open, 120 თჟკა მთნსრა ნა ადპვჟ. If you want everything, take the dump. It is one file and costs us nothing to serve.
∎ means one thing in the data too.
verified: true თავს იჩენს მხოლოდ მაშინ, როდესაც Lean kernel- მა მიიღო ფაილი, რომელიც არ იყო შეცდომაში შეყვანილი და ის გადაითვლება პროგრამიდან გამოსვლისას, ვიდრე კოპირებისას.
status: "ok" მხოლოდ ნიშნავს, რომ ინსტრუმენტი დასრულდა. Sage- ის სეანსის ბეჭდვა
True is evidence, not a proof.
status: "error" ნიშნავს რომ ვერ შევძელით მოდულის გაშვება; ეს არასდროს ნიშნავს რომ მოდული არ დააკმაყოფილა სამუშაო.