数学形式化变简单:长论文 24-48 小时可转 Lean,作者开源 skills
kfountou · x · 2026-10-05
Scott N. Armstrong 表示 autoformalization 如今已非常容易:含大量前置知识、mathlib 未覆盖内容的长篇 PDE 或概率论文,也能在 24-48 小时内完成 Lean 形式化,更难的项目耗时也不会多太多。他写了博客讲解具体做法,并公开了自己全部的 lean skill 文件,便于他人复现其工作流。
「编程与Agent」频道最新
- Thoughtworks 杰出工程师实测：本地模型做 Agentic 编码靠不靠谱 — bibryam · 2026-10-05
- WIRED:AI Agent 大军即将涌入职场,而没人做好准备 — Dr_Singularity · 2026-10-05
- 新论文 IGP-Bench：让 AI 智能体学会「何时该停手」 — _sathvikr · 2026-10-05
- PS5 已逆向移植 80%,AI 反编译时代让「闭源软件」走向终结 — almmaasoglu · 2026-10-05
- 用户吐槽 Claude Code:插话 steering 时常无视你的消息 — Angaisb_ · 2026-10-05
- 三个孩子的爸爸用 AI 聊天插件替他操作 Ableton — _AustinCalvert_ · 2026-10-05