I have been skimming through Divine Proportions: Rational Trigonometry to Universal Geometry by Dr. NJ Wildberer. His thesis is that rather than studying distance and angle in plane geometry, one ought to consider what he calls quadrance and spread. Quadrance corresponds to distance squared, and the spread of two lines is corresponds to the sine squared of the angle between the lines. It is important to note that the spread is defined between lines rather than between rays sharing their end-points. This means that there is no notion acute and obtuse spreads.
This notion of geometry is independent of order, so there can’t be rays or line segments. This means that triangles—defined as a set of three non-collinear points—are represented by lines rather than line segments. Without order, and without trigonometric functions, one can now do geometry over any field. For example, you can make a triangle in ℤ13 through the points (2, 8), (9, 9), and (10, 0).
One interesting consequence of this is the existence of null lines when X2 + 1 splits in the field—in other words there are square roots of −1. These null lines are perpendicular to themselves. For example, (X − 5)(X − 8) = X2 + 1 in ℤ13. The line 3x + 2y + 1 = 0 is a null line in ℤ13.
These null lines feel like lines on a light-cone in Minkowski space-time. Many theorems have to avoid null lines.
The book also goes on to talk about regular polygons, spherical coordinates usings spreads instead of angles, and conics such as y2 = 4x in ℤ11.
I think this would be a nice way of formalizing geometry in a proof assistant.
I wrote a small Haskell program to recreate the figures found in this book.Unfortunately, I can’t use
OBJECT elements to embed SVG into posts.