Palomar: Neues Register für Lean-verifizierte Mathematik eröffnet
Palomar: A registry of Lean verified mathematics
Terence Tao kündigt die Eröffnung des Palomar-Registers für Lean-verifizierte Mathematik an. Das von Lean FRO und ICARM initiierte Register nimmt externe GitHub-Repositories mit Lean-Code entgegen, prüft maschinell die Korrektheit der Beweise und gleicht die informellen Beschreibungen per KI ab. Es dient als Preprint-Server für formalisierte Mathematik, ist aber kein Peer-Review-Journal. Tao hat bereits seine Formalisierung des Sendov-Vermutungsbeweises eingereicht.
Eine Nullte-Näherung dessen, was Palomar sein soll, ist das Analogon eines Preprint-Servers für Lean-Beweise.