Denis Moskvin, ανεπιθύμητος ξένος πράκτορας

Introducing: Palomar - an archive for formalized mathematics. Formalized mathematics is proliferating rapidly—accelerated by AI—but remains scattered across repositories, announcements, and private links, without common standards for finding, citing, or evaluating results. Palomar is a public, searchable registry of machine-checked Lean formalizations, giving each result a durable and inspectable record. Crucially, this infrastructure and its standards must remain under the stewardship of the mathematical community, rather than being determined solely by technology companies or automated systems. Palomar is jointly incubated by the nonprofit Lean FRO and the NSF institute ICARM. The initial advisory board is Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Terence Tao, Ravi Vakil, and Akshay Venkatesh. Read more on Terence Tao's blog or visit the archive. Links in comments.