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.<p>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:<p>- "The FFN computes the Bayesian update" [2]. Axiom.<p>- "Attention routes neighbors correctly" [3]. Axiom.<p>- "BP converges" [4]. Axiom, with a comment saying it's "not provable in general."<p>- The no-hallucination corollary [5]. Axiom.<p>The paper says "formally verified against standard mathematical axioms" about all of these. They are not verified. They are assumed.<p>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.<p>Final count across all five repos: 65 axioms, 5 sorries, 149 theorems.<p>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."<p>[1] <a href="https://github.com/gregorycoppola/sigmoid-transformer-lean/blob/28e1918/SigmoidTransformerLean/GeneralTheorem.lean#L157" rel="nofollow">https://github.com/gregorycoppola/sigmoid-transformer-lean/b...</a><p>[2] <a href="https://github.com/gregorycoppola/transformer-bp-lean/blob/767a498/TransformerBPLean/Preliminaries.lean#L309" rel="nofollow">https://github.com/gregorycoppola/transformer-bp-lean/blob/7...</a><p>[3] <a href="https://github.com/gregorycoppola/transformer-bp-lean/blob/767a498/TransformerBPLean/Preliminaries.lean#L266" rel="nofollow">https://github.com/gregorycoppola/transformer-bp-lean/blob/7...</a><p>[4] <a href="https://github.com/gregorycoppola/transformer-bp-lean/blob/767a498/TransformerBPLean/Preliminaries.lean#L334" rel="nofollow">https://github.com/gregorycoppola/transformer-bp-lean/blob/7...</a><p>[5] <a href="https://github.com/gregorycoppola/transformer-bp-lean/blob/767a498/TransformerBPLean/TreeCorollary.lean#L27" rel="nofollow">https://github.com/gregorycoppola/transformer-bp-lean/blob/7...</a><p>[6] <a href="https://github.com/gregorycoppola/godel/blob/bc1d138/Godel/ORDecomposition.lean#L60" rel="nofollow">https://github.com/gregorycoppola/godel/blob/bc1d138/Godel/O...</a><p>[7] <a href="https://github.com/gregorycoppola/sigmoid-transformer-lean/blob/28e1918/SigmoidTransformerLean/Preliminaries.lean#L20" rel="nofollow">https://github.com/gregorycoppola/sigmoid-transformer-lean/b...</a>