ORIGINAL ARTICLE: Todd, P., Aley, D. A program to create new geometry proof problems. Ann Math Artif Intell (2023). https://doi.org/10.1007/s10472-023-09854-1​
Wolfram Technology Conference 2022: https://www.wolfram.com/broadcast/video.php?c=511&p=5&disp=list&v=3801
Article Abstract: In a previous paper Todd (Submitted to AMAI, 2022), linear systems corresponding to sets of angle bisector conditions are analyzed. In a system which is not full rank, one bisector condition can be derived from the others. In that paper, we describe methods for finding such rank deficient linear systems. The vector angle bisector relationship may be interpreted geometrically in a number of ways: as an angle bisector, as a reflection, as an isosceles triangle, or as a circle chord. A rank deficient linear system may be interpreted as a geometry theorem by mapping each vector angle bisector relationship onto one of these geometrical representations. In Todd (Submitted to AMAI, 2022) we illustrate the step from linear system to geometry theorem with a number of by-hand constructed examples. In this paper, we present an algorithm which automatically generates a geometry theorem from a starting point of a linear system of the type identified in Todd (Submitted to AMAI, 2022). Both statement and diagram of the new theorem are generated by the algorithm. Our implementation creates a simple text description of the new theorem and utilizes the Mathematica GeometricScene to form a diagram.

Introduction

We present a method for automatically generating new geometry theorems, suitable for solution using “angle chasing”. Specifically, we consider geometry theorems whose premises and conclusion comprise a set of bisector conditions. Each premise and the conclusion can be represented as the rows of a “bisector matrix”: one whose rows contain 1,1,-2 as their only non-zero entries. The existence of a theorem corresponds to rank deficiency in this matrix.
We initially consider rank deficient matrices which have an underlying graph, whose vertices correspond to matrix rows and whose edges correspond to matrix columns. We give each edge of the graph (considered in a specific direction) a head-weight equal to the matrix entry in the row corresponding to the vertex adjacent to its head and column corresponding to the edge. Similarly we give the edge a tail-weight. With this definition, a bisector matrix with underlying graph is rank deficient if and only if the graph is bicubic and for any cycle the product of head weights equals the product of tail weights. We present a Mathematica program which uses this characterization to identify all possible such matrices for 14 or less rows.
We present methods of transforming the rank deficient matrices into forms which incorporate line angles in addition to bisectors, and which have columns of more than two non-zero entries, while retaining the rank deficiency. We present code which takes such transformed matrices as input and outputs geometry theorems in the form of GeometricScenes. (Full code and initializations are at the end of the post)

Angle Bisector Theorems

The reflection of the altitude of a triangle in its angle bisector passes through the circumcenter, as illustrated here
Though the description of the theorem has only one explicit mention of “bisector”, the reflection can be expressed as a bisector.
In addition, the circumcenter forms isosceles triangles with the triangle sides. The base of an isosceles triangle is perpendicular to its angle bisector.
This theorem can therefore be considered as an angle bisector theorem. 
We will present a method for discovering new such theorems. 

Angles of a triangle

​​Letthedirectionofavectorbeitsanglefromthepositivexdirection.​​Thentheanglebetweentwovectorsiseitherthedifferenceintheirdirections,orthatdifferenceplus2π.

Angle Bisectors

​ γ=
α+β
2
α+β-2γ=0

Isosceles Triangles

​ γ=
α+β
2
-
π
2
α+β-2γ=π

A Bisector Theorem

θ(
v
1
)+θ(
v
2
)-2θ(
v
5
)0
θ(
v
2
)+θ(
v
3
)-2θ(
v
6
)0
θ(
v
3
)+θ(
v
4
)-2θ(
v
7
)0
θ(
v
1
)+θ(
v
4
)-2θ(
v
8
)0
θ(
v
5
)+θ(
v
7
)-2θ(
v
9
)0
θ(
v
6
)+θ(
v
8
)-2θ(
v
9
)0
​​
1
1
0
0
-2
0
0
0
0
0
1
1
0
0
-2
0
0
0
0
0
1
1
0
0
-2
0
0
1
0
0
1
0
0
0
-2
0
0
0
0
0
1
0
1
0
-2
0
0
0
0
0
1
0
1
-2
θ
1
θ
2
θ
3
θ
4
θ
5
θ
6
θ
7
θ
8
θ
9

0
0
0
0
0
0
In[]:=
MatrixRank
1
1
0
0
-2
0
0
0
0
0
1
1
0
0
-2
0
0
0
0
0
1
1
0
0
-2
0
0
1
0
0
1
0
0
0
-2
0
0
0
0
0
1
0
1
0
-2
0
0
0
0
0
1
0
1
-2

Out[]=
5

Isosceles triangles

θ(
w
1
)+θ(
w
2
)-2θ(
w
5
)π
θ(
w
2
)+θ(
w
3
)-2θ(
w
6
)π
θ(
w
3
)+θ(
w
4
)-2θ(
w
7
)-π
θ(
w
1
)+θ(
w
4
)-2θ(
w
8
)π
θ(
w
5
)+θ(
w
7
)-2θ(
w
9
)0
θ(
w
6
)+θ(
w
8
)-2θ(
w
10
)0
θ(
w
10
)-θ(
w
9
)=π/2

Two Bisector Theorems

Both have rank 7 (out of a possible 8).
How many such matrices are there?
How many have rank 7?
33

Shape Graphs

Decorated Shape Graphs

Generalize matrix

Rank deficient matrices

Why?

Rank deficient matrix characterization (proof sketch)

Rank Deficient Bisector Matrices

We need these characteristics
◼
  • The graph only has cycles of even length (bicubic).
    • ◼
  • If you traverse any cycle, you encounter as many arrows in your direction of travel as against it

    • Merging sides

    Matrix->Geometry

    Finding New Theorems

    ◼
  • Create arrow-decorated graph of rank-deficient matrix.
    • ◼
  • Identify cycles of arrow-free edges.
    • ◼
  • Create cyclic polygons.
    • ◼
  • Add parallel constraints for sides which are shared .
    • ◼
  • Create a sequence of reflections / bisections along with parallel constraints to complete the description.

    • Random Theorem Generator

    ◼
  • Picks a rank-deficient matrix at random
    • ◼
  • Randomly merges pairs of columns (=merging lines).
    • ◼
  • Interprets as a theorem.
    • ◼
  • Creates statement (without conclusion)
    • ◼
  • Creates a diagram (abandons the example and starts again if this step takes too long) .
    • ◼
  • Measures “conclusion angle” from the diagram and completes statement.

    • Reinterpreted

    A little clean up can give more appealing statements of these theorems
    In the following theorem, regardless of initial triangle BDE, the construction yields a triangle with angles 45, 22.5, and 112.5 degrees.

    Random Theorem Generator

    Discover new geometry theorems with this tool. The first parameter specifies the number of theorems you want. The second parameter how many seconds you’d like to wait for a random instance of a new theorem to be created before it should be abandoned.
    The initial value defaults to 2, the second to 15.
    Theorems are all angle bisector theorems, expressed on cyclic polygons. The theorem statement involves cyclic polygons, parallelism, bisectors and reflections. The conclusion is the value of a particular angle.
    You may need to drag points on the scenes to get sufficient separation to appreciate the diagram. Just evaluate the following line to get five more theorems. Or ask for a hundred and leave it for an hour or two.

    CITE THIS NOTEBOOK

    A program to create new geometry proof problems​
    by Philip Todd​
    Wolfram Community, STAFF PICKS, June 23, 2023
    ​https://community.wolfram.com/groups/-/m/t/2942751