Automated Planar Geometry

Dan McDonald
Peter Barendse
Jack Heimrath
Jeremy Stratton-Smith
WOLFRAM RESEARCH

(RowDefault[, (Spacer1), , (Spacer1), ])  #WolframTechConf

ABSTRACT

We present updates to the automated geometric functionality of the Wolfram Language introduced in Version 12, including new functionality for automated geometric reasoning and for creating GeometricScene objects.

INIT

SetDirectory[NotebookDirectory[]];
Get/@{"Load.m","SyntheticGeometryProofs.m","EquationalProof.m","AreaMethod.m"}
FindGeometricProof = PlaneGeometry`FindGeometricProof;

GeometricStylingRules

Overview

GeometricStylingRules is an option to GeometricScene that specifies how primitives are to be styled:

RandomInstance[GeometricScene[{a,b,c,o},{Triangle[{a,b,c}],CircleThrough[{a,b,c},o],o==Midpoint[{a,c}]},{PlanarAngle[{a,b,c}]==90 Degree},GeometricStylingRules->{"PointStyle"->{Black},"StylingPatterns"->{_CircleThrough->{Red}},"ConclusionStyle"->{Purple}}]]

Examples

Specify size and font for point labels

RandomInstance[GeometricScene[{a,b,c},{Triangle[{a,b,c}]},{},GeometricStylingRules->{"PointStyle"->Directive[PointSize[0.1],FontSize->40,FontFamily->"Comic Sans MS",Red]}]]

Remove point labels

RandomInstance[GeometricScene[{a,b,c},{Triangle[{a,b,c}]},{},GeometricStylingRules->{"PointStyle"->None}]]

Style Napoleon’s theorem with images of Le Petit Caporal himself

RandomInstance[
 Append[Entity["GeometricScene", "NapoleonsTheorem"]["Scene"], 
  GeometricStylingRules -> {"StylingPatterns" -> {_Triangle -> 
       PatternFilling[, 100]}}]]

Style Barrow's equality with smaller representations of itself

With[{s=Entity["GeometricScene","BarrowsEquality"]["Scene"]},Append[RandomInstance[s],GeometricStylingRules->{"StylingPatterns"->{_Triangle->PatternFilling[Rasterize[RandomInstance[s]],50]}}]]

Style a scene dynamically

RandomInstance[GeometricScene[{a,b,c},{Disk[a,EuclideanDistance[b,c]/2],Disk[b,EuclideanDistance[a,c]/2],Disk[c,EuclideanDistance[a,b]/2],Triangle[{a,b,c}]},GeometricStylingRules->{"StylingPatterns"->{_Triangle->Dynamic[PatternFilling[{"XGridPoint",RandomColor[]},RandomReal[{0,20}]],UpdateInterval->1],_Disk->Dynamic[PatternFilling[{"Grain",RandomColor[]},RandomReal[{0,20}]],UpdateInterval->1/Pi]}}]]

FindGeometricProof

Overview

Presented at the previous WTC, and still under development.

Produces a new ProofObject, containing a readable, “two column”, elementary level (US High School) proof of synthetic geometry facts, as well as graph representations and other proof properties.

Accepts GeometricScenes containing units and variables, as well as most geometry statements and constructions in guide/SyntheticGeometry.

Can prove a specific fact, anything matching a fact pattern (in the WL sense), or All facts.

To perform a proof step, it uses about one hundred theorems and definitions (which are inference rules of the form hypotheses :> conclusions), as well as algebra on length/area/angle measures. It can also accept a custom set of inference rules.

Each step contains an explanation that refers specifically to the hypotheses used in applying the theorem, and included a step number.

FindGeometricProof includes a rich options scheme, allowing you to:

Limit the facts returned by their number, complexity, and/or the number of proof steps needed.

Limit the time used and still return a ProofObject of what was proved.

Control the units of length/area/angle measures.

Use custom theorems.

Find the base length, in meters, of a triangle from the area and altitude and produce a classic two-column proof

scene = 
GeometricScene[{{"y","w","z","x"},{}},{Line[{"y","w","z"}],EuclideanDistance["x","w"]==(Quantity[3, "m", meters, "Meters"]),Area[Triangle[{"y","z","x"}]]==(Quantity[13, (("m")^2), meters squared, (("Meters")^2)]),PlanarAngle[{"y","w","x"},"Counterclockwise"]==90 °}];

pf=FindGeometricProof[EuclideanDistance["y","z"]==_,scene]

pf["Result"]

pf["ProofNotebook"]

Solve an advanced high school example using Ptolemy’s Theorem

PtolemysTheoremExample = 
GeometricScene[{{a,b,c,o},{}},
{
PlanarAngle[{b,a,c},"Counterclockwise"]==90°,
EuclideanDistance[b,a]==24,EuclideanDistance[c,a]==7,
CircleThrough[{a,b},o],
PlanarAngle[{c,o,b},"Counterclockwise"]==90°
},{}
];

RandomInstance[PtolemysTheoremExample]

proof = FindGeometricProof[EuclideanDistance[c,o]==_?NumericQ,PtolemysTheoremExample]

proof["Result"]

proof["ProofNotebook"]

Find the value of the golden ratio using similar rectangles

goldenScene = GeometricScene[{{"A","a","b","B","c","d"},{}},{
GeometricAssertion[{Polygon[{"A","a","b","B"}],Polygon[{"B","A","d","c"}]}, "Similar"], 
EuclideanDistance["A","B"]==EuclideanDistance["a","d"],GeometricAssertion[{Line[{"a","b"}],Line[{"A","B"}],Line[{"d","c"}]},"MatchingParallel"],GeometricAssertion[{Line[{"A","d","a"}],Line[{"B","c","b"}]},"MatchingParallel"],EuclideanDistance["A","a"]==3,PlanarAngle[{"A","a","b"},"Counterclockwise"]==Pi/2
}];

RandomInstance[goldenScene]

proof=PlaneGeometry`FindGeometricProof[
_==1/GoldenRatio,
goldenScene
]

proof["ProofNotebook"]

ProofObject[]["ProofGraphManipulate"]

The Area Method in the Wolfram Language

Overview

Using the area method in the Wolfram Language is a three step process:

Define a geometric construction via a sequence of Elementary Construction Steps.

Formulate a precise conjecture of the form (Subscript[E, 1])=(Subscript[E, 2]) (inequalities of the form ≤, <, ≥, >, ≠ are also acceptable), where (Subscript[E, 1]),(Subscript[E, 2]) are polynomials in geometric quantities of points defined in the geometric construction.

Use the VerifyConjecture function to prove whether the stated conjecture is a theorem within the geometric construction.

We have also implemented additional functions to facilitate visual exploration of constructions and conjectures.

Working Examples

British Flag Theorem

Let a, b, c, and d denote the vertices of a rectangle, and let p be any other point in the plane. Then ((OverBar[ap])^2)+((OverBar[cp])^2)=((OverBar[bp])^2)+((OverBar[dp])^2).

ClearAll[s2, s2, s3, s4];
RandomInstance@GeometricScene[
{a, b, c, d, p},
  	{
   		Style[Line[{a, p}], Blue],
   		Style[Line[{c, p}], Blue],
   		Style[Line[{b, p}], Orange],
   		Style[Line[{d, p}], Orange],
   		GeometricAssertion[Polygon[{a, b, c, d}], "Equiangular"]
   	}
  ]

Test the result numerically:

AreaMethodSceneExplorer[
	OnParallel[c,d,a,b,1]@OnPerp[d,a,b]@FreePoint[a,b,p],
	"Conjecture"->PythagoreanDifference[a,p,a]+PythagoreanDifference[c,p,c]==PythagoreanDifference[b,p,b]+PythagoreanDifference[d,p,d]
]

Find a proof:

VerifyConjecture[
	PythagoreanDifference[a,p,a]+PythagoreanDifference[d,p,d]==PythagoreanDifference[b,p,b]+PythagoreanDifference[c,p,c],
	OnParallel[d,c,a,b,1]@OnPerp[c,a,b]@FreePoint[a,b,p],
	"ProofNotebook"->True
]

It turns out that this theorem can be generalized in a slightly weaker form. For notational convenience we introduce the following function:

ClearAll[sumOfSquaredDistances];
sumOfSquaredDistances[p_, a_, b_, c_, d_] := PythagoreanDifference[a,p,a]+PythagoreanDifference[c,p,c]-(PythagoreanDifference[b,p,b]+PythagoreanDifference[d,p,d]);

Now, if we let the polygon abcd be any parallelogram, not just a rectangle, we find something interesting:

AreaMethodSceneExplorer[
	OnParallel[d,c,b,a,1]@FreePoint[a,b,c,p],
	"Conjecture"-> sumOfSquaredDistances[p, a, b, c, d]
]

We can see this more clearly if we consider the difference of the values of the sumOfSquaredDistances function for any two points p and q on the plane:

AreaMethodSceneExplorer[
	OnParallel[d,c,b,a,1]@FreePoint[a,b,c,p,q],
	"Conjecture"->sumOfSquaredDistances[p, a, b, c, d]-sumOfSquaredDistances[q, a, b, c, d]
]

As before, the proof turns out to be quite simple:

VerifyConjecture[
	sumOfSquaredDistances[p, a, b, c, d]-sumOfSquaredDistances[q, a, b, c, d]==0,
	OnParallel[d,c,b,a,1]@FreePoint[a,b,c,p,q],
	"ProofNotebook"->True
]

Hjelmslev’s Theorem

Hjelmslev’s Theorem states that if a set of collinear points {(Subscript[P, 1]),(Subscript[P, 2]),...} are isometrically mapped onto collinear points {(Subscript[Q, 1]),(Subscript[Q, 2]),...}, then the midpoints of the line segments {(Subscript[P, 1])(Subscript[Q, 1]),(Subscript[P, 2])(Subscript[Q, 2]),...} are also collinear. The “usual” proof of this result uses the classification of plane isometries. However, there are proofs which do not presuppose the parallel postulate of Euclidean geometry, which means this theorem holds non-Euclidean settings as well. One such proof is given below:

VerifyConjecture[
	Collinear[l,m,n],
	IsMidpoint[n, x, y]@IsMidpoint[m, b, d]@IsMidpoint[l, a, c]@OnLine[y, c, d, r]@OnLine[x, a, b, r]@FreePoint[a, b, c, d],
	"ProofNotebook" -> True
]

What’s New

Working With Angles

By allowing parameters to depend on previously defined points, we are now able to prove many theorems about angles. The angle bisector theorem – which states that if the line through a and e is the angle bisector of the angle ∠bac, then ((|be|)/(|ce|))=((|ba|)/(|ca|)) – is just one example:

RandomInstance@GeometricScene[{a,b,c,e},{Triangle[{a,b,c}],e∈AngleBisector[{b,a,c}],e∈Line[{b,c}]}]

VerifyConjecture[
	PythagoreanDifference[b,e,b]/PythagoreanDifference[c,e,c]==PythagoreanDifference[b,a,b]/PythagoreanDifference[c,a,c],
	IsIntersection[e,a,d,b,c]@OnParallel[d, c2, a, b, 1]@OnLine[c2,a,h,Sqrt[1+PythagoreanDifference[b,h,b]/PythagoreanDifference[a,h,a]]]@ECS3[h,b,a,c]@FreePoint[a, b, c],
	"ProofNotebook"->True,
	"UseAreaCoordinates"->True
]

Coq Parser

The area method was previously implemented in the Coq programming language, however that implementation is somewhat dated and not compatible with newer versions of Coq. Users familiar with the Coq area method package might find this tool particularly useful.

(* parallel transitivity *)
CoqParser[
	"forall A B C D X Y : Point,
	A <> B ->
	on_parallel X C A B ->
	on_parallel Y D C X ->
	parallel A B Y D /\\ parallel A B X C",
	"ProofNotebook"->True
]

Speed

On average, evaluation times for the VerifyConjecture function have decreased by a factor of ~10 compared to the version we demonstrated last year.

ClearAll[cevasTheorem,desarguesTheorem,ELTheorem,gaussNewtonLineTheorem,heronsFormula,interceptTheorem,midpointTheorem,menelausTheorem,pappusTheorem,pythagorasTheorem,triangleInequality];
cevasSetup=IsIntersection[f,c,p,a,b]@IsIntersection[e,b,p,a,c]@IsIntersection[d,a,p,b,c]@FreePoint[a,b,c,p];
cevasTheorem=((SignedDistance[a,f] SignedDistance[b,d]) SignedDistance[c,e])/((SignedDistance[f,b] SignedDistance[d,c]) SignedDistance[e,a])==1;
desarguesSetup=OnInterLineParallel[c2,a2,x,c,a,c]@OnInterLineParallel[b2,a2,x,b,a,b]@OnLine[x,a,a2]@FreePoint[a,b,c,a2];
desarguesTheorem=Parallel[b,c,b2,c2];
ELTheoreomSetup=IsCentroid[z,a,b,c]@IsOrthocenter[y,a,b,c]@IsCircumcenter[x,a,b,c]@FreePoint[a,b,c];
ELTheorem=Collinear[x,y,z];
gaussNewtonLineSetup=IsMidpoint[m3,x,y]@IsMidpoint[m2,a0,a2]@IsMidpoint[m1,a1,a3]@IsIntersection[y,a0,a1,a2,a3]@IsIntersection[x,a0,a3,a1,a2]@FreePoint[a0,a1,a2,a3];
gaussNewtonLineTheorem=Collinear[m1,m2,m3];
heroSetup=FreePoint[a,b,c];
heronsFormula=16 ((SignedArea[a,b,c])^2)==PythagoreanDifference[a,c,a] PythagoreanDifference[b,a,b]-((PythagoreanDifference[c,a,b])^2);
interceptSetup=IsIntersection[s,a,b,c,d]@OnParallel[d,b,a,c,r]@FreePoint[a,b,c];
interceptTheorem=((SignedDistance[s,a])/(SignedDistance[a,b]))==((SignedDistance[s,c])/(SignedDistance[c,d]));
midpointSetup=IsMidpoint[e,a,c]@IsMidpoint[d,b,c]@FreePoint[a,b,c];
midpointTheorem=Parallel[a,b,d,e];
menelausSetup=IsIntersection[f,x,y,a,b]@IsIntersection[e,x,y,a,c]@IsIntersection[d,x,y,b,c]@FreePoint[a,b,c,x,y];
menelausTheorem=((SignedDistance[a,f] SignedDistance[b,d]) SignedDistance[c,e])/((SignedDistance[f,b] SignedDistance[d,c]) SignedDistance[e,a])==-1;
pappusSetup=IsIntersection[z,B1,C2,B2,C1]@IsIntersection[y,A1,C2,A2,C1]@IsIntersection[x,A1,B2,A2,B1]@OnLine[C2,A2,B2]@OnLine[C1,A1,B1]@FreePoint[A1,A2,B1,B2];
pappusTheorem=Collinear[x,y,z];
pythagoreanSetup=OnPerp[c,a,b]@FreePoint[a,b];
pythagorasTheorem=PythagoreanDifference[c,a,b]==0;
triangleInequalitySetup=ECS1[a,b,c];
triangleInequality=(Sqrt[PythagoreanDifference[a,b,a]/2])+(Sqrt[PythagoreanDifference[b,c,b]/2])≥(Sqrt[PythagoreanDifference[c,a,c]])/2;
Grid[{{"Theorem","Area Coordinates","Time","Result"},Flatten@{"Ceva's Theorem","no",AbsoluteTiming[VerifyConjecture[cevasTheorem,cevasSetup]]},Flatten@{"Desargues' Theorem","no",AbsoluteTiming[VerifyConjecture[desarguesTheorem,desarguesSetup]]},Flatten@{"Euler Line","yes",AbsoluteTiming[VerifyConjecture[ELTheorem,ELTheoreomSetup,"UseAreaCoordinates"->True]]},Flatten@{"Gauss-Newton Line","yes",AbsoluteTiming[VerifyConjecture[gaussNewtonLineTheorem, gaussNewtonLineSetup,"UseAreaCoordinates"->True]]},Flatten@{"Heron's Formula","yes",AbsoluteTiming[VerifyConjecture[heronsFormula,heroSetup,"UseAreaCoordinates"->True]]},
Flatten@{"Intercept Theorem","no",AbsoluteTiming[VerifyConjecture[interceptTheorem,interceptSetup,"CheckParallelRatios"->True]]},Flatten@{"Midpoint Theorem","no",AbsoluteTiming[VerifyConjecture[midpointTheorem,midpointSetup]]},Flatten@{"Menelaus' Theorem","no",AbsoluteTiming[VerifyConjecture[menelausTheorem,menelausSetup]]},Flatten@{"Pappus' Line Theorem","no",AbsoluteTiming[VerifyConjecture[pappusTheorem,pappusSetup]]},Flatten@{"Pythagorean Theorem","no",AbsoluteTiming[VerifyConjecture[pythagorasTheorem,pythagoreanSetup]]},Flatten@{"Triangle Inequality","yes",AbsoluteTiming[VerifyConjecture[triangleInequality,triangleInequalitySetup,"UseAreaCoordinates"->True]]}},Frame->All,Alignment->{{Left,Center,Center,Center}}]

Old times:

A Tool for Constructing a GeometricScene

ResourceFunction["GeometricSceneConstructor"][]