团队将 Hironaka 奇点消解定理自动形式化进 Lean
Hidenori8Tanaka · x · 2026-10-07
jessehoogland 团队宣布在 Lean 中自动形式化了 Hironaka 1964 年的奇点消解定理——20 世纪最伟大的数学成果之一，其内容是任何奇异簇都是高维空间中某个光滑簇的「投影」。作者以长推文串形式解释了为什么要做这一形式化。
「研究」频道最新
- GroundedSLAM 发布:大幅刷新 Meta 第一人称 SLAM 基准 — Scobleizer · 2026-10-07
- HCI 学者吐槽：别把归纳式主题分析冒充「反身性」分析 — IanArawjo · 2026-10-07
- Reza Zadeh 称找到更快矩阵乘法算法，猜测大厂已接近指数 2 — Reza_Zadeh · 2026-10-07
- Reddit 网友提出图式确定性建模，解决 LLM 金融计算不可信难题 — jonnylegs · 2026-10-07
- COLM 2026 海报：面向智能体编程的测试时算力扩展研究亮相 — dan_fried · 2026-10-07
- COLM 2026 高效推理研讨会周五举行,含分论坛讨论 — tydsh · 2026-10-07