Three linked pieces of work: a framework for treating intelligence as constrained search, a complete implementation of chain-of-thought reasoning whose every step a proof assistant re-checks, and a first machine-checked case study in combinatorics. Everything below ships with reproducible artifacts and SHA-256 anchors.
Headline result
The van der Waerden number W(3,3) = 27 — machine-checked, both directions
Classical in value (Chvátal, 1970); the contribution is the certificate. The full determination reduces to a single Lean 4 biconditional over 3-colourings, whose entire human audit surface is two short definitions and the kernel:
theoremvdw33_characterization (n : Int) :
(∀ c, IsColoring n c → ¬ APfree n c) ↔ 27 ≤ n
Lean 4 · no sorry, no axiom382,964-step certificatefull 21,048-node searchtwo independent checkers
Written to a strict evidence discipline: every claim is tagged as Lean-checked, tested, measured, or a labelled conjecture — nothing is asserted beyond what the shipped artifacts support.
FrameworkL. Avent · 2026
Avent's Razor: Intelligence as Constrained Search #
Classical accounts measure intelligence by descriptive parsimony — the shortest program consistent with observation. This paper proposes an operational complement: measure a reasoning system by the constraints it can enforce during search, because an enforced constraint eliminates candidates before they are paid for, and because enforcement — unlike insight — is mechanically checkable. The framework has a quantitative face (constraint capacity, the bits of search space a constraint system deletes) and an architectural face (make invalid reasoning states unrepresentable, so untrusted generators can only search inside the valid envelope). It is supported exclusively by artifacts that exist: a complete verified-reasoning implementation, a measured capacity-versus-speedup relationship over 300 enumerable instances, language models operating the loop through a typed gate, and the W(3,3) case study. The strong exponential form of the razor is stated as a conjecture with a specified experiment.
Verified Chain-of-Thought for Finite-Domain Constraint Reasoning #
A complete, running implementation of the verified chain-of-thought loop with no mock components. Untrusted proposers — language models or a deterministic engine — construct reasoning steps in a strongly-typed step language; an 18-rule kernel computes every conclusion (proposers can never state one); completed derivations are re-checked from their serialized bytes by two independent checkers (Python, and a zero-dependency parallel Rust verifier held to exact verdict agreement over 2,197 certificates by differential fuzzing); and each accepted chain is compiled to a Lean 4 file in which every step is re-proved from exactly its cited premises. Frontier and mid-tier language models operate the loop through a typed gate; the paper reports both sessions unedited.
A Proof-Assistant-Checked Determination of the van der Waerden Number W(3,3) #
A Lean 4 kernel-checked determination of the 3-colour van der Waerden number: W(3,3) = 27. Both directions are machine-checked from first principles on a 2-core machine — an explicit AP-free 3-colouring of [1..26], and a refutation for [1..27] compiled from a single 382,964-step derivation that covers the entire 21,048-node search, with no clause learning, no symmetry breaking, and no trusted solver anywhere in the chain. The derivation is re-verified from its bytes by two disjoint checkers, then compiled to 336 Lean shard modules plus a master theorem in which every step is re-proved from its cited premises, and finally combined into one biconditional over colouring functions. To a documented search, no proof-assistant-checked determination of any 3-colour van der Waerden number existed previously.
van der Waerdensharded Lean compilationwhole-tree certificatereproducible
The certificate package contains the proof object, all Lean modules, the witness, the combined theorem, and a full checksum manifest. The proof object is the stable anchor; the Lean files pin this specific compiled rendering.
# 1. the download is the file this page publishes$ sha256sum vdw33-certificates.zip
# 2. every file inside matches the shipped manifest$ unzip -q vdw33-certificates.zip -d vdw33 && cd vdw33
$ sha256sum -c SHA256SUMS.txt
# 3. all 339 Lean modules as one digest$ cd lean_pkg && LC_ALL=C sha256sum *.lean | sha256sum
a1b660ebe8924587d929585548c86e918c52c3ebbe78a08783062ae78c1035bc
Step 2 reports one improperly-formatted line: the manifest ends with the aggregate from step 3, which names no file. The 339 modules are the master theorem, both directions, and the 336 shards the refutation is split across.
Toolchain: Lean 4.10.0 (core, no mathlib), CPython 3.11, rustc 1.95, on a 2-core / 7 GiB machine. The commands above establish that the files are the ones published here; re-running the proofs from source needs that toolchain, and each paper's appendix and the package README give the steps.