Geometry

Stream: new members

[kali]

I found this link which formalizes geometry using hilbert's axioms.

The angles defined here can be created with 3 equal points, isn't that a problem?
It's the same for triangles, there is no condition on the points.

Thanks

[Jireh Loreaux]

I'm not the author, but I suspect that it's not an issue. These are just degenerate cases. The point is that the angle determined by 3 equal points (or more generally, 3 collinear points) is just not proper (see ang_proper_iff_noncol). Then in many theorems, properness of the angle is a hypothesis, see for instance three_pt_ang_eq_iff_prep.

[Kevin Buzzard]

@Tianchen Zhao was the author, this was a Xena summer project.

[kali]

Ok ok thanks

[Tianchen Zhao]

kali said:

I found this link which formalizes geometry using hilbert's axioms.

The angles defined here can be created with 3 equal points, isn't that a problem?
It's the same for triangles, there is no condition on the points.

Thanks

That is a great question! Actually, the book I am following, Euclidean Geometry and Beyond by Hartshrone, uses the convention that three points must be noncollinear to define an angle. Indeed, most of the times we only care about 'proper' angles. However, if we use that definition in Lean, sometimes the theorem statement could be very messy since defining every angle involves proving the noncollinearity, so I didn't demand the points to be collinear and as @Jireh Loreaux said, I usually put properness condition in the statement. I guess the most results work in degenerate cases, but really we don't think of Euclidean geometry in that way. Plus, checking all the degenerate cases could be a disaster in Lean when there are many points.

[Marc Masdeu]

Take a look at https://github.com/mmasdeu/hilbert, I was also mostly following Hartshorne.

[kali]

@Tianchen Zhao It seems to be a common lean approach.
Restrictions are placed on theorems rather than objects.
It is true that it makes it easier to use.

[kali]

@Marc Masdeu I will look, thank you