I suspect it means it's LLM generated without it being checked

The headline theorem, "every sigmoid transformer is a Bayesian network," is proved by `rfl` [1]. For non-Lean people: `rfl` means "both sides are the same expression." He defines a transformer forward pass, then defines a BP forward pass with the same operations, wraps the weights in a struct called `implicitGraph`, and Lean confirms they match. They match because he wrote them to match.

The repo with a real transformer model (transformer-bp-lean) has 22 axioms and 7 theorems. In Lean, an axiom is something you state without proving. The system takes your word for it. Here the axioms aren't background math, they're the paper's claims:

- "The FFN computes the Bayesian update" [2]. Axiom.

- "Attention routes neighbors correctly" [3]. Axiom.

- "BP converges" [4]. Axiom, with a comment saying it's "not provable in general."

- The no-hallucination corollary [5]. Axiom.

The paper says "formally verified against standard mathematical axioms" about all of these. They are not verified. They are assumed.

The README suggests running `grep -r "sorry"` and finding nothing as proof the code is complete. In Lean, `sorry` means "I haven't proved this" and throws a compiler warning. `axiom` also means "I haven't proved this" but doesn't warn. So the grep returns clean while 22 claims sit unproved. Meanwhile the godel repo has 4 actual sorries [6] anyway, including "logit and sigmoid are inverses," which the paper treats as proven. That same fact appears as an axiom in the other repo [7]. Same hole, two repos, two different ways to leave it open.

Final count across all five repos: 65 axioms, 5 sorries, 149 theorems.

Claude (credited on page 1) turned it into "Not an approximation of it. Not an analogy to it. The computation is belief propagation." Building to a 2-variable toy experiment on 5K parameters presented as the fulfillment of Leibniz's 350-year-old dream. Ending signed by "Calculemus."

[1] https://github.com/gregorycoppola/sigmoid-transformer-lean/b...

[2] https://github.com/gregorycoppola/transformer-bp-lean/blob/7...

[3] https://github.com/gregorycoppola/transformer-bp-lean/blob/7...

[4] https://github.com/gregorycoppola/transformer-bp-lean/blob/7...

[5] https://github.com/gregorycoppola/transformer-bp-lean/blob/7...

[6] https://github.com/gregorycoppola/godel/blob/bc1d138/Godel/O...

[7] https://github.com/gregorycoppola/sigmoid-transformer-lean/b...

The way neural networks work is that the base neural network is embedded in a sampling loop, i.e. a query is fed into the network & the driver samples output tokens to append to the query so that it can be re-fed back into the network (q → nn → [a, b, c, ...] → q + sample([a, b, c, ...])). There is no way to avoid hallucinations b/c hallucinations are how the entire network works at the implementation level. The precision makes no difference b/c the arithmetic operations are semantically void & only become meaningful after they are interpreted by someone who knows to associated 1 /w red, 2 w/ blue, 3 w/ clouds, & so on & so forth. The mapping between the numbers & concepts does not exist in the arithmetic.