diff --git a/lakefile.lean b/lakefile.lean
index 023b9b44..9074ff1a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -47,7 +47,7 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HopfFibration,
     `CoreFormalism.StrandCapacityBound,
     `CoreFormalism.CRTSidon,
-    -- `CoreFormalism.CRTSidonN,  -- TODO(lean-port): auto-generated, targets different mathlib API
+    -- `CoreFormalism.CRTSidonN,  -- TODO(lean-port): auto-generated, ~15 structural issues
     `SilverSight.AngrySphinx,
     `SilverSight.CollatzBraid,
     `SilverSight.GoldenSpiral,