Mandelbrot 集拼图结构在 Lean 中完成形式化计算,实拍级图表曝光
geoffreyirving · x · 2026-10-28
Geoffrey Irving 分享了一张由 Lean 形式化计算(computed in Lean)生成的 Mandelbrot 集 puzzle/parapuzzle 结构图,展示 c₀=i 处的动力学平面与参数平面 correspondence:
- 动力学平面 f(z)=z²+i 的 K 是 dendrite,射线角度 1/7、2/7、4/7 落在 α 不动点;参数平面中同角度的参数射线与其等势线切出 M 的 parapuzzle 碎片,映射 Ξ(c)=hc⁻¹(c) 把动力学拼图结构搬运到参数平面
- 图中展示 Misurewicz 尖端附近 puzzle 与 parapuzzle 的匹配缩放(Tan Lei 因子 A≈0.800−0.400i),93% 的着色像素在两个平面中一致
- 所有角度用射线追踪精确数字、势用逃逸计算,在 Lean 中以双精度验证;「Display only, not certified」标注哪些部分未获证明
这是 AI 辅助形式化数学(Lean + cascade 项目)在复动力系统前沿的直观展示,涉及 MHC(Mandelbrot 局部连通性)类难题的验证基础设施。
「研究」频道最新
- RobotAgentBench 发布：VLA 会操作≠能自主，任务发现是短板 — HennyJieCC · 2026-10-28
- AIFlow 发问:生成世界训练的机器人策略过真实测试,敢不敢上线 — AIFlow_ML · 2026-10-28
- 新论文:按梯度范数排序注意力头,稀疏 RL 微调媲美全量训练 — SimonShaoleiDu · 2026-10-28
- 学者称 arXiv 已难承担预印本职,未来或沦为论文分发平台 — mjuric · 2026-10-28
- DeepMind 机器人模型短板：物体恒存性会漂移，2 厘米位移即认不出 — AIFlow_ML · 2026-10-28
- Hugging Face 研究员推出 Carbon-X 协调层：代币换社区训练额度与 DNA 赏金 — LoubnaBenAllal1 · 2026-10-28