Updates
What Happens When the World is Run on Code No One Understands?
As SI accelerates mathematical discovery and software production beyond human comprehension, the authors argue that formal verification must become public infrastructure and a national mission.
Readable Formalized Mathematics: A Case Study
Making formal verification as readable as possible through a case study of Hessenberg digraphs.
The Network Structure of Mathlib
A multilayer network analysis of Mathlib, examining logical structure, compiler-generated dependencies, and the limits of network centrality as a measure of mathematical relevance.
Infrastructure for Mathematics
On formal mathematics as epistemic infrastructure, and the engineering and cultural systems needed to store, discover, govern, and reuse it.
Letter to Rozumot: Two (or More) Mathematicses
A speculative letter about mathematical truth, understanding, and a future in which SI produces proofs that people can certify but no longer comprehend. With a preface by Jeremy Avigad.