陶哲轩团队与 Lean 社区互动，Buzzard 关心形式化证明成果
jacobaustin132 · x · 2026-09-07
Austin 回复透露，他本周在 Lean Zulip 社区与数学家 Kevin Buzzard 交流。Buzzard 目前的主要请求是整理一份勘误清单，让大家能从这次形式化证明中学到东西——这个工作已部分完成。Austin 称 Buzzard 非常友善，并且真心关心证明结果，希望 Lean 能繁荣发展。
所属事件:Buzzard 温和处理 FLT 争议：只求整理勘误表(2 条相关)→
「公司和人」频道最新
- NeurIPS 前任 SAC：拒一次邀请就再没被问过 — andrewgwils · 2026-09-07
- Caltech 数学黑客松定公平规则：全程AI对话开源并供学界审查 — FinanceYF5 · 2026-09-07
- 研究员批评某实验室安全事件披露含糊:拿缺框架当理由很荒唐 — eliebakouch · 2026-09-07
- Clara Shih 谈学生何时该用 AI:有判断力时才是最佳时机 — clarashih · 2026-09-07
- Claude Code 负责人 Boris Cherny：别省 token，先想怎么放大回报 — rohanpaul_ai · 2026-09-07
- OpenAI 智能体安全员工发声:对齐窗口正急剧收窄 — Scobleizer · 2026-09-07