Claude Opus 5.5 参与将 Gonthier 的四色定理 Coq 证明迁移到 Lean 4，并登记到 Palomar

Palomar 于 9 月 27 日登记一个四色定理 Lean 4 / Mathlib 形式化：项目将 Georges Gonthier 的 Coq 证明迁移到 Lean，并明确归因 Claude Opus 5.5 在 Robert D. Barish 指导下作为 AI agent 参与。登记说明该版本以 Mathlib 实数陈述主定理，重写可约配置检查为由 Lean kernel 检查的 bit-parallel certificate engine，并把 Coq tactic case analysis 改为一次证明正确的 checker 所检查的 case trees。