Automated Planar Geometry

I am Daniel McDonald and my colleagues Peter Brinzi, who is in Boston right now, Jack Heimreith and Jeremy Stratton Smith will be talking to you today about advances in our automated planar geometry project at Wolfram. Right, so you know the project was basically introduced in version 12. It includes the functions geometric scene, random instance, find geometric conjectures and various other ones. And we're going to be talking about updates to that as well as some Wolfram resource functions that are related. So this notebook and related packages that you'd need to load to run it are available on Pathball. Ok, so first I'm going to talk about some updates to geometric scenes, specifically geometric styling rules, which is just an option for styling geometric scenes. There we go. So previously you'd have to wrap the style head around structures inside the geometric scene to style it, but now we can just have an option at the end if you want to style multiple things at once. So you can see here we can style the points to be black, all the circles, all one of them to be red. And then this here happens to be Thales theorem. And so the conclusion is that this angle ABC is a right angle and the conclusion is styled in purple. So a few oops, let's go a few more examples for point labels. We can make them large and pick a terrible font for them. If you don't want point labels at all, you can remove them by setting point style to none. And then a few fun examples courtesy of Michael Trott. Here's Napoleon's Theorem, styled with pictures of Napoleon. In case you're wondering, it's generally accepted that Napoleon did not actually come up with improvements. Napoleon's theorem, unlike Barrow's inequality, which probably was due to Barrow. So here we've styled Barrow's equality with itself. And you can also style a scene dynamically, which hopefully is not going to cause any medical issues. Okay, so next I'm going to talk about fine geometric proof. This is the work of my colleague Peter Brinzey. Could not be here. So basically this is a synthetic automatic automated synthetic geometry proverbs that will soon be available as a resource function. It produces a proof object which is sort of a two column proof that you're used to in geometry, at least from the high school level. So it takes as input geometric scenes and then can prove a specific fact or anything matching a fact pattern, as you'll see. And there's a little bit more here about how it works, but let's just skip ahead to some examples. Right, so here we Have a geometric scene and we've. It describes a triangle with some, you know, various lengths and areas. And we want to, we want to find the Euclidean distance between these points Y and Z. So, so we input the scene as well as what we're looking for, even though we don't know the answer. And we get as output this proof object. If we want the result, it'll tell us the answers. 26 over 3 meters. And then if we want the proof, we use a sub value proof notebook. This is a pretty simple proof. And so you can see here we can, you know, kind of automatically know since the area of XYZ is 13 meters squared and the line segment from W to X is an altitude and has length of 3 meters, then we can use this formula to find the length of the base. So we can also do more complicated things like Ptolemy's theorem. And I'll. Sorry, we can use Ptolemy's theorem to solve this example and I'll show you what Ptolemy's theorem is. So here we have this geometric scene.

Where.

We have a circle through points A and B centered at point O. And we have these various distance given, including for this, this point C here. And we want to know what the distance between this point C and the center O is. And again we'll look at what's given. We know a right angle here at A and we are given distances between B and A, C and A. Sorry, C and yeah, C and A. And then also that this angle here is right. Okay, so we ask for the distance between C and O and we get this proof object and we can. The proof here is a bit longer, but sort of the crux of it. And the released version will spell Ptolemy correctly, I'm assured by Peter. Ptolemy's theorem states that in any cyclic quadrilateral the product of the diagonals is equal to the sum of the products of the opposite sides. Then we can plug and chug, then do some algebra and get our proof. Then finally there's an example where you can find the golden ratio using similar triangles. And I'm just. You can look through this on the notebook on pathable, but just sort of. This is another long one and we end up with some algebra at the end. But I'd also like to point out that we can use a sub value proof graph manipulate to get a proof graph which has tooltips showing. Okay, this is the givens and then this is how we work through the proof to end up with our result. Okay, so now I'd like to hand it over to Jack Heimrath, who will talk about his work at the Area Method.

So, hi, my name is Jack Heimrath and I'll be talking about the Area Method. Maybe first I will explain what the Area Method is, since it's not really a commonly known proof solving technique or proof generating technique. So the Area Method is simply in the big picture is that it's a semi algebraic theorem proving method which generates more or less human readable proofs as opposed to other formal proof verification procedures. But the downside is that it only works for Euclidean geometry, which for us is fine, at least for now. It only works for Euclidean geometry. Foreshadowing. Yeah. So the overview of how we implemented the Area Method in the Wolfram language is that it's basically a three step process. You define your geometric construction much like you normally would. You ask question which you have to state in a very specific Area Method format and then you use the. Use the verify conjecture function which we developed to prove or disprove our theorem and to generate a proof. Yeah, so I will now just quickly show some examples of how you would possibly work. Yes. So we'll start by trying to prove the British flag theorem, which is a simple theorem which states that in any rectangle, if we choose a point P, then the sum of the distances from P to opposite vertices of this rectangle is equal or the sum of the squares of those distances. And this is just a simple application of Pythagoras theorem. So first we can prove this method numerically. We ask our conjecture. We have. This is how we would construct this rectangle in the Area method. We define three free points. Then we define D to be on a line perpendicular to one of those, one of the, one of the lines in our construction. And we finally define C to be on a parallel line through the point previously. Through the previously defined point D, we state our conjecture. We get this nice graphic where we can show that this. So here, okay, sorry, at the top are conjectures displayed. And our conjecture is essentially that this quantity is zero. And we see that no matter how we manipulate our rectangle. Yeah, we can just get any rectangle, the point, the distance of P, the sum of the squares of distances from P to the opposite vertices is zero. But this is just a numeric verification. We would like to find a formal proof. And this is what happens here. We input, basically we provide basically the same arguments to our verified conjecture function and this outputs a proof which is literally just. This boils down to one application of Pythagoras theorem. OR 2 Applications of Pythagoras theorem. But it also turns out that this theorem can be generalized in a slightly weaker form. And we will show how to explore this. So first we define this auxiliary function which just to avoid writing those sums of squares of distances repeatedly. And now we show that if we take any parallelogram, notice that as I change the parallelogram, the sum of squared distances value changes. But if I change this move this point P for a fixed parallelogram, it remains constant. So this gives us a certain conjecture that for a given parallelogram, the sum of the distances is squares of distances is constant. We can further confirm this by choosing any two points P and Q and taking their applying the theorem to both of them and choosing the distance, the difference of the sums of squares of distances. And here we see that no matter where we move points P and Q, our conjectured quantity is 0 is exactly.

What would we expect.

And once again we can generate a proof notebook for this statement, which is again a very simple proof. The next example I would like to show is a Helmslev's theorem. Here I won't really go into much detail, but the point here is, is that this is a theorem which states that if we isometrically map points from one line onto the other line, then the midpoints of the corresponding lines will also be collinear and they will also be isometrically or equidistant according to the distances of the original points. And the big deal here is that this proof usually uses the classification of isometries in the Euclidean plane. But this proof, I mean, there are other planes which don't use the classification, but ours doesn't as well. And this allows us to hopefully in the future work with non Euclid work in non Euclidean settings. Because basically we're generating a proof of this fact without using the parallel postulate of Euclidean geometry. So this is a slightly more complicated proof. I won't go through the details, but yeah, we get that the proof is true. And what's new since last year, well, we've implemented working with angles. Again, this is a very long proof, so I won't really go into it, but we can prove the, sorry, the angle bisector theorem, for example, and we can also construct arbitrary angles, which is something that was not possible previously. Yeah, long proof, I will skip this, but in the output we will get that the theorem is true. The area method has also previously been implemented in CoQ, which is a language for formal proof verification. Unfortunately, the CoQ area method package is Very outdated and hasn't had any updates Since I think 2009 and doesn't work with modern versions of the COQ language. So what we did is we simply implemented a parser which hijacks inputs and interprets them as well from language inputs, and we can generate proofs from directly from COQ inputs. And finally, since last year, we've managed to greatly improve the evaluation times of our proofs. You can see here that comparable theorems proved on the same hardware are on average about an order of magnitude faster. This notebook will be available to anybody who would like to work with it on pathable as well as the package. And that's it for me. And I will hand it over to Jeremy Stratton Smith who will talk about geometric scene construction functionality.

Awesome. Hopefully you all can hear me. So we're sort of ending a little bit at the beginning here because as you've seen throughout the presentation, there's a lot of code involved in making these geometric scenes oftentimes. So in the past year, the functionality that I'm talking about here is essentially an interface to allow you to program to more easily build up a geometric scene without having to necessarily know all of the particulars of the syntax right at the beginning. So right off the bat, when you run geometric scene constructor, this is essentially what you get. And hopefully it's fairly straight, it's fairly self explanatory. But I will go ahead and walk us through some examples here. So you can go ahead and pick a particular kind of primitive. And as you can see, we populate a number of other things here which I'm not going to pay too much attention to mostly, but for a line, we want a line going through A and B. If we want, we can name this something else. I'm going to leave it as line AB for now and I'm also going to make a circle through. We're going to. We're going to build up Thales theorem here and the points this is going to be going through are A, B and C and the center, I'm just going to call that O with a radius R because we don't particularly care what those are.

And.

Let me make sure the line we actually, now that we have a center, I'm going to actually modify this and put OH in our line here so that we have that diameter of the circle. And I believe the final piece that we're going to need here is just having. Am I doing this correctly? Let me think. A AOB you have to think a little bit Sometimes it can be helpful if you're coming from a textbook or something where something's already drawn. But I think I just want A, B, C here. And without having to do anything else, if we just want to print this out exactly as is, we can go ahead and click, whoops, sorry, this is not my computer, so I'm adjusting. So you go ahead and click Print Geometric Scene and the code pops out for exactly what you've just written. And I'm going to go ahead and make a few new lines so you can see that better in the back. If you. If you don't want just that, you can go ahead and click Visualize Geometric Scene. And this not only prints out the code, but it also gives you the random instance and evaluates that for you so that you can see right away what exactly you're working with. If, for instance, you want to start doing a little bit more involved work on this, you can also do things like adding relations. And I think I'm actually going to make. We're going to. I'm going to start a new scene here just so that we can start from scratch. And in this case, let's just do a few lines and. Trying to think what's an interesting. Well, okay, I'll do two lines for now and we can go ahead and select these two lines. And then once we've selected a set of figures we are generating based on those figures, what kinds of relations might we have? And I realize this maybe is a little bit small, so it doesn't exactly scale with the presentation mode, but in this case I'm going to say that these two lines that I've selected are perpendicular. And when we go ahead to visualize this scene, it again automatically populates those properties for us so that we don't have to remember the particular syntax involved. So hopefully this is both flexible and usable. We can also add in things like if you want to add a particular style to one of your. Say I want to make.

I don't.

Know, I want one of my lines to be green. I can add that here if I have, you know, particular specifications that my line BC is actually supposed to be vertical and upward, for example, so it's going B, C. These are all things that you can specify inside of Geometric Scene. And this just sort of allows you to do that really easily. And here we have our line BC going vertically now that we've specified it as such. So. Yeah, any questions on that?

I think that's.

Oh, yeah, please.

If somebody wanted to take your. And extend it to, like, three dimensions, you think that would be a relatively straightforward process or.

Right. So I think that when you start thinking about three dimensions, we're stepping away from the geometric scene in plain geometry. So right now, this is built specifically to be working on plane geometry and within the geometric scene environment in terms of. I guess when you're talking about extending things to three dimensions, then you're sort of talking about. Are you talking about regions? Are you talking about graphics primitives? Because right now this is working just with these primitives as. As they are thought about from the geometric scene perspective. And if you wanted to be building something for 3D geometry, it would be.

It would.

It would be a different sort of environment to be working in, if that makes sense. I can talk. We can talk about it more if you want, though.

Does the product handle polygons of more than four edges?

Certainly, yeah. So if you want to add in, there's a. There is a generic polygon primitive here, and you can add however many points you want to it.

Yeah, yeah.

And. Yeah. And as you can see, you can specify various properties of the polygons and primitives as you go.

Yeah.

Any other questions?

No?

Okay, awesome. Thank you so much, everyone. And hopefully you'll be able to make use of this.