An initial formalized Mandelbrot picture

Stream: maths

[Geoffrey Irving]

Here is a formally verified point sampled render of the Mandelbrot potential function, which varies continuously from 1 on the Mandelbrot set to 0 at infinity (potential is roughly 1/|c| for large c). The definition of the image is here, and the correctness proof shows that each pixel is either (1) bright red, representing failure of the interval arithmetic computation, or (2) has each UInt8 color channel different from the exactly rounded answer by at most 1.

bad-mandelbrot-2024feb8-256x238.png

The main caveat is that this is point sampled: each pixel represents a conservative estimate of the potential function at a particular rational, in a regular grid. I'm going to make better images later out whether the estimates cover a whole square cell, but first I need to prove the Koebe quarter theorem.

[Geoffrey Irving]

Higher resolution:

bad-mandelbrot-2024feb8-2048x1902.png

[Kevin Buzzard]

The buggy red dots are gone too?

[Geoffrey Irving]

Zoom in. :)