Automated Geometry Theorem Generation

So I'm going to talk about automatically discovering geometry theorems, something you might want to do if you wanted to pose a proof problem that the solution didn't exist on the Internet, or one might want to do to automatically provide test situations for a symbolic geometry program. Specifically, I'm going to talk about angle theorems. And even more specifically, I'm going to talk about angle bisector theorems. Now, that's not quite as small a universe as it would initially seem. For example, the theorem there, although only has one explicit angle bisector, it has a reflection, which when you think about it, reflection specifies that the mirror is the angle bisector of the incoming ray and the outgoing ray. And it also has a CircumCenter which defines three isosceles triangles and the isosceles triangle. The base is perpendicular to the angle bisector at the apex. And so this is in fact an entirely angle bisector theorem. I'm actually going to represent angles in terms of the directions of directed lines, their angle from the positive x axis. And so the angle between two such lines is just the difference in their directions as long as the positive x axis doesn't lie in the angle. If it does, it's that difference plus 2 PI. Now this need to remember where the positive x axis is makes this a very poor representation for human beings to use. But computers can be coerced to deal with it. I define the principal angle bisectivity in two directed lines to be the line which has a direction, the average of the two directions. This is going to be in the sector that does not contain the positive x axis, which may of course be a reflex sector. If you have an isosceles triangle, the base is just PI by two away from the angle bisector. The angle bisector has of course satisfies the equation alpha plus beta minus two gamma equals zero. That's just expressing the average. The base of the isosceles triangle has that same equation, but with a PI or a minus PI depending on which direction we're regarding it on the right hand side of the equation. So here is a pure bisector theorem. We have V5 is the bisector as angle bisector of V1 and V2. And we can see contributes the equation over there to the right there. V6 is the bisector of V2 and V3 contributing that equation V7 bisector of V3 and V4 V8 the bisector of V1 and V4. Now because V1 and V4 has the positive x axis between them. Then that V8, as you can see, is in the reflex sector. V9 we're defining as the bisector of V5 and V7. And we're going to make a final statement, which I can, is that V9 is also the bisector of V6 and V8. So those six linear equations can be expressed as a matrix equation. If we look at the rank of this matrix here, we find it's rank five, it has six rows. So that says we're rank deficient, which means that the sixth row could be defined by the previous five, I.e. that this is a theorem that sixth row is determined. So if we think in terms of isosceles triangles, we're going to get a couple of differences. One, we're going to have something other than zero on the right hand side. There's some PI's and minus PI is distributed there. But also our two final bisectors are clearly not pointing in the same direction. So I've separated them out. I've got W9 and W10. W9 is the bisector of W5 and W7. W10 is the bisector of W6 and W8. And I've created an equation that says they're a specific angle, actually PI by 2 apart. So we end up with a matrix which has, if you notice the difference, I've split the final column into two, but I've added an extra row for the angle. But that still has rank one less than it ought to have as rank six. So the final rule is determined and we have a theorem. So that was, if you like, a little tutorial about looking at these equations, these theorems as matrices. Here I want to go to where I started with this little project. I started with a couple of different theorems, both of which are bisector theorems. The first was this theorem where we have two cyclic quadrilaterals which share three of their sides. The theorem states that the fourth side of each FG and DE are parallel. So I can break this into eight isosceles triangles and come up with a matrix. So for example, I have an isosceles triangle 1, 8, 12, and over here, matrix I've got a line with 1, 8, 12. I have called FG and ED the same thing. They're both direction 12 because they're going to end up being, we want them to be parallel so they both have the same direction. So they're Both occupying this 12th column of my matrix. And that matrix is rank deficient. It has rank 7. Here is the other theorem I was thinking about. This one. We have a hinged mirror abc and we're impinging two parallel rays on that A and C. And the reflected rays meet in a point which lies on the circumcircle of A, C and O, where O is the circumcenter of A, B and C. Now, this has got a lot of isosceles triangles in it, but it's also got a couple of explicit reflections. So I have taken the. I've called the two parallel lines both 12, and we see that 12 reflects in AB reflects in line 1 to give me 8. And so that gives contributes the line of the, the row of my matrix with 8, 12 and 1. And likewise 12 reflects in 10 to give you 7. And that gives me the final row 12, 7. And the bisector is 10. Now, when I looked at these matrices, both have rank seven. So both reflect both our theorems. But when I looked at them, I noticed that the non 0 entries are in the same place. Of course, that was fortuitous labeling on my part, but I did collaborate to create these. So I was thinking, okay, what I want to do, of course, is up with new theorems. So if I could start with another matrix that's ranked efficient, I could then work out a way of creating a theorem for that. And I thought, well, I've got two with this pattern that are ranked efficient. How many others could I get? Well, how many such matrices are there? There's only three to the eight. How many? You have to put the minus two into somewhere on each row. So that's only 6,000 odd. I easily crank that into Mathematica and calculate the rank of each. How many of Those have rank seven? The answer is 33. Okay, great, 33 matrices, 33 theorems. Then I thought, well, wait a minute, maybe they're not all really the same because I can change the labeling of things. And maybe those 33 are just my two in different guises. So I had to, I wanted to actually look at the two matrices in some visual form to give me an idea about that. So visually, sure, every row has got three non zero elements. By definition, it's got one and one and a minus two. But these two theorems, both fortuitously or both, have exactly two non zero elements in every column. And so I thought, okay, that's something that could be represented as a graph where the non 0 elements represent edges of the, the columns of my, of my matrix represent edges of the graph. So I create a graph with you know 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 1, 625 and so forth. And that's what it looks like. I'm looking at a cube, but I want to see the matrix represented graphically. So I need to indicate where the minus 2 is on that cube. And so what I did was I decided that minus two is going to be in a row and a column. The row represents vertex of the matrix, the column an edge. So I'm going to put an arrow on the edge next door to the vertex that is the row and column. So for example, in my matrix I have a minus 2 in the 44 location. So next to vertex 4 on edge 4 I put minus 2. And here I also have minus 2 in the fifth row. And so next to vertex 5 on row 4 I put an arrow. There's going to be an arrow next to every vertex on one of the edges. Second theorem's matrix looks like that. And so if I look at them both at once, I can see they're clearly not rotated versions. These are two quite different patterns. We can also see that the first one there'll be three potential rotations. And the second one, if you think about it, there's 12. So I've actually got 15 of my 33 right here. But we can, in Mathematic I can use the graph automorphism group of the graph to find all the duplicates and weed them out. And the end result is I have four different matrices, different rank deficient matrices based on, based on the cube. Okay, well I've got two new new theorems I can generate. Here's a theorem based on that one, and here's a theorem based on that one. But I want more than two. So I thought, right, where can I find other rank deficient matrices? And let's work by analogy. I thought, well, let's think of matrices which also have a graph sitting behind them. Well, I know that I'm going to have three elements per row. So the graph that I'm going to use is going to have to be uniform degree three or cubic. These are well studied. On eight vertices I have five connected cubic graphs. So it was an easy thing to go in and just run my program, find all the possible minus two locations for these different graphs. And here's how many I found. None, none, 33, none and none. So I thought, well, why seems odd. Well, it turns out that a matrix with an underlying connected graph is rank deficient if and only if the matrix corresponding to any graph cycle has zero determinant and so you can order your rows and columns. The cycle's determinant looks like that. And so just thinking about how you used to compute determinants when you did them by hand, it's going to be that one times the determinant of this thing, so that's the product of all the A's, and then plus or minus, depending on how many you have to count along here, this one times the determinant of this thing here, which is the product of all the B's. So if N is even, the determinant is the difference between the product of the A's and the product of the B's. If N is odd, it's the sum, and with values 1, 1 and minus 2, you cannot have n odd and a zero determinant. So we can't have odd cycles. And even cycles have to contain the same number of minus twos among the A's as among the B's. So graphically that gives us this. For a rank deficient bisective matrix, we need. The graph has only cycles of even length, which is called a bicubic graph. And if you traverse any cycle, you encounter as many arrows in your direction of travel as going against it. So every time you go against an arrow, you add one. Every time you get one going with you, you subtract one and you have to add up to zero as you go around the arc. And you can verify that all four of those graphs have that property. So I need to look at other numbers than 8 if I want more rank division graphs. But I know I need to look for bicubic graphs. Four, there are no bicubic graphs. Six, there is one bicubic graph and it yields these two rank deficient matrices. Ten has two bicubic graphs and it yields nineteen rank deficient matrices. Twelve has these five bicubic graphs and it yields one hundred and forty six matrices. Fourteen has thirteen bicubic graphs and yields eight hundred seven matrices. Now, the problem is, once you get up to 13 or 14, you're getting rather complicated theorems. There's quite a few lines, but you can simplify the theorem. Once you got the complicated theorem, you can simplify it by merging lines. So, for example, this theorem we started with can generate this other simpler theorem by merging line 1 and 8. Then line 12 disappears and we end up with the combined line 1 and 8 being perpendicular to the baseline. In similar fashion, a theorem derived from this 10 row matrix, which is not too complicated, but it can be simplified by initially merging the isosceles triangle ADL into a single line and give us this second theorem. And then that third one can be created by merging the two red lines. Give us this, this one here. So the complicated ones can be made reasonably simpler. So I'm interested in going in generating new geometry diagrams. So I want to go from matrix to geometry. This matrix obviously creates this piece of geometry. But you can reinterpret the bisectors in different ways to get different forms of, of the same theorem, reinterpreting them as pure bisectors, as reflections, as cyclic polygons, and so forth. However, my little, my program is only going to choose one method. So all the theorems are going to look somewhat similar. What I'm going to do is I'm going to aim for cyclic polygons from the get go. They're useful because you can throw away all the spoke lines and make them implicit and so it keeps the clutter down. So the process looked a bit like this. We start with one of the matrices, identify cycles or even paths of sides which don't have any arrows on them. These are good candidates for spokes of a cyclic polygon. The neighboring edges on the graph become the sides of the cyclic polygon and any shared size like we have here and here become parallel constraints between the sides of the, of the cyclic polygon. And the final edge in this one is now states that the final two bisectors are the same or the same as long as you treat the same as meaning they have a fixed angle between them. Fixed angle in this case PI by 2. So here's what it does in code. My program, which first of all, it's going to create a little description, a little neutral description of the, of the theorem. It sends that in to get a textual description minus the conclusion. We then get a graphical form in the form of a geometric scene with the conclusion in red. We still don't actually have a value to the conclusion. We now create the geometric instance of that. And from the geometric instance I can actually extract what the conclusion is going to be. L2 is perpendicular to L1. In some cases the conclusion actually depends on the instance and not on the geometric scene itself because of the location of where that x axis is. And so such like actually it's not quite that, right? So random theorem generator just picks a rank deficient matrix at random, randomly merges pairs of columns, interprets that as a theorem, creates a statement without conclusion, creates a diagram, abandons the example and starts again. If this step takes too long, which it sometimes can, then Measures the conclusion angle from the diagram and completes the statement. Here is result of a run of this generating a bunch of theorems. Here's one that is generating a perpendicular. Here's one that generates a pair of parallel lines. It doesn't have to be perpendicular parallel. We'll see in this one. It's 67.5 degrees. That is of course PI by 3, PI by 8. It will have to be a binary rational of PI. This one is 45 degrees. And some of these clean up quite nicely. Let me show you that one expressed in terms of parallelograms and rectangle. That's a reasonable little theorem you might ask somebody to prove. Here's another one of the ones that came out of that run cleaned up where you're asking for an angle with a couple of parallelograms intersecting a circle. My personal favorite from that run is this one which starts with a general triangle and ends with a specific triangle. But unlike Napoleon or Morley or those guys, my specific triangle is not an equilateral, not even isosleason, not even got a single 90 degree angle in it. However, it is determined by the construction. So at that point I'd like to stop. I put the software, the functions on the. The functions attached somewhere to the, to the presentation. I'll just run it in case anyone's got any questions. We can actually get the excitement of seeing a new theorem popping up in front of us. So have a go with it if you like. It takes a couple of parameters. The second one is how long you're prepared to rate for the. Ah, there we go. It did generate a couple of theorems and that looks, yeah, it's quite a fun thing. Watch these things come out and see if you can find ones which you can express in a somewhat simpler, nicer way. So I will say thank you at that point and stop. Thank you.