Skip to the content.

∞-Cosmos

A project to formalize ∞-cosmoi in Lean.

Blueprint (web) Blueprint (pdf) Documentation GitHub

Useful links:

Zulip chat for Lean for coordination
Blueprint
Blueprint as pdf
Dependency graph
Doc pages for this repository

infinity-cosmos is maintained by Emily Riehl, with help from Mario Carneiro and Dominic Verity. Visit the GitHub repository for more information.