Automated Drawings, Conjectures, and Proofs 
in Planar Geometry 
Using the Wolfram Language

Daniel McDonald
dmcdonald@wolfram.com

Wolfram Research Institute
Champaign, Illinois, USA

Join the Conversation #WolframTechConf

Overview of the Synthetic Geometry Project

Describe Scene

GeometricScene[]

Version 12.0 Experimental

"Scene description language" within the Wolfram Language framework allows users to symbolically describe coordinate-free scenes in plane geometry.

Draw Scene

RandomInstance[]

Version 12.0 Experimental

Turn scene descriptions into randomized drawings of those scenes.

Give visual representations of scenes.

Find coordinates for points that satisfy the scene.

Make Conjectures About Scene

FindGeometricConjectures[]

Version 12.0 Experimental

Using coordinates returned by scene drawer, make conjectures about original abstract scene.

Prove Theorems About Scene

FindGeometricProof[]

Not Version 12.0, but have code that works on simple examples

Give human-readable synthetic proofs of theorems that hold given the hypotheses of the original abstract scene.

Examples

Thales’ Theorem

Let A, B, and C be distinct points on a circle where the line AC is a diameter.
Then the angle ∠ABC is a right angle.

thalesHyp1 = GeometricScene[
{"A","B","C","O"},
{
CircleThrough[{"A","B","C"},"O"],
Triangle[{"A","B","C"}],
"O"==Midpoint[{"A","C"}]
}
];
thalesPic1=RandomInstance[thalesHyp1]

thalesHyp2 = GeometricScene[
{"A","B","C"},
{
TriangleCenter[Triangle[{"A","B","C"}],"Circumcenter"]==Midpoint[{"A","C"}]
}
];
thalesPic2=RandomInstance[thalesHyp2]

The input form is a GeometricScene[] object where the points are given concrete coordinates (and the scalar quantities, if any, are given concrete values).

InputForm[thalesPic1]

FindGeometricConjectures[] makes conjectures about the drawn scene based on the concrete values found by RandomInstance[].

thalesCon1=FindGeometricConjectures[thalesPic1];
thalesCon1["Conclusions"]

FindGeometricConjectures[thalesPic2]["Conclusions"]

Pappus’ Hexagon Theorem

Let {A, B, C}, and {D, E, F} be two sets of collinear points.
Then the intersection points X, Y, Z of line pairs AE and DB, AF and DC, BF and EC are collinear.

pappusHyps=GeometricScene[
{"A","B","C","D","E","F","X","Y","Z"},
{
Line[{{"A","B","C"},{"D","E","F"},{"A","X","E"},{"B","X","D"},{"A","Y","F"},{"C","Y","D"},{"B","Z","F"},{"C","Z","E"}}],
Style[InfiniteLine[{"X","Z"}],Red]
}
];
pappusPic=RandomInstance[pappusHyps,RandomSeeding->1]

FindGeometricConjectures[pappusPic]["Conclusions"]

Kosnita’s Theorem

Let ABC be an arbitrary triangle, O its circumcenter and Oa, Ob, Oc are the circumcenters of three triangles OBC, OCA, and OAB respectively. 
Then the three straight lines AOa, BOb and COc are concurrent.

kosnitaPic=RandomInstance[GeometricScene[
{"O","A","B","C","Oa","Ob","Oc","K"},
{
"O"==TriangleCenter[Triangle[{"A","B","C"}],"Circumcenter"],
"Oa"==TriangleCenter[Triangle[{"O","B","C"}],"Circumcenter"],
"Ob"==TriangleCenter[Triangle[{"A","O","C"}],"Circumcenter"],
"Oc"==TriangleCenter[Triangle[{"A","B","O"}],"Circumcenter"],
GeometricAssertion[{"A","K","Oa"},"Collinear"],
GeometricAssertion[{"B","K","Ob"},"Collinear"],
Style[InfiniteLine[{"C","Oc"}],Red]
}
],RandomSeeding->5]

FindGeometricConjectures[kosnitaPic]["Conclusions"]

Preview of FindGeometricProof[]

What is the measure of the angle ∠zuv in the diagram below?

scene1=GeometricScene[
{{"u","v","w","x","y","z"},{}},
{
GeometricAssertion[{InfiniteLine[{"x","y"}],InfiniteLine[{"z","w"}],InfiniteLine[{"u","v"}]},"MatchingParallel"],
InfiniteLine[{"x","z","u"}],
PlanarAngle[{"y","x","z"},"Counterclockwise"]==30Degree
}
];
drawnScene1=RandomInstance[scene1,RandomSeeding->1]

FindGeometricConjectures[drawnScene1]["Conclusions"]

FindGeometricProof[PlanarAngle[{"z","u","v"}]==_,scene1]

ProofObject[]

%["TwoColumnProof"]

({{"Fact", "Reason"}, {(RowWithSeparators[ || , " || ", ({{(RowDefault["x", "y"])}}), ({{(RowDefault["z", "w"])}}), ({{(RowDefault["u", "v"])}})]), "given"}, {(RowWithSeparators[ , " ", ({{(RowDefault["x", "z", "u"])}}), "is a line"]), "given"}, {(RowDefault["∠yxz", " == ", (QuantityPostfix[29.999999999999996`, "°", degrees, "AngularDegrees"])]), "given"}, {(RowDefault["∠yxu", " == ", (QuantityPostfix[29.999999999999996`, "°", degrees, "AngularDegrees"])]), (RowDefault["Since ", ({{(RowDefault["x", "z", "u"])}}), " are on a line, ", "∠yxu", " is just ", "∠yxz", " by another name, which is ", "\!\(\*TemplateBox[List[\"29.999999999999996`\", RowBox[List[\"\\[InvisibleSpace]\", \"\\\"\\[Degree]\\\"\"]], \"degrees\", \"\\\"AngularDegrees\\\"\"], \"QuantityPostfix\", Rule[SyntaxForm, Mod]]\)"])}, {(RowDefault["∠xzw", " == ", (QuantityPostfix[150.`, "°", degrees, "AngularDegrees"])]), (RowDefault["Since ", ({{(RowDefault["x", "y"])}}), " and ", ({{(RowDefault["z", "w"])}}), " are parallel lines, ", "∠xzw", " is ", "the supplement of", " ", "∠yxz"])}, {(RowDefault["∠wzu", " == ", (QuantityPostfix[29.999999999999993`, "°", degrees, "AngularDegrees"])]), "∠wzu is a supplementary angle to ∠xzw, which is \!\(\*TemplateBox[List[\"150.`\", RowBox[List[\"\\[InvisibleSpace]\", \"\\\"\\[Degree]\\\"\"]], \"degrees\", \"\\\"AngularDegrees\\\"\"], \"QuantityPostfix\", Rule[SyntaxForm, Mod]]\)"}, {(RowDefault["∠xuv", " == ", (QuantityPostfix[150.`, "°", degrees, "AngularDegrees"])]), (RowDefault["Since ", ({{(RowDefault["x", "y"])}}), " and ", ({{(RowDefault["u", "v"])}}), " are parallel lines, ", "∠xuv", " is ", "the supplement of", " ", "∠yxu"])}, {(RowDefault["∠zuv", " == ", (QuantityPostfix[150.`, "°", degrees, "AngularDegrees"])]), (RowDefault["Since ", ({{(RowDefault["x", "z", "u"])}}), " are on a line, ", "∠zuv", " is just ", "∠xuv", " by another name, which is ", "\!\(\*TemplateBox[List[\"150.`\", RowBox[List[\"\\[InvisibleSpace]\", \"\\\"\\[Degree]\\\"\"]], \"degrees\", \"\\\"AngularDegrees\\\"\"], \"QuantityPostfix\", Rule[SyntaxForm, Mod]]\)"])}})

Finding implicit assumptions in theorem statements

Finsler-Hadwiger Theorem

Suppose ABCD and AB'C'D' are two squares with common vertex A. Let Q and S be the midpoints of B' D and D' B respectively, and let R and T be the centers of the two squares. 
Then the quadrilateral QRST is a square as well.

Drawing the scene as described

No mention in the written statement that squares ABCD and AB'C'D' have to have the same orientation, but...

fhBadPic=RandomInstance[GeometricScene[
{"D","C","B","A","D'","C'","B'","Q","R","S","T"},
{
p1==Polygon[{"D","C","B","A"}],
p2==Polygon[{"D'","C'","B'","A"}],
GeometricAssertion[{p1,p2},"Regular"],
"Q"==Midpoint[Line[{"B'","D"}]],
"S"==Midpoint[Line[{"B","D'"}]],
"R"==Midpoint[{"A","C"}],
"T"==Midpoint[{"A","C'"}],
Style[Polygon[{"Q","R","S","T"}],Opacity[.4],Red]
}
],RandomSeeding->5]

... if they have opposite orientations, then quadrilateral QRST isn’t necessarily a square.

Select[FindGeometricConjectures[fhBadPic]["Conclusions"],Not@*FreeQ["Regular"]]

Adding the missing hypothesis

Now we add the assumption that the two original squares are both counterclockwise.

fhGoodPic=RandomInstance[GeometricScene[
{"D","C","B","A","D'","C'","B'","Q","R","S","T"},
{
p1==Polygon[{"D","C","B","A"}],
p2==Polygon[{"D'","C'","B'","A"}],
GeometricAssertion[{p1,p2},"Regular","Counterclockwise"],
"Q"==Midpoint[Line[{"B'","D"}]],
"S"==Midpoint[Line[{"B","D'"}]],
"R"==Midpoint[{"A","C"}],
"T"==Midpoint[{"A","C'"}],
Style[Polygon[{"Q","R","S","T"}],Opacity[.4],Red]
}
],RandomSeeding->1]

Paul Finsler and Hugo Hadwiger can rest in peace.

Select[FindGeometricConjectures[fhGoodPic]["Conclusions"],Not@*FreeQ["Regular"]]

Why we shouldn’t automatically give polygons same orientation

Other hypotheses might force two polygons to have opposite orientations, or ordering of vertices of polygons might be used for other purposes, like similarity mappings.

RandomInstance[GeometricScene[
{"A","B","C","D"},
{
p1==Style[Polygon[{"A","B","D"}],Red],
p2==Style[Polygon[{"B","D","C"}],Blue],
Area[p1]+Area[p2]==Area[Polygon[{"A","B","C","D"}]],
GeometricAssertion[{p1,p2},"Similar"]
}
],RandomSeeding->3]

Polygon Dissections

A perfect dissection of a polygon P is a decomposition of P into internally disjoint polygons (Subscript[P, 1]),...,(Subscript[P, n]) (1<n<∞) that are mutually similar but pairwise incongruent.

First Example

Here’s a triangle dissection by Andrzej Zak. The solution is unique and relies on special properties of the Plastic constant.

The scene drawer manages to draw it.

RandomInstance[GeometricScene[
{a,b,c,d,g,e,f},
{
p0==Polygon[{e,g,f}],
p1==Style[Polygon[{a,b,c}],Red],
p2==Style[Polygon[{b,c,d}],Green],
p3==Style[Polygon[{d,c,g}],Blue],
p4==Style[Polygon[{g,c,a}],Magenta],
p5==Style[Polygon[{e,d,b}],Cyan],
p6==Style[Polygon[{g,a,f}],Yellow],
GeometricAssertion[{p0,p1,p2,p3,p4,p5,p6},"Similar"]
}
],RandomSeeding->3]

Second Example

Here’s another very hard similar triangle construction, whose values are powers of Root[-1-((#1)^2)+((#1)^8)&,2].

Again, the scene drawer can handle it.

RandomInstance[GeometricScene[
{a,b,c,d,e,o},
{
Polygon[{a,b,c,d,e}],
p1==Style[Polygon[{a,b,o}],Red],
p2==Style[Polygon[{b,o,c}],Blue],
p3==Style[Polygon[{c,d,o}],Yellow],
p4==Style[Polygon[{d,o,e}],Purple],
p5==Style[Polygon[{e,o,a}],Orange],
GeometricAssertion[{p1,p2,p3,p4,p5},"Similar"]
}
],RandomSeeding->6]

New functions that can be used outside of GeometricScene

TriangleConstruct
"MedialTriangle", "AntimedialTriangle", "Triangle", 
"Cevian", "Altitude", "Median", "Symmedian", "AngleBisectingCevian", "OppositeSide", "Boundary",
"AngleBisector", "ExteriorAngleBisector", "PerpendicularBisector", "EulerLine", 
"Circumcircle", "Incircle", "Excircle", "NinePointCircle",
"Centroid", "Circumcenter", "Excenter", "Incenter", "NinePointCenter", "Orthocenter", "SymmedianPoint", "CevianEndpoint", "Foot", "Midpoint", "SymmedianEndpoint", "AngleBisectingCevianEndpoint"

TriangleMeasurement
"Area", "Perimeter", "Semiperimeter", "Circumradius", "Exradius", "ExteriorAngle", "FullExteriorAngle", "Height", "Inradius", "InteriorAngle", "NinePointRadius"

TriangleCenter
"Centroid", "Circumcenter", "Excenter", "Incenter", "NinePointCenter", "Orthocenter", "SymmedianPoint", "CevianEndpoint", "Foot", "Midpoint", "SymmedianEndpoint", "AngleBisectingCevianEndpoint"

Midpoint

PlanarAngle
"Proper", "Clockwise", "Counterclockwise"

PolygonAngle
"Interior", "Exterior", "FullExterior"

AngleBisector
"Interior", "Exterior"

PerpendicularBisector

Nine point circle

TriangleCenter[{{a1,a2},{b1,b2},{c1,c2}},"NinePointCenter"]

TriangleMeasurement[{{a1,a2},{b1,b2},{c1,c2}},"NinePointRadius"]

TriangleConstruct[{{a1,a2},{b1,b2},{c1,c2}},"NinePointCircle"]

tri={{-1,0},{2,0},{0,2}};
feet=TriangleConstruct[tri,{"Foot",All}];
midpoints=TriangleConstruct[tri,{"Midpoint",All}];
orthocenter=TriangleCenter[tri,"Orthocenter"];
orthoMidpoints=Point[Midpoint[{#,orthocenter}]]&/@tri;
ninePointCircle=TriangleConstruct[tri,"NinePointCircle"];
Graphics[{{Opacity[.1],Triangle[tri]},ninePointCircle,PointSize[Large],{Red,midpoints},{Blue,feet},{Yellow,orthoMidpoints}}]

Angles and bisectors

tri={{-1,0},{2,0},{0,2}};
Graphics[{Triangle[tri],Thickness[.01],
{Red,AngleBisector[tri]},
{Blue,AngleBisector[tri,"Exterior"]},
{Green,PerpendicularBisector[tri[[{1,2}]]]}
}]

PlanarAngle[tri]

PlanarAngle[tri,"Clockwise"]

PlanarAngle[tri,"Counterclockwise"]

PolygonAngle[Polygon[tri],1]/Degree

PolygonAngle[Polygon[tri],1,"Exterior"]/Degree

PolygonAngle[Polygon[tri],1,"FullExterior"]/Degree

More Constructions

tri={{-1,0},{2,0},{0,2}};
Graphics[{
{Blue,TriangleConstruct[tri,"AntimedialTriangle"]},
{Green,Triangle[tri]},
{Red,TriangleConstruct[tri,"MedialTriangle"]}
}]

Graphics[{Triangle[tri],{Red,TriangleConstruct[tri,{"Excircle", All}]}}]

Graphics[{{Opacity[.1],Triangle[tri]},
{Blue,TriangleConstruct[tri,{"Altitude",All}]},
{Yellow,PointSize[Large],TriangleConstruct[tri,"Orthocenter"]}
}]

Graphics[{{Opacity[.1],Triangle[tri]},
{Blue,TriangleConstruct[tri,"EulerLine"]},{Yellow,PointSize[Large],TriangleConstruct[tri,#]&/@{"Centroid","Orthocenter","Circumcenter","NinePointCenter"}}
}]

Thank you!

dmcdonald@wolfram.com

Rest of Synthetic Geometry Team:
Peter Barendse (FindGeometricProof[] developer)
Lin Cong (FindGeometricConjectures[] developer)
Ian Ford (design and documentation)
James Mulnix (design and technical help)
Michael Trott (design and technical help)

Test Suite Development:
Joe Chen
Ed Pegg
Marc Vredeveld

Graphics and Formatting:
Brett Champion
Lou D’Andria
Jeremy Davis
Tim Shedelbower

People whose lives we’ve made much more difficult:
Charles Pooh
Itai Seggev