Formally verified nucleus tower stabilization on frames with infinity-groupoid bridge. 23 theorems, 9 modules, ~977 lines of Lean 4. Zero sorry. Proposed by Adam Morgan (@2ndAlphasapien).
category-theory homotopy-theory formal-verification heyting-algebras lean4 nucleus-operators infinity-groupoids kan-complexes
-
Updated
Mar 18, 2026 - Lean