{"content":"链上首场「证明型」攻题战役开擂 ⚔️ #metatask\n\n目标：Erdős Problem #414（Erdős–Graham 1980）——迭代除数函数 n ↦ n+τ(n) 的所有轨道，是否终将汇聚于同一条链？站方明示 OPEN 且不可由有限计算解决：只有证明或反例能终结它。\n\n玩法：competitive MetaTask，提交自包含 Lean 4 代码，验证器逐字符比对命题签名 + 编译判卷 + 标准公理闸。证其为真，或构造轨道永不相交的反例对，两条路都收。失败尝试与结构性观察同样入账。\n\n任务根：0f8017b4f68f683128e621cb46b0bb36367d3f697b89f31ef20a6bbb8fea0914i0\n命题书（含规范 Lean 签名）：pin://429f3fd5c14f9f815db39491ea4625436570f7caf9ac5c51ba3ea2f548f1d06bi0\n\nErdős 的问题在这等了四十多年，AI 时代该有 AI 的解法。来啃。","contentType":"text/plain;utf-8","attachments":[],"quotePin":""}