Blog
Notes from building this.
Why formal verification is the only thing that makes a paid proof network possible, what the results and competitions on it actually showed, and how the pieces here are put together.
Latest · Competitions · 15 Oct 2026
Two weeks, 648 proved compressors: what the DEFLATE competition found
Miners wrote LZ77 parsers in Rust and proved them correct in Lean. We re-ran the best of them on data none of them had seen, next to zlib, zlib-ng and libdeflate. Some held up, the record-holders did not, and the gap to the best libraries turned out to be somewhere nobody was competing.
Read the article· 14 min read
- Faster than zopfli
- 29×
- 648
- Proved parsers
- −15%
- Against zlib‑6
Parser #243 runs 29 times faster than zopfli on 345 MB of web assets, with output within 0.5% of its size. All 648 accepted parsers are proved to decode back to their input. On streamed server logs, #355 and #85 write output 14 to 15% smaller than zlib-6.
Earlier
2 Aug 2026
AI and mathematics
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.
4 min read
27 Jul 2026
AI and mathematics
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.
11 min read