Lean FRO 与 ICARM 孵化 Palomar：为 AI 时代的 Lean-verified mathematics 建立公开注册与审计层

Terence Tao 于 8 月 18 日宣布 Palomar registry 正式开放 submissions。项目针对 AI-generated / AI-assisted proofs 大量涌现后出现的 trust problem：不仅检查 Lean repository 是否 typecheck，还检查是否引入额外 axioms、exact formal statement 是什么，以及 formal statement 与 informal claim 的语义对应。Palomar 由 Lean FRO 与 ICARM 孵化，定位类似形式数学的 public registry，而不是 novelty 或 mathematical importance 的自动认证。