Automated Planar Geometry in Wolfram Language

My name is Daniel McDonald. I am the lead developer for the synthetic geometry team here at Wolfram Research. Along with my colleague Peter Behrens, who has another video uploaded, we will be giving some updates updates for the synthetic geometry project in the Wolfram language, I will be introducing the new kernel function geometric solve values, and Peter will be talking about updates for fine geometric proof. We also encourage you to check out our colleague Shawn Wei Yang's separate talk that involves some synthetic geometry functionality. So I'll be talking about the function geometric solve values, which is will be appearing new in version 14 in a few short weeks. And so geometric solvalue takes its input, a geometric scene and some expression, and it solves for that expression, which represents some quantity in the geometric scene. So let's take a look at some examples. So as our first example, in most of these talks, I like to use Thales theorem. So Thales theorem, we have a geometric scene and we have a, a triangle and the circle that goes through the vertices of that triangle. And we specify that one side of that triangle is a diameter of that circle. So we can use our function random instance to visualize Thales theorem. So here we've got our circle going through the vertices of the triangle and one side of the triangle goes to the center of the circle. So geometric solve values, you know, can work in sort of two separate ways. One way is we solve for something for a particular scene instance. So for this particular scene instance, we're going to try to solve for the angle at this point B here. And if we do that, we get, we just get a numerical value based on the scene and it looks like it's about half of PI if we want to solve for this angle at B in general. So this is not based on this particular scene, but just based on our abstract scene. Then instead of inputting this particular scene instance, we just input the abstract scene for the first argument. And in fact we do get PI over two. So, so, right. So geometric solve values can solve for a particular instance or for a scene in general. So let's look at another example. So now let's consider a new scene where we've got one point, that one point C that hasn't fully been specified. It's got a Y coordinate, but it does, but we don't know the X coordinate. We just know it's positive and the other points in the triangle have been, have been specified. So let's visualize this. So our point C here has X value X and y value 5. And we are interested in the area of this triangle abc. So again we can look at.

This.

Particular instance and it's easy enough to find the area, we just do it numerically. But we can also find an expression for this area in any value of x. And so here we get 2x. So let's move on to a third example. So here let's look at a scene featuring a right triangle where we know the leg lengths but not the hypotenuse. So again, let's visualize this using random instance, right? So we're given that that AB has length one, AC has length two. And then H is this Euclidean distance, AKA the hypotenuse. So the sub value algebraic formulation of a geometric scene object gives a conjunction of constraints for that scene to be valid. That is, so if we take this sub value algebraic formulation of the scene, we get this conjunction of constraints for this scene to hold. So to find this hypotenuse we can, we can run the existing function solvalues on this algebraic formulation, or we can run our new function geometric solvalues directly on the scene. And in fact we get the same results. So just to be clear, running sol values on the algebraic formulation does.

Is.

Not simply how geometric solve values works. Most complicated scenes running solve values on the formulation will basic will take longer than you'd like to evaluate. No fault of salt values. It's there just can be much more complicated algebraic formulations than this. So in general I wouldn't recommend it. Geometric solve values does some chicanery behind the scenes to, to speed things up. Okay, so now let's look at.

A.

Few more complicated examples. So let's solve for the area of a triangle, right? So we've got the scene where we have these links specified and, and also specified the relationship between these two angles. And we would like to solve for the area of this triangle T. You know, in general, not just based on this particular scene. So if your geometry skills are are sharp, then perhaps you might like to take a look at this notebook and try to work this out on your own. But if you your geometry skills are not sharp or you're just a little bit lazy, you can run geometric sol values on this and see that the answer is 33. So we do get an exact answer for the area of this triangle. And let's, let's try another example. So here we've got a quadrilateral.

You.

Know, we can look at this picture. So what givens do we have? So we've got, we are given.

A.

Couple angles and a relationship perpendicular relationship between two lines and a few distances. And we want to find the area of this, this polygon P. And so again I encourage you to see if you can work this out on your, you know, go back to this slide and see if you can work it out on your own. But if you don't want to, you can see that the, the answer in general is 48 area units or 48 length units squared, I suppose. And then let's solve for an angle in this, this figure. So we're, so we've got, we are given 100 degree angle here and we're shown that the distance between A and B is the same as the distance between B and C. And then we're also given a couple other angles. So at A We've got 30 degrees and at. Qbc, which is here, we've got that this little angle here is also 30 degrees and we are looking for this angle APQ, which is right here. So again I encourage you, if you're geometry geometrically inclined to go back to the slide and see if you can work this out on your own. But if you don't, don't want to, or want to check your work, we can run geometric solve values and see that in fact this angle is also 30 degrees. And our final example for this part of the talk, we're going to solve for the distance between two points. So we've got this quadrilateral and we've got a few of these angles specified as this right angle. So right angle here, right angle here and right angle here. And we're given a few distances between points.

So we've got.

A, e is 6b, f is 6e, d is 3 and ab is the same as bc. So we've got a, b and bc the same distance. And we are looking for the distance between A and C, so the length of this orange line. So again, see if you can work it out on your own and get the answer which is 18. All right, so, so you know geometric sol values, as you see, just gives you an answer. If you're actually interested in how to prove these things using Wolfram language, then you should learn about fine geometric proof from my colleague Peter Barenz, who will be coming up next in this talk. Thank you.

Greetings fellow geometers. My name is Peter Behrens and I'm going to give an update on the resource function Find geometric proof. This has been discussed at previous tech conferences. It's still under development. Basically, fine geometric proof takes in a geometric scene object and produces a proof it includes many different properties and representations of the proof. But the most interesting one is the human readable proof that takes the form of a classic two column proof that is aimed at the high school level geometry student. Fine geometric proof uses a collection of elementary synthetic geometry theorems as its axioms, uses those to produce more and more conclusions. The first way to use it would be to give it a geometric scene and in the first argument give it a specific assertion that you'd like to prove. So this could be anything like the Euclidean distance from point A to point B is equal to 10. It could also be something with units. It could also be something with a pattern in it. And that would be telling it to find the first instance of a fact, return the first proved instance of a fact that fits that pattern. Alternatively, you can use the all keyword in the first argument. And that just tells it to produce as many facts as it can from the geometric scene, which could be quite a lot as you can imagine, depending on how complicated the scene is. It can also, given just a geometric scene, try to prove the conclusions which are that third argument of the geometric scene, that optional third argument. Now there's a lot of different options which are useful to sort of hone the kind of behavior you want, especially when it comes to using very complicated geometric scenes that can potentially produce a lot of facts, a lot of which may be not very interesting. The proof object that results contains a lot of different properties. We have many representations for a computable version, a data set version. Augmented scene and scene with conclusions are two ways of taking the facts that have been proved and recycling them into a geometric scene for further use, say with random instance. There are two graphical representations of the proof, the proof graph and the proof graph. Manipulate. The proof notebook is that classic two column proof that at least us high school students are used to and of course the length. So a very easy example. We can just find the base from an area and an altitude. In this case we have units of meters. We're given a line, a distance and an area. But if we put this scene into find geometric proof and ask it to prove that the the length of the base that is from Y to Z is a certain number of meters, it will find that proof. We can ask for the result property and we get that exact that exact distance fact in this case and the proof notebook. Here we see this kind of two column proof. Each fact is numbered, it's given a reason, and each reason references previous facts by number. Here's an example of using the all Keyword. Here we have a basic scene where we just have three parallel lines and then a transverse line and we're given exactly one angle. Here we've got the random instance of the same. If we ask to prove all facts. In this case we're given 21. It could often be much more and it could even go on for a very long time. But this is just simple enough that it doesn't prove too many things. It gets all the angles it can and then it finds some of the relationships between angles that it can't find. Looking at the proof graph, we have some nice features, such as tool tips for the inferences. Each fact is labeled with a vertex and the given ones are noted. Another thing we can do is to play around with the axioms that are allowed to a specific value of that option called full trigonometry. And that just allows the additional axioms of trigonometry. So if here, here we have a scene that's a triangle, but it's not a special triangle for which we would not need trigonometry. It's just a sort of a random triangle with two angles and a distance. And if we just run find geometric proof to find the area as a real, it will fail and give us this failure object. Although we could ask for the partial proof and that will give us. A few steps, which we could then look at the proof notebook and all the other properties that the proof object has. But if we set the geometric axiom's option to full trigonometry, we can actually get the proof. And if we look at the two column proof, you see that it uses the law of sines to begin with and then it uses Heron's formula, once it knows all three sides can find the area. A more advanced example is here, where it might not be so obvious how we get the distance from C to O. So we ask for a numeric value. In this case we have a pattern because we don't know the answer already. If we didn't specify that it was numeric, it might give us something that we don't want, like the distance from C to O is equal the distance from B to C or something. So we want a numerical value in 14 steps, it finds the result and the result is 15. And if we look at the proof notebook, we can see that it uses Ptolemy's theorem on cyclic quadrilaterals and some algebra on some of these previous steps to get the final result. Thank you for listening.

All right, so that is our talk. Unfortunately, Peter is a bit under the weather today. So I'm Dan. From the first video, I can continue answering, answering questions in the chat. It is, let's see, I feel like. Right, so I'm, I think I'm the only one who's able to speak. So I'll keep answering questions in the chat until 2 o' clock when hopefully you go to your next, next session. So anyway, so previous questions had to do with Whether there's a 3D version of this coming out. And that's sort of our next project for the synthetic geometry is for. Our next big project is to allow for sort of an interactive construction method for geometric scenes. Rather than having to code it, you can sort of have a palette where you sort of draw your own lines and circles and we figure out the relations that you want to hold, hold among your structures. And then we, you know, create a geometric scene based on that. And then sort of after that, our next major project will probably be something like geometric scene vaccine 3D, which will be a major undertaking and will maybe require a few new computational techniques because that will be rather computationally intensive. Let's see. And Bruce just asked a question. These capabilities are clearly valuable in the classroom. We hope so be aware of their use outside the classroom. I will say that as far as random instance goes, this is, this is what's technically known as a geometric constraint solver. And so geometric constraint solvers outside of the classroom are actually used in CAD drawings. I feel like we will be, you know, if we get the geometric scene 3D working, I think that will be quite useful for CAD drawings. You know, I think there are, are some, you know, some uses for the current geometric scene for 2D CAD drawings. But I think it will be quite useful once we can get it into 3D. As far as the next question here about adapting our scope to hyperbolic geometry or non Euclidean geometry, that we've gotten that question before that, that project would, if that happens, would that would happen after we got the geometric scene 3D working. So I think 3D Euclidean geometry would happen before that. And you know, along with our, you know, 3D, you know, geometric scene 3D is presumably what that would be called. We would probably want some other sort of palette for constructing those. And then once we get done with that, then the next major project would be looking into the viability of non Euclidean geometry. So none geometry is on our radar.

But.

That would be very far down the line because we're about to release version 14 and in the ideal world we would get this palette for the current geometric Scene and by version 15 maybe, and then have some version of geometric scene 3D for version 6, 16 maybe. And then if we did that non Euclidean geometric scene, that would, that would be probably version 17 or 18. So that is quite far down the road. It's been on our radar. But there are some, you know, that will be. There are some. There's a lot of design work and computational, computational experiments that we'll have to do before we can, before we can get, get non Euclidean geometric scenes working. Let's see. Right, so we have the geometric scene constructor and Wolfram Alpha nopeg addition that can be used in Mathematica. How is that different from what you said in your next project? Right, so that is actually sort of a halfway step to our next project. So one where, you know, we'll be sort of tweaking the design of that to get that in the kernel with this. But the big project will be something more like you would see with geogebra or some of the other existing geometry functionality, where rather than click things off.

Of.

Click text buttons that say, okay, I want a circle or something, you would actually have something where you could draw a circle. So something a little closer to. The drawing programs, to actual drawing programs, where you'd have circles and lines and you actually are placing the circles and lines where you want to. And then perhaps you can add some implicit constraints if you want, but sort of drawing a geometric scene yourself. And then we figure out what the actual coded version of that geometric scene is if we want to plug it into any of our functionality. So yes, you are correct that, so you are correct that this geometric scene constructor is sort of our first step in this avenue. And we do hope to, after some design reviews, we do hope to get that into the kernel first and then we would, we would work towards these actual drawing palettes.