Synthetic Geometry

The Wolfram Language provides not only extensive support for analytic geometry, but also support for the symbolic representation of synthetic geometry scenes in a form suitable for automated coordinate-independent reasoning.

Scene Representation and Visualization

Synthetic geometry scenes are represented in the Wolfram Language with GeometricScene. Scenes contain parameters representing named points and quantities, as well as hypotheses consisting of symbolic 2D regions and assertions involving those parameters. Conclusions can also be added to represent geometric theorems or conjectures that those hypotheses entail. Particular instances of a scene can be represented by specifying coordinates and values for all of the parameters appearing in the scene. Multiple instances of the same scene can be represented with a single GeometricScene object.

GeometricScene[{p1,p2,},{hyp1,hyp2,}]abstract 2D geometric scene defined by the hypotheses hypi in terms of the symbolic points pi
GeometricScene[{{p1,p2,},{k1,k2,}},hyps]scene whose hypotheses depend on the symbolic scalar values ki
GeometricScene[{p1{x1,y1},p2{x2,y2},},hyps]specific instance of a geometric scene with explicit coordinates for each point
GeometricScene[{{p1{x11,y11},},{p1{x21,y21},},},hyps]collection of specific instances of a scene
GeometricScene[,,{con1,con2,}]scene together with some conclusions coni about it
GeometricScene[{scene1,scene2,}]combines several scene instances into one scene object

Wrapper for geometric scenes.

The simplest geometric scenes consist of only a list of points and a list of hypotheses.

Here is a scene consisting of a circumscribed triangle with one side on the diameter:
In[1]:=
Click for copyable input

Geometric scenes can be visualized by finding a particular instance of the scene using RandomInstance.

RandomInstance[scene]find a random instance of a scene
RandomInstance[scene,n]find n instances

Function to find instances of a geometric scene.

This finds a random instance of the scene:
In[2]:=
Click for copyable input
Out[2]=
This finds several instances of the scene:
In[3]:=
Click for copyable input
Out[3]=

Many 2D regions can be used as hypotheses in a geometric scene. All regions appearing in the hypotheses of a geometric scene are assumed to be nondegenerate and are displayed in instances of that scene:

AngleBisector[{p,q,r}]infinite line bisecting the angle p q r
Circle[p,r]circle of radius r centered at the point p
CircleThrough[{p1,p2,}]circle passing through the points pi
Circumsphere[{p1,p2,p3}]sphere passing through the points pi
Disk[p,r]filled disk of radius r centered at the point p
HalfLine[{p,q}]half-infinite line, or ray, starting at the point p and passing through the point q
InfiniteLine[{p,q}]infinite line passing through the points p and q
Insphere[{p1,p2,p3}]sphere tangent to the sides of the triangle p1 p2 p3
Line[{p1,p2,}]line segment passing through the points pi, in that order
Midpoint[{p,q}]midpoint of the line segment p q
PerpendicularBisector[{p,q}]perpendicular bisector of the line segment p q
Point[p]point p
Polygon[{p1,p2,}]polygon with vertices pi
RegionBoundary[reg]boundary of the region reg
RegionCentroid[reg]centroid of the region reg
RegionNearest[reg,p]point closest to the point p in the region reg
Triangle[{p,q,r}]triangle with vertices p, q and r
TriangleCenter[{p,q,r},spec]center of triangle p q r specified by spec
TriangleConstruct[{p,q,r},spec]constructed geometric region defined by the triangle p q r specified by spec

2D regions supported in GeometricScene.

This is a more complex geometric scene:
In[4]:=
Click for copyable input
In[5]:=
Click for copyable input
Out[5]=

Hypotheses can also be geometric assertions or equations involving geometric quantities defined on elements of the scene.

ArcLength[reg]arc length of the region reg
Area[reg]area of the region reg
EuclideanDistance[p,q]Euclidean distance between the points p and q
Perimeter[reg]perimeter of the region reg
PlanarAngle[{p,q,r}]the measure of the angle p q r
PolygonAngle[poly,p]vertex angle of the polygon poly at the vertex p
RegionDistance[reg,p]distance from the point p to the region reg
RegionMeasure[reg]measure of the region reg
SignedRegionDistance[reg,p]signed distance from the point p to the region reg
TriangleMeasurement[{p,q,r},spec]measurement of the triangle p q r specified by spec

Geometric quantities supported by GeometricScene.

pregassertion that the point p is an element of the region reg
x1assertion that the regions/quantities xi are equal
GeometricAssertion[objs,prop]assertion that the objects objs satisfy the property prop
RegionMember[reg,p]assertion that the point p is a member of the region reg

Assertions supported by GeometricScene.

This is the scene description for Brahmagupta's theorem:
In[6]:=
Click for copyable input
Out[7]=

GeometricScene also supports style:

Style[objs,opts]specify a style

Specifying styles within GeometricScene.

Find a perfect polygon dissection:
In[8]:=
Click for copyable input
Out[8]=

Finding Conjectures

The Wolfram Language can use these scene descriptions to find conjectures that may hold for a geometric scene.

FindGeometricConjectures[scene]find conjectures that might hold for scene.
FindGeometricConjectures[{scene1,scene2,}]find conjectures that might hold for the instances scenei
FindGeometricConjectures[scenes,patt]find conjectures of the form patt
FindGeometricConjectures[scenes,patt,n]find up to n conjectures

Function to find conjectures for a geometric scene.

Discover Thales's theorem:
In[9]:=
Click for copyable input
In[10]:=
Click for copyable input
Out[10]=
In[11]:=
Click for copyable input
Out[11]=
Discover Brahmagupta's theorem:
In[12]:=
Click for copyable input
In[13]:=
Click for copyable input
Out[13]=
In[14]:=
Click for copyable input
Out[14]=
Discover Pappus's hexagon theorem:
In[15]:=
Click for copyable input
In[16]:=
Click for copyable input
Out[16]=
In[17]:=
Click for copyable input
Out[17]=
Discover Kosnita's theorem:
In[18]:=
Click for copyable input
In[19]:=
Click for copyable input
Out[19]=
In[20]:=
Click for copyable input
Out[20]=
Discover the FinslerHadwiger theorem:
In[21]:=
Click for copyable input
In[22]:=
Click for copyable input
Out[22]=
In[23]:=
Click for copyable input
Out[23]=