Claude 在纯 Lean 环境中绘制出 Mandelbrot 集

Geoffrey Irving 让 Claude 在纯 Lean 证明助手环境中、不借助 Python 计算并绘制出 Mandelbrot 集合。模型还用公有领域的 Hershey 描边字体渲染文字，并以点阵字体画出图形。该实验展示了大模型在专用形式化编程环境中的代码生成与图形渲染能力。