The Mathematics of Software ChangeExploring consistency, migration, and reconstruction through Algebraic Architecture Theory.Sep 24, 2026·25 min read·35
Atlas Theorem: How Far Can You Zoom Out?Four refutations, 13,000 lines of Lean, and a proof that resolution doesn't change the diagnosisAug 8, 2026·24 min read·72
Taming a 40-Minute Lean CI: Three Rounds, Three Wrong SuspectsOur Lean 4 + mathlib project used to spend 41 minutes in CI on every single PR. Today, the worst case — rebuilding the heaviest files from scratch — takes 12 minutes, and an ordinary PR finishes in a Aug 2, 2026·21 min read·148
The SAGA Comparison Theorem Preprint Is Out: Two Rulers, One ReadingTL;DR We have published a paper on Zenodo (DOI: 10.5281/zenodo.21603761, CC BY 4.0) that formalizes the "locally correct, globally broken" phenomenon of software architecture as mathematics, proves iJul 27, 2026·12 min read·29
SAGA's Cape of Good Hope: The One Cent That Cohomology CaughtTL;DR This is the sequel to the SAGA theorem article. Last time, I gave the "locally correct, globally broken" phenomenon a theorem, proved in Lean 4. This time I took that theorem out into the real Jul 18, 2026·16 min read·38
The Rising Sea of Software Engineering — Rebuilding the Discipline on Algebraic GeometryAI now writes code faster than humans can review it. That is not a prediction; it is the daily experience of most engineering teams. And here is the other daily experience: no matter how much you inveJul 7, 2026·15 min read·120
The SAGA Theorem: The Day Software Architecture Became Genuine Algebraic GeometryTL;DR Every module passes review, yet the system as a whole is broken. This "locally correct, globally inconsistent" phenomenon has a name in mathematics: cohomology, specifically H^1. AAT (AlgebraiJul 2, 2026·19 min read·300
