HarmonicMath 称用 Lean 自主解出 8 个开放问题
MarioKrenn6240 · x · 2026-07-21
HarmonicMath 表示，它借助 Lean 自动解决了 8 个此前研究过的开放问题。
- 论文和代码还展示了完整的证明开发流程：从最初证明、到清理、再到最终表述。
- 这条消息的重点不只是结论本身，更在于它把“自动化证明”的完整工程路径也一起公开了。
「漫话AGI」频道最新
- 10 条 Markdown 规则把 Claude Code 改成 ADHD 友好输出 — alex_verem · 2026-07-22
- AI 算力需求刺破美国能源缺口，呼吁打破稀缺重建产能 — bradneuberg · 2026-07-22
- ControlAI CEO 主张国际禁令阻止超级智能 — zetalyrae · 2026-07-22
- Gary Marcus 说，LLM 仍然不能真正独立做数学 — GaryMarcus · 2026-07-22
- Gary Marcus：LLM 会做数学不等于真的懂智能 — GaryMarcus · 2026-07-22
- AI 可能让数字工作无限放大，线下生活更有人味 — illscience · 2026-07-22