Verification

Formal checking and statement meaning are separate questions. Review whether a proposition expresses the intended problem even when both proof checkers pass.

Two kernels

Lean checks each proof against its immutable target and pinned module sources. Hunch then exports its proof expressions and checks them with Nanoda, an independent Rust implementation compiled to WebAssembly. Both run on the account-free verifier origin. Nanoda has no filesystem, network or other host imports.

Lean + Nanoda means both checks passed. Lean alone means the independent check was not completed; its status records not_run, capacity or error. An independent rejection quarantines a new submission. Older proofs retain their historical status until rechecked. Only propext, Classical.choice and Quot.sound are admitted as axioms.

Portable receipts

Download a signed receipt from any checked attempt or module. It binds the exact source, statement, dependency source hashes, checking results and runtime manifest. The signature attests to Hunch’s recorded evidence; local replay checks the proof again.

node hunch.mjs receipt 42 --out receipt-42
node hunch.mjs receipt-check receipt-42
node hunch.mjs receipt-check receipt-42 --local

The CLI contains the trusted public signing key. First replay downloads checksum-pinned runtimes; cached artifacts can be reused. Historical receipts explicitly identify missing runtime fingerprints and independent checks.

Verified dependencies

Choose “Make reusable lemma” on a verified attempt, or run the command below. The resulting named lemma is checked again before other targets can pin its module ID and content hash. Its original proof attribution is retained. Dependency source is embedded in each challenge and rechecked, including the transitive closure. Research links alone do not establish formal dependencies.

node hunch.mjs module from 42 --wait
node hunch.mjs dependencies 16
node hunch.mjs module verify 1

Reusable modules currently allow at most 16 dependencies and 16,000-character proof terms per declaration. Larger proof submissions remain supported up to 64 MiB.

Receipt public keys · Independent checker pins · Lean validation guidance