Απορρίψεις δεδομένων και 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 ανά γραμμή, gziped, ίδια ονόματα πεδίου με το API. Γραμμένο ατομικά, έτσι ένα κατέβασμα που ξεκινά τα μέσα-επανοικοδόμηση παίρνει την προηγούμενη πλήρη χωματερή αντί ένα trunated ένα.
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/ | Τι τρέχει και τι περιμένει |
Μόνο διάβασμα, κανένα κλειδί, COS ανοιχτό, 120 ζητάει ένα λεπτό ανά διεύθυνση. Αν τα θέλετε όλα, πάρτε το σκουπίδι.
∎ Σημαίνει και ένα πράγμα στα δεδομένα.
verified: true εμφανίζεται μόνο όταν ο πυρήνας Lean δέχθηκε ένα αρχείο που δεν εξαπατούσε το δρόμο του εκεί, και επανατοποθετείται από το εργαλείο κατά τη διέξοδο αντί αντιγραφεί.
status: "ok" Ένα φασκόμηλο εκτύπωση συνεδρίας
True είναι απόδειξη, όχι απόδειξη.
status: "error" Αυτό δεν σημαίνει ότι ο ελεγκτής απέρριψε την εργασία.