Announcing the Palomar registry of Lean formalized mathematics: https://palomar-registry.org/ . See also my blog announcement at https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/ and the Lean Zulip channel at https://leanprover.zulipchat.com/#narrow/channel/621638-Palomar.