HNHiroyuki Nakahatainblog.iroha1203.dev·4h ago · 18 min readUncharted Waters: Thirteen Rules for Not Trusting an AI's ProofsTL;DR I want to hand an AI agent a multi-day job and have it run to completion. This post collects the rules for that — thirteen of them. Never let the loop rewrite its own spec. Enumerate up front w10
HNHiroyuki Nakahatainblog.iroha1203.dev·5d ago · 22 min readSemantic Geometry of ArchitectureTL;DR Does software architecture have a denotational semantics? Yes. But it differs from the classical one in three ways. Syntax is generated from observation. The meaning of a whole system does not 10
HNHiroyuki Nakahatainblog.iroha1203.dev·Aug 8 · 24 min readAtlas Theorem: How Far Can You Zoom Out?TL;DR A veteran reviewer does not read every line. They switch reading resolution to match the property they are checking. Is there a guarantee that reading coarsely misses no bugs? This article is t00
HNHiroyuki Nakahatainblog.iroha1203.dev·Aug 2 · 21 min readTaming 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 54LT
HNHiroyuki Nakahatainblog.iroha1203.dev·Jul 27 · 12 min readThe 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 i00
