A trained transformer, checked from its weights by Lean

24 October 2026, revised 30 October 2026. Thomas Lince (teal-sea).

The result

A one-layer, four-head transformer was trained to add two numbers modulo 113. A Lean theorem says it gets every one of the 12,769 possible inputs right: for each pair (a, b), the correct answer has a strictly larger logit than every other class, so the model returns it.

A 113 by 113 square, one cell per input pair (a, b). Each cell is shaded by the proved answer (a + b) mod 113: dark for 0, light for 112. The shade brightens from the top left to the anti-diagonal, snaps back to dark, and brightens again to the bottom right. Beside it: 12,769 input pairs, every cell proved by Lean's kernel, integer weights at S = 256, exact real softmax. — All 12,769 input pairs. Cell (a, b) is shaded by the answer the theorem proves, (a + b) mod 113, dark for 0 and light for 112. The hard edge is where the sum wraps.

The theorem is TransformerBridge.FinalRaw.raw_model_adds_mod_113. It has no hypotheses and uses only Lean's three standard axioms, propext, Classical.choice and Quot.sound. Lean's kernel checked it, and nanoda, a separately written checker, checked it again from the released objects.

The object is precise: the model built from quantised integer weights at S = 256, with exact real softmax. It is not the floating-point checkpoint those weights were rounded from.

Why softmax is the hard part

Integer weights do not make a transformer an integer computation. Attention runs through softmax, which means exponentials and division, so the logits are real numbers. Running the model and seeing the right answers would prove nothing about those real numbers.

The proof splits the work. Lean checks an integer margin on every input, checks bounds on the tables that calculation uses, and proves those tables come from the raw weights; a real-analysis argument then carries the margin over to the real logits. None of these steps is left as an assumption in the final statement. The status file lists each piece.

The trick: pack, then check

The costly step was proving that two families of tables, TI and TU, really are products of the weight matrices. Each has 916 slots across the four heads, holding vectors of 512 and 113 entries.

Checked one slot at a time, that took about 370 seconds per slot, measured on five slots. All 916 would have taken about 94 hours; that estimate was never run.

The fix is Kronecker substitution. Write a vector as the digits of one large integer, x₀ + x₁ B + x₂ B² + …. If every entry lies between -K and K and 2K < B, two packed integers are equal only if every entry is. So the kernel packs whole rows, pushes them through each head's linear maps, and compares one large integer per row. Checked by whole heads this way, the 17 modules took 200 seconds to compile and 322 to replay.

Two bands. Top: 916 thin ticks in four rows, one row per attention head, the first five bright: the slots accepted one at a time at about 370 seconds each (measured); all 916 extrapolate to about 94 hours (derived, never run). Bottom: eight wide bars, two per head, a long one for TI with 512 entries and a short one for TU with 113 entries, each a whole packed row. 17 modules compiled in 200 seconds and replayed in 322 seconds, measured separately. Below: each row becomes one integer x0 + x1 B + x2 B^2 + ...; with 2K < B, one equal integer forces every entry equal. — Top: the 916 slots, checked one at a time at about 370 seconds each; the first five were run, the rest is the 94-hour estimate. Bottom: the same work as packed whole rows per head, 17 modules compiled in 200 seconds and replayed in 322.

One detail mattered: the kernel packs the original weight lists itself. An earlier version supplied pre-packed numbers and proved they matched the lists, and that proof cost most of what packing saved. Softmax, ReLU and rounding need their own proofs; the method note has the details.

Does it reject wrong data?

Nine controls change the data, for example raising one learned weight by one or changing one table entry by one. The kernel rejects every altered check, and each unchanged twin passes. That shows the checks are not vacuous. It does not show that every changed weight makes the network wrong.

What it does not show

This is a tiny model on a toy task, proved by going through every input. That works for 12,769 pairs and does not scale to a language model. The theorem is about the integer model with exact softmax, not about floating-point execution.

Brian Naughton's certified-grokking already certifies all 12,769 inputs of the same architecture, from a published float32 checkpoint, relying on a trusted Python interval core. Gross et al.'s compact-proofs work gives bounds built from the mechanism, with the gap between floats and reals left open, and Gross's Coq repository has finished brute-force accuracy proofs for trained max-of-two transformers, in floats.

What is added here is the combination: an unconditional theorem about the raw integer weights with real softmax, checked by the kernel end to end, and the whole-head packed check. Neither transformer verification nor Kronecker substitution is new.

How it was built

AI agents trained the model and wrote the proofs. Training used AdamW on 6,384 pairs with 6,385 held out, then margin training; the released weights are the best checkpoint, at epoch 3,044. Thomas Lince directed the project and checked the statements, limits and releases.

An agent's account of why the theorem holds is not evidence; the kernel is. The release also checks the theorem's statement and its axioms, so a proof under the right name with a changed statement or an extra axiom would fail.

Check it yourself

The command block is in VERIFY.md. It needs Linux x86_64, about 30 GB of disk and 16 GiB of memory. In a clean Ubuntu 24.04 container it took 439 seconds and 13.7 GiB at peak, downloads included. It prints the theorem and replays the 20 new modules through Lean's kernel; earlier project and upstream objects are authenticated by hash, not rebuilt. The compiled objects are in the evidence release.

# DOC-START
set -euo pipefail
mkdir -p lean-evidence-r2
cd lean-evidence-r2
base=https://github.com/teal-sea/lean-checked-network/releases/download/transformer-final-raw-evidence-r2
curl -fSL --retry 2 "$base/SHA256SUMS" -o SHA256SUMS
printf '%s  %s\n' 7d5c6116b1e40d627bae043884c1d5ab301f2b098b286a5b08fbc3f2d6140c2c SHA256SUMS | sha256sum -c -
curl -fSL --retry 2 "$base/transformer-final-raw-evidence-r2.tar.zst" -o transformer-final-raw-evidence-r2.tar.zst
grep '  transformer-final-raw-evidence-r2.tar.zst$' SHA256SUMS | sha256sum -c -
tar --zstd -xf transformer-final-raw-evidence-r2.tar.zst
sha256sum --quiet -c SHA256SUMS
cd transformer-final-raw-evidence-r2
curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o "$HOME/lean-evidence-elan-init.sh"
sh "$HOME/lean-evidence-elan-init.sh" -y --default-toolchain none
export PATH="$HOME/.elan/bin:$PATH"
lean --version
bash ./verify.sh --work "$HOME/verify-work"
# DOC-END

A second result: ACAS Xu

A second Lean theorem says ACAS Xu network 1_1, from the VNN-COMP benchmark, satisfies property 1 everywhere in its input box, on TorchLean's exact network semantics: ACASChecked.acas_1_1_property1. alpha-beta-CROWN, outside the trusted base, cut the box into 34 leaves; Lean checks each leaf's arithmetic and that the leaves cover the box. Standard axioms only; nanoda checked 59,489 declarations.

A square with input X1 across and X2 up, each from -0.5 to 0.5, cut into rectangles by the certificate's 33 splits. 31 splits are on X1 or X2 and appear as cell edges; 2 are on X0 and are drawn as a dashed diagonal inside two small cells near X1 = 0, which is why there are 34 leaves and not 32 cells. The cells are smallest near X1 = 0. Leaf 38, with the smallest checked margin, is outlined in teal and labelled 38, at X1 from -0.125 to 0 and X2 from 0 to 0.25. Text: 34 leaves, each checked by Lean's kernel; together they cover the box. — The 34 leaf boxes, projected onto X1 and X2. alpha-beta-CROWN chose 33 splits, 31 on X1 or X2 and two on X0 (dashed). Lean checked every leaf and that together they cover the box. Teal: leaf 38, the smallest checked margin, 0.5698.

Finding that proof took alpha-beta-CROWN 16 seconds. In a pre-release run, compiling the Lean check of its arithmetic took 38 minutes, about 3.5 CPU-hours, and replaying it about 2.8 CPU-hours more. The ONNX-to-Lean importer is audited, not proved, and nothing here covers floating-point execution, other networks or properties, or aircraft. The ACAS README, method and status have the rest.