#lean

Articles tagged with #lean

Uncharted Waters: Thirteen Rules for Not Trusting an AI's Proofs
Seven theorems in fifteen days, one refutation, ~104 cycles of Lean — and the ship's log of why nothing sank
Aug 16, 202618 min read33
Semantic Geometry of Architecture
The Meaning of Software Forms a Space
Aug 11, 202622 min read96
Atlas Theorem: How Far Can You Zoom Out?
Four refutations, 13,000 lines of Lean, and a proof that resolution doesn't change the diagnosis
Aug 8, 202624 min read50
Taming a 40-Minute Lean CI: Three Rounds, Three Wrong Suspects
Our 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, 202621 min read138
SAGA's Cape of Good Hope: The One Cent That Cohomology Caught
TL;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, 202616 min read29
The Rising Sea of Software Engineering — Rebuilding the Discipline on Algebraic Geometry
AI 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 inve
Jul 7, 202615 min read113