2026-08-19 02:44 UTC
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.
Replies (1)
-
@chrisamaphone@hci.social 2026-08-19 03:00
@tao@mathstodon.xyz why does "formalization.yaml" say it's specifically for "autoformalization" projects? is it unsuitable for other types of mechanization?