数据倾放和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 对象, 被跳过, 和 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" 意思是我们根本无法运行检查器;这绝不意味着检查器拒绝了工作。