v3.0.1

blam 3.0.1 changes no interface. It republishes the README with what has been established since 3.0.0, chiefly a 162-bit self-interpreter, and corrects how the busy-beaver values are credited.

A 162-bit self-interpreter

BLC's smallest known self-interpreter is now 162 bits, six below Sean Palmer's 168 (tromp/AIT's int.lam). On the way it went through a 165 (Codex's design), which computes the skip once, on the whole stream, before dispatch.

• What changed. The 162 keeps the 165's recursion and its second-bit stage and replaces the reader. The reader applies the input stream to the identity, so after a 0 the first cell selects its own tail as the zero branch. After a 1 it reopens the stream, hands the tail to the continuation, and skips the variable's code with the second-bit stage as an erased third operand. That stage is now the reader's last operand instead of a let.
• Proved. Lean proves it correct for every closed program (selfint_contract162 in lean/Blc/Selfint162.lean). It proves the 165 and Palmer's 168 the same way. An independent adversarial review re-derived the contract and the size.
• Checked. It passes the self-interpreter battery (667 programs pass, 1 skipped, none fail) and the extended battery through 21 bits (3,341 pass, 2 skipped, none fail). Its let structure is the unique minimum up to three cuts. Its βη component through slack 24 (12,024,847 terms) holds nothing smaller.
• Universal machines. The same reader gives 172 bits (non-strict) and 184 (strict), against Tromp's 178 and 190. Both of Tromp's wirings follow from a self-interpreter's contract, so Lean proves U (⌜M⌝ ++ N) →β* M N for every closed M for all six machines around the 162, the 165 and the 168, Tromp's own uni.lam included. Each is pinned to its wire (lean/Blc/Universal.lean). blam selfint wiring --strict (lab) now runs a seventh strictness probe, Codex's counterexample to base environments that apply the parser; battery.py --strict runs the same seven.
• Lower bounds. Every self-interpreter has at least 37 bits, by a handwritten proof that two independent reviews checked (global floor). At least 27 bits are kernel-checked in Lean.
• How it was found. Codex, refuting a step in Claude's proof that the 165's reader was optimal, built a 44-bit reader as a counterexample. Spliced into the 165, it gave a correct 166. blam golf letopt then moved the second-bit stage into the reader's operand slot, which was Grok's idea, and that gave 162.

The full record is docs/classical/self-interpreter/interpreter.md.

The rest of tromp/AIT

The golf branch, sent upstream as tromp/AIT#13, shrinks 40 programs by 1,159 bits in all:

• the IOCCC BLC8 universal machine goes from 43 bytes to 38 (strict) and 36 (non-strict);
• the bytewise BLC2 machine goes from 500 bits to 390;
• the constant in KP(x) ≤ KO(x) + c goes from 615 to 540;
• the symmetry-of-information constants drop by up to 132 bits;
• Loader's number fits in 1781 bits.

The 162's reader is in all six programs that share it: int.lam, uni.lam, int4, ko2kp, nf and pairup_Kp. docs/classical/golf.md records how each one was checked.

Correction

The 3.0.0 README said the census establishes BBλ(33) = 1,812, BBλ(34) = 327,686 and BBλ(35) = 38,127,987,424,941. These are Tromp's values (OEIS A333479). The census and blam's kernel-checked adjudications confirm them independently. The README also no longer quotes the census bound BBλ(41) ≥ 38,127,987,424,947. It is true, but A333479 already lists a(36) = 5·2²⁵⁶ + 6, which makes it uninformative.

Found and checked with Claude (Anthropic), Codex (OpenAI), Grok (xAI) and Gemini (Google).