Matematik Terence Tao oznámil otevření registru Palomar, který má přinést pořádek do rychle rostoucího počtu matematických důkazů generovaných umělou inteligencí a formalizovaných v dokazovacím nástroji Lean. Registr, za nímž stojí iniciativy Lean FRO a ICARM, přijímá snapshoty GitHub repozitářů s Lean kódem. Automaticky kontroluje, že důkazy procházejí typovou kontrolou a neobsahují podvody typu přidaných axiomů, a pomocí velkého jazykového modelu ověřuje, že se formální zápis shoduje s neformálním tvrzením. Tao už do registru úspěšně vložil vlastní formalizaci důkazu Sendovovy domněnky. Palomar podle něj není peer-reviewed časopis, ale obdoba preprintového serveru pro Lean důkazy.
