compass and straightedge constructions

Stream: Is there code for X?

[Tianchen Zhao]

Is there code for compass and straightedge constructions in matlib? Do we have all prerequisites to formalise it and prove theorems about it(eg imposibility to double to cube)? Did anyone work on this before? Thank you :)

[Kevin Buzzard]

We have all the algebra, ie we can prove Q(2^(1/3)) has degree 3 over Q so can't be in any field obtained by continually adjoining square roots. Translating this into a geometric statement is a different kettle of fish though