STOC 2027 全部 1665 篇投稿公开，AI 已把 1496 篇定理译成 Lean 4
ChenhaoTan · x · 2026-11-13
理论计算机科学顶会 STOC 2027 将全部 1,665 篇投稿公开，社区随即在 Prove2Me 平台发起 STOC 2027 Formalization Initiative。
- AI agent 已把其中 1,496 篇投稿的主定理与辅助引理翻译成 Lean 4 形式化陈述，部分已给出完整证明形式化。
- 项目向作者、研究者与社区开放认领：可对照原论文校验形式化陈述并补充证明。
- 门槛低：不需要懂 Lean 或完全理解论文数学，只要会用 AI agent 就能参与形式化工作。
「编程与Agent」频道最新
- 任务完美完成但对象错了:Reddit 热议 Agent 的意图错配失败模式 — djgoel123 · 2026-11-13
- Codex 重度用户求助:会话一多就找不到结果,老会话管理成痛点 — grahamhart_ · 2026-11-13
- Kernel Autoresearch：让编码智能体把可迁移归纳偏置写成程序 — kenneth0stanley · 2026-11-13
- ChatGPT 沙箱里反复要授权惹恼用户:一次任务被迫确认三四次 — Frustrated9876 · 2026-11-13
- Mitchell Hashimoto：用 eve 加 Vercel Workflows 搭自定义 agent — cramforce · 2026-11-13
- Gemini 多智能体 /teamwork 实况:多 brain 任务日志实时并行跑飞 — RyanSpunk · 2026-11-13