Hodge Certificate Checker, Search, Export & Visualizer
Lean 4.28.0 + Mathlib
WASM VM (45 KB)
v1 Shipped
Project ID: f4e10742-bd72-442a-88b0-b1a915a3f51b
Description: Hodge VM — checking, searching and exporting hodge.computer certificates in the browser
Created: 2026-10-20T22:19:51.544517
Status: IN_PROGRESS
Owner: J (google-oauth2|112348243083922428340)
RequestProject/Hodge/ holds the verbatim repository contract (HodgeComputer.Verify, Spec.lean), a computable sparse-polynomial checker over ℚ (runChecks, Check.lean / Oracle.lean, runs with #eval), and the theorem HodgeOracle.check_sound: if every Boolean check passes, Verify holds for the interpreted polynomials. Proved without sorry; axioms propext, Classical.choice, Quot.sound.vm/, 45,563 bytes, sha256 777b4204a1249cc51ce836d5c4740bb23b25ff1c1b50dec796f212aedd15c6ab): sparse polynomials in six variables with exact big-rational coefficients, instructions LOADPOLY, ADD, SUB, MUL, SMUL, POW, PDERIV, DIR, DIV, EQ, ISZERO, ISHOM, DEG, EVALMOD, REPORT, … (see spec/isa.md), step and memory limits with clear errors, MiniLean report convention (claim k → (k,1) / (k,0)).fractions checker agree on all golden vectors.lake build builds Spec, SPoly, Check, Oracle, Golden, Literal (a few minutes once Mathlib is cached). The 41 per-instance certificate modules (RequestProject/Hodge/Instances/) are a separate library HodgeInstances, not in the default build, so a slow instance can never break the core build.
Instances are built one at a time, smallest first, with hodge-vm/tools/build_instances.sh [timeout] [Module ...]; results go to tests/instance-build-status.tsv. Current status: 39 of 41 kernel-checked (14 s – 386 s each); Contact46006 (147 KB) and M3Coupled (190 KB) are not kernel-checked yet. Failures and timeouts are recorded, not fatal.
#print axioms on the witness theorem gives exactly propext, Classical.choice, Quot.sound for all 39 kernel-checked instances — 34 via tools/axiom_audit.sh and the 5 largest one module per run via tools/audit_one.sh.
No native_decide anywhere in anything described as proved — it adds an axiom the repository's verifier rejects. The core soundness theorem HodgeOracle.check_sound uses propext, Classical.choice, Quot.sound only.
| Item | Result |
|---|---|
| Witnesses available | 41 of 62 accepted instances carry a witness.json; 21 are accepted by existence proofs with no finite witness to check; 16 instances are open |
| Lean oracle (M1) | 41/41 pass all 5 checks, all 123 negative controls rejected |
| VM (M2) | 0 disagreements WASM / JS / Lean / Python on 41 witnesses |
| Coprimality | Established for all 41 witnesses |
| Search, accepted ansatz (M4) | Re-derives 41/41 |
| Search, graded ansatz | 39/41; Klein-Hesse and Klein-Rational exceed 1,500-unknown limit |
| Open instances | 16 instances × 4 denominators, graded ansatz, ≤1,500 unknowns: no candidate — not evidence of nonexistence |
| Export dry run (M5) | Generated Solution.lean compiled with local Lean against the copied contract, clean axioms |
| Edge (Appendix A) | E1, E2 (41, 0 disagreements), E4, E5 (graded search via edge units recovers 39/41) pass on the Node listener |
# Serve the hodge-vm folder with any static server python3 -m http.server 8000 # Then open http://localhost:8000/index.html # Works from file:// as well (data and wasm are sharded JS files loaded on demand)
# studio/studio-hodge.js + studio/hodge.claims.mlean # Patch with tools/patch_studio.py (spec/studio.md)
node edge/node-server.mjs # Build a Workers bundle with python3 tools/make_hodge_edge.py
bash vm/build.sh # Rust, wasm32-unknown-unknown python3 tools/make_wasm_shards.py
lake build # Core only lake build RequestProject.Hodge.Instances.FermatQ2 # One instance hodge-vm/tools/build_instances.sh 1800 # All instances in background
node tests/test_vm.js node tests/test_search.js node tests/test_claims.js node tests/test_page.js # and --file node tests/test_studio.js node tests/test_edge.mjs # --graded for E5 bash tests/export_dryrun_all.sh python3 tools/chunk_check.py
Every page is ≤ 20,000 estimated tokens (3 characters per token; checked by tools/chunk_check.py). The two largest instances are split into part modules P1…P5 to fit. INDEX.md lists each page with its size, sha256, dependencies and summary. tasks/ holds task cards. tools/make_bundles.py concatenates whole pages; tools/unpack_reply.py applies a reply after checking checksums.