我用「vibe」证出了康威猜想：一个月、一堆 token 和一个 Lean 证明

📋 概述

作者花掉整整一个月的空闲时间与大量模型 token，让前沿模型辅助写出了康威「细化猜想」（Conway's refinement conjecture）的 Lean 形式化证明。该猜想说的是超现实数中的全能整数满足细化性质：若 ab = cd，则存在整数 e、f、g、h 使得 a = ef、b = gh、c = eg、d = fh。证明已通过 Palomar registry 的机械检查，也有同时熟悉 Lean 与该领域的人认为命题陈述没问题，但作者强调它尚未被数学家独立验证，并公开邀请他人反驳。他自认是数学新手，最初只是想验证「不真正理解问题实质也能把题解出来」这件事有多荒谬——结果反而被它吸引。