Straightedge and compass construction in Lean

This project formalizes some basic theory of straightedge and compass construction in Lean, including a prove of theorem #8 from Freek Wiedijk's list of 100 theorems.

Main declarations

• EuclideanGeometry.ConstructiblePoint: predicate for constructible points using straightedge and compass.
• constructibleClosure: constructible closure of a field. That is, the union of all iterated quadratic extensions of th field.
• EuclideanGeometry.ConstructiblePoint.mem_constructibleClosure: constructible points on the complex plane are in the constructible closure.
• EuclideanGeometry.constructiblePoint_of_mem_constructibleClosure: constructible numbers are all constructible points
• EuclideanGeometry.not_exist_angle_trisection: the impossibility of trisecting the angle. (Wiedijk #8)
• EuclideanGeometry.not_exist_doubling_cube: the impossibility of doubling the cube. (Wiedijk #8)
• EuclideanGeometry.mohr_mascheroni_point: Mohr–Mascheroni theorem (straightedge is redundant)
• EuclideanGeometry.constructible_polygon: Gauss–Wantzel theorem (constructibility of regular polygons)

Comparator setup

The comparator.json setup currently only verifies the two Wiedijk #8 theorems. There isn't a technical reason to set up for other theorems and I am just lazy.