Ariadne: The Mathematics of Refactoring in the Age of AI“I want to add multilingual support to the site.” It sounds like a small change: add translation files and switch the strings shown on screen. Then you switch to English, and the return button disappeOct 4, 2026·21 min read·59
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·151
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
