Mandelbrot

Stream: general

[Charles Hughes]

My friend and I made a quick little Mandelbrot visualizer in Lean4! https://github.com/chughes87/Mandlebrah. It was my first Lean project :D

[Charles Hughes]

Feedback is welcome/encouraged ;)

[Kevin Buzzard]

Do you have something which is tweetable? e.g. an actual png file or whatever?

[Kevin Buzzard]

oh -- I just checked and my linux box will open the ppm file as a picture file. But would a Windows machine? The browsers I'm trying just open it as a text file.

[Charles Hughes]

I could probably generate one if you want

[Kevin Buzzard]

If you pushed a png file to the repo and then I linked to the raw file then I'm guessing a browser would open it as a picture, but I might be wrong.

[Charles Hughes]

pushed

[Charles Hughes]

I'm having a hard time building the project in OSX latest version. I uninstalled and reinstalled xcode stuff and it wasnt helpful

[Charles Hughes]

I got the image just by running it in vscode lol

[Eric Fode (he) (S'12)]

Now I’m trying to figure out how to test this. in particular buildDimToComplex. How do I express a theorem regarding the relationship a the space of complex numbers it maps too, like that all of them are equally spaced?

[Eric Fode (he) (S'12)]

Here is a pr with some that i'd be interested in https://github.com/chughes87/Mandlebrah/pull/2

[Mario Carneiro]

Short answer: It's floats, give up

[Mario Carneiro]

(1) Floats are axiomatized in lean 4 so there are no interesting theorems to prove about them, and (2) even if they weren't, all the interesting theorems about floats are false

[Cody Roux]

Come on, Mario, you know that's not true!

[Mario Carneiro]

I consider a proper marriage of floats and verification using interval arithmetic or similar to be an open engineering problem

[Cody Roux]

In Coq you have this

Probably wouldn't be the worst thing in the world to port that to Lean, but....

[Mario Carneiro]

Porting that to lean would indeed solve problem (1)

[Mario Carneiro]

it would also prove that problem (2) is a problem

[Cody Roux]

Disclaimer: I did a postdoc with Guillaume on porting the excellent Gappa to SMT.

It's proof producing!

[Mario Carneiro]

ah, now that looks more like it

[Cody Roux]

There are plenty of interesting theorems for programs involving floats. Almost all require the numbers to be bounded by some "reasonable" constant though.

[Eric Fode (he) (S'12)]

interesting. What if i switched it to rational complex numbers instead of real complex numbers?

[Mario Carneiro]

those would definitely be usable in verification

[Mario Carneiro]

but there is probably a concern with the numbers blowing up since you are squaring repeatedly

[Cody Roux]

with the caveat that they are notoriously slow in "real" numerics

[Eric Fode (he) (S'12)]

Interesting, I'd have to make my fractions reduce? Does a recursively squared fraction always eventually become reducible?

[Mario Carneiro]

no, in fact it never does

[Mario Carneiro]

if you want to reduce you will have to approximate, which brings back 60% of the pain of floats

[Eric Fode (he) (S'12)]

Interesting! Hahaahah, practical tools are always lies.

[Eric Fode (he) (S'12)]

The paper for flocq is really interesting, thank you for the pointer @Cody Roux .

[Eric Fode (he) (S'12)]

What is the lean equivalent of Fixpoint?

[Mario Carneiro]

def

[Mario Carneiro]

You can just write recursive definitions without a special keyword

[Eric Fode (he) (S'12)]

Niceee! Ty.

[Eric Fode (he) (S'12)]

Gotta make BinaryIntegers first

[Mario Carneiro]

Ah, you are probably better off using Nat for that

[Eric Fode (he) (S'12)]

Excellent, I was worried it used the structure of the BinaryInteger to encode the float.

[Mario Carneiro]

If it is a bounded numeric type you might get by with using UInt8 or one of the other types; if it has a weird size then you can use a subtype like {n : Nat // n < 37} (which I guess is the same as Fin 37)

[Cody Roux]

As a word of warning: floats are actually pretty finicky, you might want to try fixed-point integers, which have better properties.