RESEARCH · Research project
Readable Formalized Mathematics: A Case Study
Making formal verification as readable as possible through a case study of Hessenberg digraphs.
Closure of Knowledge
Understand and Guide Mathematical Research
BUILD & RESEARCH
Explore.
Projects and research from the CloK community.
Explore project
RESEARCH · Preprint
The Network Structure of Mathlib
Mapping the dependency structure of Mathlib.
BUILD · VISUALIZER
Astrolabe
Explore the dependency structure of public Lean projects.
UPDATES
Ideas from our friends.
Writing and perspectives from friends of CloK.
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.
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.
OUR VISION
Humanity, History & Knowledge
Across millennia, humanity has carried knowledge through memory, writing, machines, and networks. Follow the story of how we learn, preserve, and build upon what came before.