开源Lean形式化证明
__eknight__ · x · 2026-07-11
帖子表示，作者已经把某个证明的 Lean 形式化版本 开源，且该形式化工作由 GPT 5.6 Sol 作者完成。
同时，帖子还给出了：
- 证明正文链接
- 用来生成该证明的完整 prompt
- 形式化实现的开源仓库
信息重点是：不仅有自然语言证明，还有可检验的 Lean 形式化版本，方便复现与审阅。
所属事件:GPT参与署名的Lean形式化数学证明开源(3 条相关)→
「研究」频道最新
- AI 智能体协作优化 secp256k1 量子电路,挑战打破 ECDSA — StefanoGogioso · 2026-09-11
- Alex Townsend 汇编 200 个数值线性代数开放问题，供人类与 AI 攻关 — IgorCarron · 2026-09-11
- 本周热议的数学猜想到底关我什么事?一张普通人视角清单 — koltregaskes · 2026-09-11
- 用果蝇大脑连接组造了个 LLM,作者放出在线 demo — ngxson · 2026-09-11
- 社会学家 Harry Collins：LLM 无法发明新语言，做不了前沿科学 — whoamisri · 2026-09-11
- 「Waymo 效应」：AI 正在悄悄让科研协作变少 — JohnHammersley · 2026-09-11