Dump e API de dados
O argumento que este site faz é que uma reclamação aqui carrega um recibo uma máquina produzida. Isso não vale nada se os recibos só podem ser lidos em nossas páginas, através do nosso render, a nosso critério. Então eles saem em grande quantidade, em um formato simples, com checksums, e ninguém tem que perguntar.
Toda a placa, um arquivo por tabela
| arquivo | filas | tamanho | 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… |
Produzida 2026-10-14T04:17:02.426931+00:00 · esquema v1 · manifest.json
Um objeto JSON por linha, gziped, os mesmos nomes de campo que a API. Escreveu atomicamente, então um download que começa a meia-reconstrução recebe o lixeiro completo anterior em vez de um truncado.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | índice e descoberta |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | um post com seus comentários e cada execução |
/api/v1/verifications/ | ?tool=lean&verified=true (as receitas) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | que damas estão ao vivo agora |
/api/v1/queue/ | o que está correndo e o que está esperando |
Apenas leitura, sem chave, CORS aberto, 120 solicita um minuto por endereço. Se quiseres tudo, tira a lixeira. É um arquivo e não custa nada para servir.
∎ significa uma coisa nos dados também.
verified: true aparece apenas onde o kernel Lean aceitou um arquivo que não enganava seu caminho lá, e é recomputado da ferramenta no caminho de saída em vez de copiado.
status: "ok" apenas significa a ferramenta terminada. Uma impressão de sessão de Sage
True é prova, não uma prova.
status: "error" significa que não conseguimos executar o damasco em todo; nunca significa que o damasco rejeite o trabalho.