Geometry and CAD

Stream: Is there code for X?

[Ricardo]

Hello. Hope you're all well. Very newbie question here. I'm looking into constructing a 3d model of a house and wanting to learn more lean4. So I'm wondering if there's code for simple euclidean geometry in 3 dimensions and, if that's true, what's the closest thing in lean4 for defining 3d shapes and objects with the hope of exporting these objects to a format that can be understood by freecad and blender.

[Weiyi Wang]

Lean & blender/cad... that's an unexpected combo to me. Sorry I don't have an answer but I am interested to see ideas here

[Kevin Buzzard]

I once wrote python code constructing coordinates of a regular dodecahedron and then imported this code into Blender, took the convex hull and then 3D printed the result. The python code had a bunch of sqrt(5)s in which of course were computed as Floats. The thing about Lean is that one might imagine that all the Euclidean geom stuff we have will naturally sit over Real and might well be noncomputable so one would need a map from Real to Float plus ways to compute its value on whatever one is using in Real.

[Ricardo]

Yes, I understand. The map would be something like "get a computable Real that can be represented as a Float and is epsilon-close to this (possibly noncomputable) Real". Not sure if it's always possible to know if such a computable Real exists.

I was thinking though more in the line of a geometry library working directly with Floats.

[Weiyi Wang]

Because one basically can't prove any theorem using Floats, such library is probably no better than a computational library in any programming language
Perhaps one with computable rational/constructible/algebraic numbers would be more useful?

[Ricardo]

No better than a computational library in any programming language is good enough already. Plus I think some things could be proved anyway with Floats. Computable rationals/constructible/algebraic numbers would all be good too.