diff --git a/lakefile.lean b/lakefile.lean
index e4c0d81e..38cbf85a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -37,6 +37,8 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HachimojiCodec,
     `CoreFormalism.HachimojiLUT,
     `CoreFormalism.HachimojiBridging,
+    `CoreFormalism.HachimojiManifoldAxiom,
+    `CoreFormalism.ChentsovFinite,
     `SilverSight.WireFormat,
     `SilverSight.ProductSchema,
     `SilverSight.ProductWireFormat,