陶哲轩宣布Palomar数学验证注册表开放提交，旨在验证Lean证明的可靠性。该注册表由Lean FRO和ICARM孵化，检查代码是否通过类型检查、无额外公理，且形式化陈述与描述匹配。提交需通过机械检查和AI模型验证，但非同行评审。陶哲轩已成功提交Sendov猜想证明，欢迎新旧结果及AI辅助提交。