Writing
Notes from building this.
Why formal verification is the only thing that makes a paid proof network possible, what the July 2026 results actually showed, and how the pieces here are put together.
AI and mathematics · 2 Aug 2026 · 4 min read
Why a kernel, and not a committee
A referee reads an argument and forms a judgement. The Lean kernel checks a term against a type. Only one of those can be run by a subnet.
AI and mathematics · 27 Jul 2026 · 11 min read
What Terence Tao is telling mathematics to build
Two conjectures fell in one week of July 2026. Two days later, the most influential mathematician alive stood up at the ICM and described what the field now has to build. This is that argument, and why this subnet is a bet on it.