Life

2026/07/02 Closing the Loop: How Faithful Specialization Completed a Mock Theta Proof
2026/06/28 Breaking Through: A New Proof of a Mock Theta Function Identity in Lean 4
2026/06/27 Tell, Don't Compute: Precomputed Certificates for Heavy Kernel Verification
2026/06/27 Mechanize, Don't Hope: What I Learned Writing Skills for an LLM Agent
2026/06/27 Eliminating native_decide: How an AI Agent Cracked a 658-Digit Verification Wall
2026/06/20 What Holds a Polyhedron Together
2026/06/17 The Heavy Level
2026/06/14 The Same Key for Two Locks
2026/06/13 The Arm, Thrice Broken
2026/06/05 Formalizing a Time-Optimal Self-Stabilizing Majority Protocol, End to End
2026/05/27 The set Trap in Lean 4: When Cached Builds Hide Real Errors
2026/05/21 Formalizing Exact Majority: Bridging Informal and Machine-Checked Proofs
2026/05/14 Ripple Update: CTMC Infrastructure and Kurtz's Mean-Field Theorem
2026/05/12 When Formal Verification Finds a Real Bug: A Proof Gap in Ehrenfest Urn Theory
2026/04/26 Backhouse's Pancake Functions: A Single-Knob Family of Strict-GPAC π
2026/04/25 Computing ζ(5) by GPAC: Three Routes, Three Obstructions
2026/04/25 Computing ζ(2): a Residual Generating Function and a Recurring Obstruction
2026/04/25 Computing π Without an Inverter: Three Direct Designs
2026/04/25 Building the Chudnovsky π-Computer: an Explicit Analog Design
2026/04/25 Why π Stops Getting Faster: the Heegner-163 Ceiling
2026/04/25 The 1-Dimensional Kernel: Why Apéry's Trick Doesn't Port to Ramanujan
2026/04/24 Tunable-Rate Inverters for Analog Reciprocal Computation
2026/04/24 Where You Place √2 Matters: An Integration-by-Parts Trick on Ramanujan's Circuit
2026/04/24 A Six-State Analog Circuit for Ramanujan's 1914 Series
2026/04/06 Xing: Private Paths of Memory
2026/03/26 From Railway Relays to Chemical Reaction Networks: Analog Computing Through the Ages
2026/03/25 Hello World