There is a standard construction of a regular heptadecagon by H.W. Richmond (1893) (https://en.wikipedia.org/wiki/Heptadecagon ) (As anyone knows, it was Gauss who found out that it is possible to do this with a ruler and a compass. It is worth to be noted that he was 19 at the time and that this discovery was among the reasons why he has chosen mathematics rather then languages for a career.) For the sake of clarity, here is the diagram.

The construction works because (or if)

$$\angle AOP_3=\frac{3}{17}\cdot 2\pi.$$

Now, three questions.

Q1. Is it possible to prove this statement using Hilbert's axioms?

Q2. Is it possible to prove this statement using Tarski's axioms? (https://en.wikipedia.org/wiki/Tarski%27s_axioms)

Q3. What the proof, if written in the style of Euclid, may be like?

A few comments. First, it almost certainly does not matter *which* construction is chosen, but some choice it better to be made here. Second, first two questions are, in fact, reference requests. (Nobody doubts that the answer is yes.)
Finally, the last question is about history of mathematics. (Not an alternative history where the construction were discovered by ancient geometers, but the real one.) Invention of algebraic methods made possible nice proofs in place of cumbersome ones, and one may be curious about how much advantage it gives in comparison to the ancient geometric algebra.

upper, not alower, bound on the set of $n$ for which an $n$-gon is constructible.) $\endgroup$ – LSpice Jul 9 '18 at 16:07A formal system for Euclid's Elements), which states that every statement true in every ordered field closed under positive square roots is provable in Euclid'sElements. $\endgroup$ – Gro-Tsen Jul 10 '18 at 0:48