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.
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.
abstract 2D geometric scene defined by the hypotheses hypi in terms of the symbolic points pi
scene whose hypotheses depend on the symbolic scalar values ki
specific instance of a geometric scene with explicit coordinates for each point
collection of specific instances of a scene
scene together with some conclusions coni about it
combines several scene instances into one scene object
Geometric scenes can be visualized by finding a particular instance of the scene using RandomInstance.
find a random instance of a scene
find n instances
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:
infinite line bisecting the angle ∠ p q r
circle of radius r centered at the point p
circle passing through the points pi
sphere passing through the points pi
filled disk of radius r centered at the point p
half-infinite line, or ray, starting at the point p and passing through the point q
infinite line passing through the points p and q
sphere tangent to the sides of the triangle △ p1 p2 p3
line segment passing through the points pi, in that order
midpoint of the line segment p q
perpendicular bisector of the line segment p q
polygon with vertices pi
boundary of the region reg
centroid of the region reg
point closest to the point p in the region reg
triangle with vertices p, q and r
center of triangle △ p q r specified by spec
constructed geometric region defined by the triangle △ p q r specified by spec
2D regions supported in GeometricScene.
Hypotheses can also be geometric assertions or equations involving geometric quantities defined on elements of the scene.
arc length of the region reg
area of the region reg
Euclidean distance between the points p and q
perimeter of the region reg
the measure of the angle ∠ p q r
vertex angle of the polygon poly at the vertex p
distance from the point p to the region reg
measure of the region reg
signed distance from the point p to the region reg
measurement of the triangle △ p q r specified by spec
Geometric quantities supported by GeometricScene.
assertion that the point p is an element of the region reg
assertion that the regions/quantities xi are equal
assertion that the objects objs satisfy the property prop
step consisting of multiple hypotheses
assertion that the point p is a member of the region reg
Assertions supported by GeometricScene.
GeometricScene also supports style:
specify a style
style all structures matching a pattern
Specifying styles within GeometricScene.
The Wolfram Language can use these scene descriptions to find conjectures that may hold for a geometric scene.
find conjectures that might hold for scene
find conjectures that might hold for the instances scenei
find conjectures of the form patt
find up to n conjectures