The Weil conjectures project: a prototype for organizing mathematics into layered natural-language notes connected to a machine-checked formalization.