Automated Planar Geometry

Daniel McDonald
dmcdonald@wolfram.com

Peter Barendse
pbarendse@wolfram.com

Ian Ford
ianf@wolfram.com

Lin Cong
lcong@wolfram.com

Xiaofan Zhang
xiaofanz@wolfram.com

Michael Trott
mtrott@wolfram.com

James Mulnix
jmulnix@wolfram.com

Wolfram Research Institute
Champaign, Illinois, USA

Join the Conversation #WolframTechConf

Init

(*Quit[]*)

SetDirectory["/Users/pbarendse/kernel/StartUp/PlaneGeometry/"]

<<GeometrySceneDrawer.m
<<Midpoint.m
<<AngleBisector.m
<<PerpendicularBisector.m
<<TriangleData.m
<<GeometryConjecture.m

(*SetDirectory["C:\\Users\\dmcdonald\\kernel2\\kernel\\StartUp\\Graphics\\"]
Unprotect[Typeset`ReleaseHold]
Unprotect[Graphics]
Unprotect[Typeset`ResolveTicks]
<<GraphicsFormat.m*)

Overview of the Synthetic Geometry Project

Describe Scenes

GeometricScene[]

Version 12.0 Experimental

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

Version 12.1 Experimental

Adding capabilities for representing constructions and moving points dynamically. Expanding scope of supported geometric statements.

Draw Scenes

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 Scenes

FindGeometricConjectures[]

Version 12.0 Experimental

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

Prove Theorems About Scenes

FindGeometricProof[]

Version 12.1 Experimental

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

Access Curated Scenes from Classical Geometry

EntityValue[“GeometricScene”, “Entities”]

Version 12.1 Experimental

Query information about famous theorems and constructions from Euclid and beyond, including their GeometricScene representations.

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[].

FindGeometricConjectures[thalesPic1]

FindGeometricConjectures[thalesPic2,PlanarAngle[_]==_]["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"}
}]
}
];
pappusPic=RandomInstance[pappusHyps,RandomSeeding->1]

FindGeometricConjectures[pappusPic]

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"},
{
"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"],
Line[{{"A","Oa"},{"B","Ob"},{"C","Oc"}}]
}
],RandomSeeding->6]

FindGeometricConjectures[kosnitaPic]

Solve for an Unknown Radius

Specify a scene with four pairwise tangent circles where the three largest circles have radii of 357, 221 and 340, respectively.

RandomInstance[GeometricScene[
{{a,b,c,d},{rad}},
{
EuclideanDistance[a,b]==357,
EuclideanDistance[b,c]==221,
EuclideanDistance[a,c]==340,
GeometricAssertion[{Circle[a,238],Circle[b,119],Circle[c,102],Circle[d,rad]},"PairwiseTangent"]
}
]]

Solve for the radius of the fourth circle.

Replace[rad,%["Quantities"]]

Constructions from Euclid’s Elements

Proposition 1 of Book I of Euclid’s Elements states that given any two points a and b, one can construct an equilateral triangle having a and b as two of its vertices. In particular, draw two circles centered at a and b, respectively, whose radii are equal to the distance between them. Then their point of intersection c forms the third vertex of such an equilateral triangle.

RandomInstance[GeometricScene[
{a,b,c},
{
CircleThrough[{b,c},a],
CircleThrough[{a,c},b],
Style[Triangle[{a,b,c}],Pink]
}
]]

GeometricScene[] can now represent explicit step-by-step constructions.

RandomInstance[GeometricScene[
{{a,b,c},{d}},
{
{
EuclideanDistance[a,b]==d
},
{
cir1==Circle[a,d],
cir2==Circle[b,d]
},
{
c∈cir1,
c∈cir2
},
{
Style[Triangle[{a,b,c}],Pink]
}
}
]]

Proposition 22 of Book I generalizes Proposition 1 by stating that for any positive quantities r, s and t, such that max(s,t)≤r<s+t, there is a triangle having side lengths r, s and t.

Randomly choose positive quantities r, s and t, such that max(s,t)≤r<s+t.

{s,t}=RandomReal[10,2]

r=RandomReal[{Max[s,t],s+t}]

The construction proceeds as follows: construct a straight line through the points d, f, g and h in order, with d and f distance r apart, f and g distance s apart and g and h distance t apart. Draw the circle centered at f going through d, as well as the circle centered at g going through h. If k is one of the points where these circles intersect, then f is distance r from k, f is distance s from g and g is distance t from k. Thus the points f, g and k form such a triangle.

RandomInstance[GeometricScene[
{d,f,g,h,k},
{
{
Line[{d,f,g,h}],
EuclideanDistance[d,f]==r,
EuclideanDistance[f,g]==s,
EuclideanDistance[g,h]==t
},
{
CircleThrough[{d,k},f],
CircleThrough[{k,h},g]
},
{
Style[Triangle[{f,g,k}],Pink]
}
}
]]

PlaneGeometry`SyntheticGeometryProofsDump`mPrint = False;

A Preview of FindGeometricProof[ ] : Generating synthetic proofs accessible to 9th - grade geometry students

I was lucky enough to be tasked with creating something...
	- that could potentially be used in WolframAlpha, 
	- that would take 9th-grade level geometry questions as input (in natural language/diagram, eventually)
	- and output a synthetic proof of the type students understand and even expect.
	
For these reasons, we constructed what I call a “naive” prover: rather than start with Tarski’s axioms for geometry, or implementing the area method of Wu, et. al., our internal mechanism, and everything else reflect the needs of high-school level geometry, while still, I believe, being powerful enough to be of interest to others.

Drawbacks of a “naive” prover:
	- doesn’t handle degeneracy easily (but this is true of 9th grade geometry class)
	- unclear issues of theory/completeness/decidability 

Advantages of the “naive” prover: 
	- more precise control over what can be proved, and how long it takes
	- no need to translate into readable proofs
	- proofs are very similar to the ones given in a traditional 9th-grade geometry class

Precursor/Model of the Prover : FindEquationalProof[ ]

proof=FindEquationalProof[(Subscript[∀, x])f(g(x))==g(f(x)),(Subscript[∀, x])f(x)==g(x)]

proof["ProofNotebook"]

proof["ProofGraph"]

A Basic Problem

basicProblem=GeometricScene[{{"x","y","z","w"},{}},{
GeometricAssertion[{Line[{"x","y"}],Line[{"z","w"}]},"MatchingParallel"],
PlanarAngle[{"y","x","z"},"Counterclockwise"]==30 °
}];

RandomInstance[basicProblem]

proof=FindGeometricProof[
PlanarAngle[{"w","z","x"},"Clockwise"]==150 Degree,
basicProblem
]

proof["Properties"]

proof["ProofDataset"](*a computable version, easily ported back to, say, RandomInstance[]*)

proof["ProofNotebook"](*note: styling TBD*)

proof["Result"]

proof["ProofGraph"] (*note: styling TBD*)

A Harder 9th Grade Geometry Problem

We can also omit the first argument, and just prove everything we can. Here, the prover finds “all” the lengths (but not the radius of the circle):

RandomInstance[
myDrawing = GeometricScene[{{"x1","x2","x3","y2","z2","c","y1"},{r}},
{
GeometricAssertion[{Line[{"x1","x2","x3"}],CircleThrough[{"x2","y2","z2"},"c",r]},"Tangent"],GeometricAssertion[{Line[{"y1","y2","x3"}],CircleThrough[{"x2","y2","z2"},"c",r]},"Tangent"],GeometricAssertion[{Line[{"x1","z2","y1"}],CircleThrough[{"x2","y2","z2"},"c",r]},"Tangent"],
EuclideanDistance["x2","x3"]==1.9,
EuclideanDistance["x3","y1"]==2.9,
EuclideanDistance["y1","x1"]==1.8
}
]
]

tt=FindGeometricProof[myDrawing]

(note that FindGeometricProof[Automatic, myDrawing] works the same way)

tt["ProofNotebook"]

A Harder Example : finding an implicit Rectangle/Area

In Wolfram Language, the hypotheses of the requested proof are:

scene2 =GeometricScene[{{"\[FormalB]","b","c","d","\[FormalD]"}},{
PlanarAngle[{"\[FormalB]","b","c"},"Counterclockwise"]==90 °,PlanarAngle[{"b","c","d"},"Counterclockwise"]==90 °,PlanarAngle[{"c","d","\[FormalD]"},"Counterclockwise"]==90 °,EuclideanDistance["\[FormalB]","b"]==10,EuclideanDistance["b","c"]==20,EuclideanDistance["c","d"]==15,EuclideanDistance["d","\[FormalD]"]==8}];

We can ask for a proof of the area of the polygon we are interested in, even if we don’t specify the polygon in the exact same form as it is found:

pf = FindGeometricProof[HoldPattern[Area[Polygon[{"\[FormalD]","\[FormalB]","b","c","d"}]]]==_, scene2];

pf["Result"]

pf["ProofNotebook"]

pf["ProofGraph"]

You can also use FindGeometricProof on an existing ProofObject[], which is convenient if, for example, you want to quickly prune an existing proof object to target a (different) fact

pf2=FindGeometricProof[scene2, TimeConstraint->5]

pf2["ProofGraph"](* Proof Graph after 1 minute*)

More Functionality : Finding and Reconstructing Constructed Points, etc. (design TBD) :

pf2a = FindGeometricProof[Area[{_?(!StringQ[#]&),"b","c","d"}]==_, pf2]

pf2a["ProofNotebook"]

pf2a["ProofGraph"]

pf2a["AugmentedScene"](* puts proof conclusions back into a new GeometricScene[], possibly in steps *)

Find the Golden Ratio

goldenscene=GeometricScene[{{"A","a","b","B","c","d"},{}},{
GeometricAssertion[{Polygon[{"A","a","b","B"}],Polygon[{"A","B","c","d"}]}, "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"]==90 Degree
}];

N[1/GoldenRatio]

FindGeometricProof[_==1/GoldenRatio,goldenscene]["ProofNotebook"] (*~30sec*)

Prove Thales' Theorem

The prover relies on about 30 axiom - patterns ("theorems"/"lemmas" in a textbook). However, it can prove some classic theorems as well, which aren' t currently included :

thales=
GeometricScene[{{"a","b","c","o"},{β,γ, r}},
{CircleThrough[{"b","a","c"},"o",r],
Line[{"a","o","c"}],
PlanarAngle[{"a","b","c"}, "Counterclockwise"]==β,
PlanarAngle[{"b","c","a"}, "Counterclockwise"]==γ}
];

thales//RandomInstance

ttt=FindGeometricProof[PlanarAngle[{"c","b","a"},_]==_?NumericQ,thales] (*~20 sec*)

ttt["TwoColumnProof"]

Notice the algebra here is done in one step, by the full WL logico - algebraic prover (i.e., Reduce[])

Challenging Example : Classic Gears-and-Chain Problem

In this case, the prover doesn’t construct the point “e”, but if you just “point” in the right direction, it will find the answer:

diagram=GeometricScene[{{"b","e","k","a","c"},{}},
{
Line[{"b","e","k"}],
GeometricAssertion[{InfiniteLine[{"a","b"}],InfiniteLine[{"c","e"}]},"MatchingParallel"],
CircleThrough[{"a"},"c",5],CircleThrough[{"b"},"k",15],
EuclideanDistance["a","b"]==29,
PlanarAngle[{"c","a","b"},"Counterclockwise"]==90 °,PlanarAngle[{"a","b","k"},"Counterclockwise"]==90 °
},{}];

RandomInstance@diagram

gearsPf=FindGeometricProof[EuclideanDistance["c","k"]==_,diagram]

gearsPf["TwoColumnProof"]

gearsPf["ProofGraph"]

Curated Scenes

We have curated 261 famous scenes from classical geometry for the Wolfram Knowledgebase:

EntityValue["GeometricScene","EntityCount"]

Each scene is represented as an Entity. A complete list can be obtained through EntityValue:

EntityValue["GeometricScene","Entities"]//Short

A random sample of entities can be obtained using RandomEntity or through EntityValue:

EntityValue["GeometricScene",{"RandomEntities",5}]

Entity Classes

Entity classes represent collections of entities with some common characteristics. We provide a few named entity classes:

EntityValue["GeometricScene","EntityClasses"]

Obtain a list of scenes coming from Euclid’s Elements:

EntityValue[EntityClass["GeometricScene","EuclidsElements"],"Entities"]

Properties of a Scene

Each type of entity has a list of supported properties. The properties for the “GeometricScene” entity type can be obtained through EntityValue:

EntityValue["GeometricScene","Properties"]

The most important property here is the “Scene” property, which gives a GeometricScene object:

scene=EntityValue[Entity["GeometricScene","ThalesTheorem"],"Scene"]

This GeometricScene object can be passed to functions like RandomInstance, FindGeometricConjectures, and FindGeometricProof discussed earlier:

RandomInstance[scene]

FindGeometricConjectures[scene]

Properties of a Scene cont’d...

Some entities have more than one representation as a GeometricScene. These are given by the “AlternateScenes” property:

EntityValue[Entity["GeometricScene","AAATheorem"],"AlternateScenes"]

Each scene also has a natural language description given by the “Statement” property:

EntityValue[Entity["GeometricScene","DesarguesTheorem"],"Statement"]

And some have more than one way of stating them:

EntityValue[Entity["GeometricScene","DesarguesTheorem"],"AlternateStatements"]

Bibliographic and Historical Properties

We have curated information on who the original formulators of the scenes were, where available:

EntityValue[Entity["GeometricScene","Droz-FarnyTheorem"],"Formulators"]

Ask for the date of formulation:

EntityValue[Entity["GeometricScene","Droz-FarnyTheorem"],"FormulationDates"]

In the case of theorems, the provers of the theorem may not be the same as the formulators:

EntityValue[Entity["GeometricScene","Droz-FarnyTheorem"],"Provers"]

We can similarly ask for the proof dates:

EntityValue[Entity["GeometricScene","Droz-FarnyTheorem"],"ProofDates"]

The property “EponymousPeople” can be used to get a list of people the scene is named after, if any:

EntityValue[Entity["GeometricScene","Droz-FarnyTheorem"],"EponymousPeople"]

If a scene has an article on MathWorld or is the topic of any interactive demonstrations from the Wolfram Demonstrations Project, these can be obtained from the “MathWorld” and “RelatedDemonstrations” properties:

EntityValue[Entity["GeometricScene","Finsler-HadwigerTheorem"],"MathWorld"]

(Entity["Finsler\[Hyphen]Hadwiger theorem", Entity["MathWorld","Finsler-HadwigerTheorem"], "Entity[\"MathWorld\", \"Finsler-HadwigerTheorem\"]", "MathWorld topic"])

EntityValue[Entity["GeometricScene","Finsler-HadwigerTheorem"],"RelatedDemonstrations"]

{(Entity["Finsler-Hadwiger Theorem", Entity["WolframDemonstration","1701af47"], "Entity[\"WolframDemonstration\", \"1701af47\"]", "Wolfram demonstration"])}

(Entity["Finsler-Hadwiger Theorem", Entity["WolframDemonstration","1701af47"], "Entity[\"WolframDemonstration\", \"1701af47\"]", "Wolfram demonstration"])["Manipulate"]

Thank You!