Refine Theorem Statements: Finsler–Hadwiger Theorem

RandomInstance and FindGeometricConjectures can be used to discover errors in the statement of a theorem. For example, the statement of the theorem may be missing an important hypothesis that keeps the theorem from holding in all cases.

Most statements of the Finsler–Hadwiger theorem are given as follows: Suppose and are two squares that share a vertex . Let and be the midpoints of and , respectively, and let and be the centers of the two squares. Then the quadrilateral is a square as well.

Represent these hypotheses as a GeometricScene.

As the generated scene plainly shows, the hypotheses are insufficient to guarantee that the quadrilateral is a square. FindGeometricConjectures will not find any conjectures about regular polygons.

Refine the hypotheses by adding the stipulation that and share a common orientation.

Now the search for conjectures about regular polygons will find the desired conclusion.