不用 Python：纯 Lean 算 Mandelbrot，Claude 用点阵字体画出图

geoffreyirving · x · 2026-10-15

Geoffrey Irving 分享了在纯 Lean 证明助手中计算 Mandelbrot 集合的成果：他让 Claude 在没有 Python 的情况下制作图表，Claude 于是改用公有领域的 Hershey 点阵描线字体来渲染文字。

配图展示了 Mandelbrot 集八个最大的本原调谐副本、q=2 角映射的相图，以及普通双精度与认证区间算术（certified disk arithmetic）逐像素对比——约 95% 的像素可通过认证，其余集中在混沌导致证书失效的碎形边缘。