CausalSmith:GPT-5.6 与 Claude 协作全自动产出 Lean 4 验证的计量理论论文
daveholtz · x · 2026-09-15
耶鲁研究者 Vasilis Syrgkanis 团队（学生 Jiyuan Tan 主力）发布 CausalSmith——一个全自动 agentic 研究管线，能端到端完成因果推断的计量理论研究和论文写作。
关键事实：
- 站点上所有工作论文中的定理、假设、引理均经 Lean 4 机器验证，点击任意命题可查看对应 Lean 代码；底层基于 Causalean 库，带自然语言翻译与审查状态。
- 分工明确：OpenAI GPT-5.6 Sol 负责主要数学推导与 Lean 形式化，Anthropic Claude Opus 4.8 负责规划与 Lean 代码审查，OpenAI GPT-5.5 负责论文撰写。
- 首篇亮点论文研究固定重叠（fixed overlap）下离散混杂的平均处理效应极小化极大速率，证明 MSE 速率 1/n + d²/(n²(log n)²)，并给出 AI 审稿人 8/10 的评分。
这是「AI 科学家」方向少见的以形式化验证保证正确性的尝试，意味着产出的数学结论可机器查证而非仅靠模型自述。
「编程与Agent」频道最新
- GPT-6 Astra 八个狂野用例:数小时做出游戏、机器人demo和3D管线 — socialwithaayan · 2026-09-16
- 提议:把可预测 UI 流程交给本地脚本执行,大幅省下 computer-use 视觉调用 — Iinganouo · 2026-09-16
- 用 OpenTelemetry 追踪 Agent 与 LLM 调用的教程 — dl_weekly · 2026-09-16
- Atria Dawn Preview 发布：基于 744B MoE 底座，多项 agent 基准领先 — alexcovo_eth · 2026-09-16
- LangChain:每个托管Deep Agent都是MCP server,可被Agent当工具调用 — LangChain · 2026-09-16
- LlamaIndex 复盘用 Stainless 生成 SDK,团队已加入 Anthropic — llama_index · 2026-09-16