# Automated Detection of Interesting Properties in Regular Polygons

## Abstract

We demonstrate a systematic, automated way of discovery of a large number of new geometry theorems on regular polygons. The applied theory includes a formula by Watkins and Zeitlin on minimal polynomials of $$\cos \frac{2\pi }{n}$$, and a method by Recio and Vélez to discover a property in a plane geometry construction. This method exploits Wu’s idea on algebraizing the geometric setup and utilizes the theory of Gröbner bases. Also a bijective function is given that maps the investigated cases to the first natural numbers. Finally, several examples are shown that are all previously unknown results in planar Euclidean geometry.

## Introduction

Obtaining interesting mathematical theorems automatically is a dream of many mathematicians. By defining a formal language (with its logical axioms) on a research field, and a set of (non-logical) axioms, one can deduce various statements only by the repeated application of inference rules to the axioms. In principle, proofs for all propositions in a research field can be traced back to consecutive uses of the axioms.

Several axiomatizations are available for many research fields in mathematics, however, interesting theorems (with proofs) are more difficult to find. One problem is that combining certain inference rules to the axioms usually produces an unmanageable big database of propositions, including trivial or uninteresting ones. There is already remarkable work done in this field, including  which is one of the first reports, and, in particular, producing proofs in elementary planar geometry, we refer to [1, 3, 5] where the combinatorial explosion is also addressed. The other problem is to identify which propositions are interesting enough to call them theorems, here we refer the reader to [6, 9].

In this paper we limit our considerations to planar Euclidean geometry, namely to find interesting properties in a regular polygon. The literature on listing such properties is, actually, huge, including constructible polygons (by compass and straightedge or origami, for example). In fact, from the very start of the availability of computer algebra systems (CAS) and dynamic geometry software (DGS), namely, the 1990s, non-constructible polygons can also be better observed, either numerically or symbolically. One example is Karst’s statement (Fig. 1) that claims parallelism of segments OB and JM in a regular nonagon, constructed with Mathematica in http://mathworld.wolfram.com/RegularNonagon.html by citing  (see also https://www.geogebra.org/m/AXd5ByHX#material/x5u93pFr for a freely available online resource). Such theorems are, however, difficult to find in the literature, and they seem hard to discover in a purely mechanical way.

In this study we deal with a simple geometric system. We consider the following “axioms”:

1. 1.

A regular n-gon with vertices (0, 0) and (1, 0) is given. The vertices of the regular n-gon are called points.

2. 2.

A connection of two points is called a segment.

3. 3.

Intersection point of two segments is considered as a point. (The segments can be lengthened to form a line if the segments are not intersecting.)

By using the last two “axioms” again and again, we can construct a large set of new points and segments. When considering all possible segments defined in this way, we can compute the lengths of them symbolically, and, depending on the “simplicity” of the symbolic result we classify the segment either as “interesting” or “not interesting”. This is, of course, somewhat subjective, but this approach can be slightly modified later by allowing other results interesting enough, or by defining some other points as well for the domain of interest.

In this paper the application of the last two “axioms” will be limited to a certain number. This will limit our considerations, but the obtained results will be still interesting.

The paper consists of the following parts: In Sect. 2 the mathematical background is explained on computing a given segment symbolically. Section 3 presents some manually obtained new results. Section 4 demonstrates how the mathematical computations can be automated by using the symbolic tool RegularNGons and its numerical counterpart. Finally, Sect. 5 depicts some future ideas.

The papers [17, 18] can provide more information on the topic. Also, to recall some fundamental ideas, without any further notices we will refer to  which has a similar structure like this paper has, however, we will communicate several new ideas here—most importantly some new possible parameters in Sect. 4.2, a report on the availability of a numerical study tool in Sect. 4.3, a formal description in Sect. 4.5 with proofs, and some detailed explanations in Examples 12 and 5. Furthermore, very recent results are shown in Sect. 4.7. Also, the list of references contains some updated items. Also a minor correction has been added on the structure of the obtained polynomials in Sect. 3.2.

In this paper we give a collection of theorems that are of geometric kind and related to a concrete setup of a regular polygon. Also, some propositions are discussed that contain preliminary knowledge or general correlations.

We remark that the “geometry theorems” we obtain in this article are related to lengths appearing in regular polygons. Therefore these results may also be considered as “algebraic theorems” because the lengths are always expressed by roots of algebraic equations. On the other hand, the method we use can be easily extended to focus on “more geometric” properties like perpendicularity or parallelism of the obtained segments. Also, combining some “algebraic theorems” we can even conclude congruency of triangles (see the third property in Theorem 3.4 in Sect. 2), among others. Finally, concurrency of lines can also be handled in a way that is described in Example 8.

## Mathematical Background

In this section we discuss the mathematical background on a possible method to handle regular polygons with means in algebraic geometry.

### Constructibility

The algebraization of the setup of a planar geometry statement is a well known process since the revolutionary book  of Chou’s. It demonstrates on 512 mathematical statements how an equation system can describe a geometric construction, and by performing some manipulations on the equation system, a mechanical proof can be obtained. Chou’s work was one of the first publicly available applications of Wu’s algebraic geometry method . It focuses mainly on constructible setups, that is, mostly on such constructions that can be created only by using the classic approach, namely by compass and straightedge. In addition, there is a proof on Morley’s trisector theorem presented which assumes a non-Euclidean, cubic way of being constructed, however, the explicit way of construction is successfully avoided, therefore the theorem is manageable. Also, Wu’s method was successfully used in theorems that cannot be constructed with compass and straightedge, see  for a recent example.

It is well known (Gauß, 1801, Wantzel, 1837, see [25, 27]) that a regular n-gon is constructible by using compass and straightedge if and only if n is the product of a power of 2 and any number of distinct Fermat primes (including none). We recall that a Fermat prime is a prime number of the form $$2^{2^m}+1$$. By using this theorem the list of the constructible regular n-gons are:

\begin{aligned} n=3, 4, 5, 6, 8, 10, 12, 15, 16, 17, 20, 24,\ldots \end{aligned}

A generalization of this result (Pierpont, 1895, see ) by allowing an angle trisector as well (for example, origami folding steps), is that a regular n-gon is constructible if and only if

\begin{aligned} n=2^r\cdot 3^s\cdot p_1\cdot p_2\cdots p_k, \end{aligned}

where $$r,s,k\ge 0$$ and the $$p_i$$ are distinct primes of form $$2^t\cdot 3^u+1$$ . The first constructible regular n-gons of this kind are

\begin{aligned} n=3, 4, 5, 6, 7, 8, 9, 10, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 24, \ldots \end{aligned}

From this second list the cases $$n=11$$, $$n=22$$ and $$n=23$$ are missing again, and, as a natural consequence, there are much less scientific results known on regular 11-, 22- and 23-gons than for n-gons appearing in the lists. Later we will show some—to our best knowledge—new results on the cases $$n=11$$ and $$n=23$$, among other ones.

### An Algebraic Formula for the Vertices

From now on we assume that $$n\ge 1$$. The cases $$n=1,2$$ have no geometrical meaning, but they will be useful from the algebraic point of view.

In the algebraic geometry approach the usual way to describe the points of a construction is to assign coordinates $$(x_i,y_i)$$ for a given point $$P_i$$ ($$i=0,1,2,\ldots$$). When speaking about a polygon, in many cases the first vertices are put into coordinates $$P_0=(0,0)$$ and $$P_1=(1,0)$$, and the other coordinates are described either by using exact rationals, or the coordinates are expressed as possible solutions of algebraic equations.

For example, when defining a square, $$P_2=(1,1)$$ and $$P_3=(0,1)$$ seem to make sense, but for a regular triangle two equations for $$P_2=(x_2,y_2)$$ are required, namely $$x_2^2+y_2^2=1$$ and $$(x_2-1)^2+y_2^2=1$$. This equation system has two solutions, namely $$x_2=\frac{1}{2},y_2=\frac{\sqrt{3}}{2}$$ and $$x_2=\frac{1}{2},y_2=-\frac{\sqrt{3}}{2}$$. It is well known that there is no way in the algebraic geometry approach to avoid such duplicates, unless the coordinates are rational. In other words, if both minimal polynomials of the coordinates are linear (or constant), then the duplicates can be avoided, otherwise not. Here, for $$x_2$$ we have $$x_2-\frac{1}{2}(=0)$$, but for $$y_2$$ the minimal polynomial is $$y_2^2-\frac{3}{4}(=0)$$.

In this paper we will find convenient to enlarge the notion of minimal polynomial by considering certain multiples of it, to have integer coefficients. That is, we will say that also $$2x_2-1$$ is a minimal polynomial of $$x_2=\frac{1}{2}$$, and similarly, $$4y_2^2-3$$ is a minimal polynomial of $$\frac{\sqrt{3}}{2}$$. The correspondence between them can be presented by calling them associates and using the notation $$x_2-\frac{1}{2}\sim 2x_2-1$$.

To express the coordinates of the vertices, minimal polynomial of $$\cos \frac{2\pi }{n}$$ will play an important role. The paper  suggests an algorithm to obtain the minimal polynomial $$p_c(x)$$ of $$\cos \frac{2\pi }{n}$$, based on the Chebyshev polynomials $$T_j(x)$$ of the first kind (see Algorithm 1—in our computations in this paper, however, we usually skip the division in the last step).Footnote 1

Assume we have an equation

\begin{aligned} p_c(x)=0. \end{aligned}
(2.1)

By considering the equation

\begin{aligned} x^2+y^2=1 \end{aligned}
(2.2)

as well, after eliminating x we can obtain a polynomial $$p_s(y)$$ such that $$p_s\left( \sin \frac{2\pi }{n}\right) =0$$. Table 1 shows the minimal polynomials for $$n\le 17$$ in the enlarged sense of definition.

It is clear, that—not considering the cases $$n=1,2,3,4,6$$—the number of roots of $$p_c$$ is more than one, therefore the solution of the equation system (2.1) and (2.2) is not unique. The number of solutions for (2.1) depends on the degree of $$p_c$$, and—not considering the cases $$n=1,2$$—the number of solutions for (2.2) is two for each root of $$p_c(x)$$, therefore the number of solutions for (2.1) and (2.2) is usually $$2\cdot \text {deg}(p_c)$$. As a result, the point

\begin{aligned} P=\left( \cos \frac{2\pi }{n},\sin \frac{2\pi }{n}\right) \end{aligned}

cannot be exactly determined by an algebraic equation in the algebraic geometry approach. Table 2 shows the degree of ambiguity for different values of n.

Actually, for the case $$n=4$$ we can find a better practical way than considering the Eqs. (2.1) and (2.2). The point $$P_2$$ can be described with the equations $$x_2=1, y_2=1$$. Here we can avoid using the quadratic Eq. (2.2) that introduces an unnecessary root for y.

Later we will show that Table 2 can be computed with Euler’s totient function as well, that is, the degree equals to $$\varphi (n)$$:

### Proposition 2.1

Let $$n>2$$. Then the equation system (2.1) and (2.2) has $$\varphi (n)$$ different solutions in (xy).

Now we are ready to set up additional formulas to describe the coordinates of the vertices of a regular n-gon, having its first vertices $$P_0=(0,0)$$ and $$P_1=(1,0)$$, and the remaining vertices $$P_2=(x_2,y_2),\ldots ,P_{n-1}=(x_{n-1},y_{n-1})$$ are to be found. By using consecutive rotations and assuming $$x=\cos \frac{2\pi }{n}, y=\sin \frac{2\pi }{n}$$, we can claim that

\begin{aligned} \left( {\begin{array}{c}x_i\\ y_i\end{array}}\right) -\left( {\begin{array}{c}x_{i-1}\\ y_{i-1}\end{array}}\right) =\begin{pmatrix}x&{}-y\\ y&{}x\end{pmatrix}\cdot \left( \left( {\begin{array}{c}x_{i-1}\\ y_{i-1}\end{array}}\right) -\left( {\begin{array}{c}x_{i-2}\\ y_{i-2}\end{array}}\right) \right) \end{aligned}

and therefore

\begin{aligned} x_i&=-xy_{i-1}+x_{i-1}+xx_{i-1}+yy_{i-2}-xx_{i-2}, \end{aligned}
(2.3)
\begin{aligned} y_i&=y_{i-1}+xy_{i-1}+yx_{i-1}-xy_{i-2}-yx_{i-2} \end{aligned}
(2.4)

for all $$i=2,3,\ldots ,n-1$$.

## Manual Results on Regular 5- and 11-gons

In this section we present a well-known statement on a regular 5-gon that can be obtained by using the formulas from the previous section. Also, we list some properties of a regular 11-gon, obtained with the same approach.

From now on we use a special notation to describe the performed steps when using the “axioms”. n will be fixed. The vertices of the regular n-gon will be denoted by $$P_0,P_1,P_2,\ldots ,P_{n-1}$$. To simplify Figs. 2 and 3, these points are labelled by their indices, that is, $$0,1,2,\ldots ,4$$ will refer to the points $$P_0,P_1,P_2,\ldots ,P_4$$. In addition, points ABCDEFG and H will be some fixed vertices of the n-gon. (We always use this notation in this paper, except in Fig. 4). By using axiom 2, segments $$d=AB$$, $$e=CD$$, $$f=EF$$ and $$g=GH$$ will be defined. Now, by using axiom 3, intersection of segments d and e will be denoted by R. Similarly, intersection of segments f and g will be denoted by S. By using axiom 2 again, the segment RS can be considered. Its length will be denoted by q.

### Theorem 3.1

Consider a regular pentagon (Fig. 2) with vertices $$P_0,P_1,\ldots ,P_4$$. Let $$A=P_0$$, $$B=P_2$$, $$C=P_1$$, $$D=P_3$$, $$E=P_0$$, $$F=P_2$$, $$G=P_1$$, $$H=P_4$$. Let us define diagonals $$d=AB, e=CD, f=EF, g=GH$$ and intersection points $$R=d\cap e, S=f\cap g$$. Now, when the length of $$P_0P_1$$ is 1, then the length of RS is $$q=\frac{3-\sqrt{5}}{2}$$.

This result is well-known from elementary geometry, but here we provide a proof that uses the developed formulas from Sect. 2. We will use the variables $$x_0,x_1,x_2,x_3,x_4$$ for the x-coordinates of the vertices, $$y_0,y_1,y_2,y_3,y_4$$ for the y-coordinates, and x and y for the cosine and sine of $$2\pi /5$$, respectively. Points $$P_0$$ and $$P_1$$ will be put into (0, 0) and (1, 0).

By using Table 1 and Eqs. (2.3) and (2.4), we have the following hypotheses:

\begin{aligned} h_1&=4x^2+2x-1=0,\\ h_2&=x^2+y^2-1=0,\\ h_3&=x_0=0,\\ h_4&=y_0=0,\\ h_5&=x_1-1=0,\\ h_6&=y_1=0,\\ h_7&=-x_2+-xy_{1}+x_{1}+xx_{1}+yy_{0}-xx_{0}=0,\\ h_8&=-y_2+y_{1}+xy_{1}+yx_{1}-xy_{0}-yx_{0}=0,\\ h_9&=-x_3+-xy_{2}+x_{2}+xx_{2}+yy_{1}-xx_{1}=0,\\ h_{10}&=-y_3+y_{2}+xy_{2}+yx_{2}-xy_{1}-yx_{1}=0,\\ h_{11}&=-x_4+-xy_{3}+x_{3}+xx_{3}+yy_{2}-xx_{2}=0,\\ h_{12}&=-y_4+y_{3}+xy_{3}+yx_{3}-xy_{2}-yx_{2}=0. \end{aligned}

Since $$R\in d$$ and $$R\in e$$, we can claim that

\begin{aligned} h_{13}=\begin{vmatrix}x_0&y_0&1 \\ x_2&y_2&1 \\ x_r&y_r&1\end{vmatrix}=0, \quad h_{14}=\begin{vmatrix}x_1&y_1&1 \\ x_3&y_3&1 \\ x_r&y_r&1\end{vmatrix}=0, \end{aligned}
(3.1)

where $$R=(x_r,y_r)$$. Similarly,

\begin{aligned} h_{15}=\begin{vmatrix}x_0&y_0&1 \\ x_2&y_2&1 \\ x_s&y_s&1\end{vmatrix}=0,\quad h_{16}=\begin{vmatrix}x_1&y_1&1 \\ x_4&y_4&1 \\ x_s&y_s&1\end{vmatrix}=0, \end{aligned}
(3.2)

where $$S=(x_s,y_s)$$. Finally we can define the length |RS| by stating

\begin{aligned} h_{17}=q^2-\left( \left( x_r-x_s\right) ^2+\left( y_r-y_s\right) ^2\right) =0. \end{aligned}

From here we can go ahead with two methods:

1. 1.

We directly prove that $$q=\frac{3-\sqrt{5}}{2}$$. As we will see, this actually does not follow from the hypotheses, because they describe a different case as well, shown in Fig. 3. That is, we need to prove a weaker thesis, namely that $$q=\frac{3-\sqrt{5}}{2}$$ or $$q=\frac{3+\sqrt{5}}{2}$$, which is equivalent to

\begin{aligned} \left( q-\frac{3-\sqrt{5}}{2}\right) \cdot \left( q-\frac{3+\sqrt{5}}{2}\right) =0. \end{aligned}

Unfortunately, this form is still not complete, because q is defined implicitly by using $$q^2$$, that is, if q is a root, also $$-q$$ will appear. The correct form for t is therefore

\begin{aligned} \begin{aligned} t=&\left( q-\frac{3-\sqrt{5}}{2}\right) \cdot \left( q-\frac{3+\sqrt{5}}{2}\right) \cdot \\&\cdot \left( -q-\frac{3-\sqrt{5}}{2}\right) \cdot \left( -q-\frac{3+\sqrt{5}}{2}\right) =0, \end{aligned} \end{aligned}

that is, after expansion,

\begin{aligned} t=(q^2-3q+1)\cdot (q^2+3q+1)=q^4-7q^2+1=0. \end{aligned}

Proving the thesis $$t=0$$ can be done by contradiction: we insert $$t\cdot z-1=0$$ into the equation system $$\{h_1,h_2,\ldots ,h_{17}\}$$ and get a contradictory equation system. This approach is based on the Rabinowitsch trick, introduced by Kapur in 1986 (see ).

2. 2.

We can also discover the exact value of q by eliminating all variables from the ideal $$\langle h_1,h_2,\ldots ,h_{17}\rangle$$, except q. We will follow this second method in the rest of the paper. This approach was suggested by Recio and Vélez in 1999 (see ). By obtaining a polynomial of q we actually get a product of minimal polynomials of the candidates for q. Elimination delivers an ideal, and since it contains the only variable q, it has to be generated by a single polynomial. We will use such polynomial for this generator that has integer coefficients and they are coprimes.

The first method may be more natural from the classical point of view, but for automation the second one fits better. Let us emphasize that the first method can be used only after one has a conjecture already. By contrast, the second method can be used before having a conjecture, namely, to find a conjecture and its proof at the same time.

For the first method we must admit that in Wu’s approach there is no way to express that the length of a segment is $$\frac{3-\sqrt{5}}{2}$$, after making our conjecture. Instead, we need to use the minimal polynomial of the conjectured number. Actually, $$q^2-3q+1$$ is the minimal polynomial of both $$\frac{3-\sqrt{5}}{2}$$ and $$\frac{3+\sqrt{5}}{2}$$, and $$q^2+3q+1$$ is of $$-\frac{3-\sqrt{5}}{2}$$ and $$-\frac{3+\sqrt{5}}{2}$$. In fact, given a length q in general, we need to prove that the equation $$t=t_1\cdot t_2=0$$ is implied where $$t_1$$ and $$t_2$$ are the minimal polynomials of the expected q and $$-q$$, respectively. Even if geometrically $$t_1=0$$ is implied, from the algebraic point of view $$t_1\cdot t_2=0$$ is to be proven.

Since q appears only in $$h_{17}$$, and only as a square, it is obvious that

### Proposition 3.2

q always appears to an even power in t.

Finally, when using the second method, by elimination (here we utilize computer algebra), we will indeed obtain that

\begin{aligned} \langle h_1,h_2,\ldots ,h_{17}\rangle \cap {\mathbb {Q}}[q]=\langle q^4-7q^2+1\rangle . \end{aligned}

This confirms that both methods yield the same result.

### Regular Star-Polygons

Before going further, we need to explain the situation with the regular star-pentagon in Fig. 3. Here we need to mention that the equation $$h_1=4x^2+2x-1=0$$ describes not only $$\cos (2\pi /5)$$ but also $$\cos (2\cdot 2\pi /5)$$, $$\cos (3\cdot 2\pi /5)$$ and $$\cos (4\cdot 2\pi /5)$$, however, because of symmetry, the first and last, and the second and third values are the same. We can think of these values as the projections of $$z_1,z_2,z_3,z_4$$ on the real axis, where

\begin{aligned} z_j=\left( \cos (2\pi /5)+i\sin (2\pi /5)\right) ^j=\cos (j\cdot 2\pi /5)+i\sin (j\cdot 2\pi /5), \end{aligned}

$$j=1,2,3,4$$. In other words, $$z_j$$ are the primitive 5th roots of unity.

That is, in this special case (for $$n=5$$) $$h_1$$ is a minimal polynomial of $$\text {Re}\,z_1(=\text {Re}\,z_4)$$ and $$\text {Re}\,z_2(=\text {Re}\,z_3)$$. By considering the formulas (2.3) and (2.4) we can learn that the rotation is controlled by the vector (xy), where $$\frac{2\pi }{n}$$ is the external angle of the regular n-gon. When changing the angle to a double, triple, $$\ldots$$, value, we obtain regular star-n-gons, unless the external angle describes a regular (star-) m-gon ($$m<n$$).

This fact is well-known in the theory of regular polytopes , but let us illustrate this property by another example. When choosing $$n=6$$, we have $$h'_1=2x-1=0$$ that describes $$\cos (2\pi /6)=\cos (5\cdot 2\pi /6)$$. Now by considering $$z'_1,z'_2,z'_3,z'_4,z'_5$$ where

\begin{aligned} z'_j=\cos (j\cdot 2\pi /6)+i\sin (j\cdot 2\pi /6), \end{aligned}

$$j=1,2,3,4,5$$, we can see that $$z'_2$$ can also be considered as a generator for $$\cos (1\cdot 2\pi /3)$$ (when projecting it on the x-axis) since $$2\cdot 2\pi /6=1\cdot 2\pi /3$$. That is, $$z'_2(=\overline{z'_4})$$ is not used when generating the minimal polynomial of $$\cos (2\pi /6)$$ (it occurs at the creation of the minimal polynomial of $$\cos (2\pi /3)$$), and this is the case also for $$z'_3$$ (because it is used for the minimal polynomial of $$\cos (2\pi /2)$$). In other words, all $$z'_j$$ are 6th roots of unity, but $$z'_2$$ and $$z'_4$$ are also the primitive 3rd roots of unity and $$z'_3$$ is the primitive square root of unity.

An immediate consequence is that $$z'_j$$ is used as a generator in the minimal polynomial of $$\cos (2\pi /6)$$ if and only if j and 6 are coprimes, but since $$\cos (2\pi /6)=\cos (5\cdot 2\pi /6)$$, only the first half of the indices j play a technical role. In general, when n is arbitrary, the number of technically used generators are $$\varphi (n)/2$$ (the other $$\varphi (n)/2$$ ones produce the same projections).

Finally, when considering the equation $$x^2+y^2=1$$ as well, if $$n\ge 3$$, there are two solutions in y, hence the hypotheses describe all cases when j and n are coprimes (not just for the half of the cases, that is, for $$1\le j\le n/2$$). Practically, the hypotheses depict not just the regular n-gon case, but also all regular star-n-gons. It is clear, after this chain of thoughts, that the number of cases is $$\varphi (n)$$ (which is the number of positive coprimes to n, less than n). From this immediately follows that the degree of ambiguity for $$\left( \cos \frac{2\pi }{n},\sin \frac{2\pi }{n}\right)$$ is exactly$$\varphi (n)$$, thus Proposition 2.1 is proven.

Also, it is clear that there exists essentially only one regular 5-gon and one star regular 5-gon (namely, $$\{5/2\}$$, when using the Schläfli symbol, see ). But these are just two different cases. The other two ones, according to $$\varphi (5)$$, are symmetrically equivalent cases. The axis of symmetry is the x-axis in our case.

On the other hand, by using our method, it is not always possible to distinguish between these $$\varphi (n)$$ cases only by considering the factorization over $${\mathbb {Q}}$$. Let us sketch up some difficulties here. The polynomial t that is obtained via elimination, usually has only real roots—half of them are positive and the others are negative. There are two main cases:

1. 1.

t is irreducible over $${\mathbb {Q}}$$:

1. (a)

If $$\deg t=2$$, $$t=q^2-c$$, where c is a rational. In this case clearly $$q=\sqrt{c}$$ follows and the solution is unique.

2. (b)

$$\deg t>2$$. In this case t is at least quartic (see Proposition 3.2) and therefore it contains at least 4 different real roots, at least 2 of them are positive and have geometric meaning. But, because t is irreducible over $${\mathbb {Q}}$$, by using only polynomial equations it is not possible to distinguish between its positive roots. We will see further details in Example 1 in Sect. 4.5.

2. 2.

Otherwise, the resulting polynomial t is a product of two polynomials $$t_1,t_2\in {\mathbb {Q}}[q]$$, and the half of the union of their roots are positive, while the others are negative. On the other hand, the positive roots can be placed in several combinations in $$t_1$$ and $$t_2$$ in general:

1. (a)

In our example in this section there are two positive roots in $$t_1$$ and two negative ones in $$t_2$$. When considering similar cases, the positive roots can always occur in, say $$t_1$$, and the negative roots then in $$t_2$$. Albeit the elimination delivers the product $$t=t_1\cdot t_2$$, clearly $$t_2$$ cannot play a geometrical role (since negative length has no meaning), therefore $$t_1$$ can be concluded. However, if $$t_1$$ contains more than one (positive) root, those roots cannot be distinguished without continuing the factorization over $${\mathbb {R}}$$. This is the case in our concrete example as well.

2. (b)

In general, $$t_1$$ may contain a few positive solutions, but $$t_2$$ may also contain some other ones. In such cases the positive solutions in $$t_1$$ and $$t_2$$, respectively, cannot be distinguished from each other. Such an example is the polynomial $$t=t_1\cdot t_2$$ where $$t_1=q^2-q-1$$ and $$t_2=q^2+q-1$$. It describes the length of the diagonal of a regular (star-) pentagon, namely both lengths $$\frac{\sqrt{5}\pm 1}{2}$$. Here $$t_1$$ contains one of the positive roots, namely $$\frac{\sqrt{5}+1}{2}$$, while $$t_2$$ the other one, $$\frac{\sqrt{5}-1}{2}$$. At the end of the day, only t can be concluded (that is, neither $$t_1$$ or $$t_2$$ can be concluded exclusively), none of its factors can be dropped because both contain geometrically useful data.

As a conclusion we learn that factorization over $${\mathbb {R}}$$ is a requirement to identify all roots of t precisely that may play a geometric role. Usually this step requires additional techniques and it is beyond the scope of this paper.

We will summarize the above considerations more formally later in Sect. 4.5, but here we emphasize a very important correlation that was proven above, namely:

### Proposition 3.3

The number of different regular star-polygons with n sides is $$\varphi (n)/2-1$$.

To simplify things, we will denote the set of regular polygons and star-polygons with n sides by $${\mathcal {R}}_n$$. With this notation $$|{\mathcal {R}}_n|=\varphi (n)/2$$. The notation $$\{n\}$$ will denote a regular n-gon and $$\{n/k\}$$ a regular star-polygon (here $$\gcd (n,k)=1$$, $$k\in {\mathbb {N}}$$, $$k<n/2$$). The special case $$k=1$$ can be written both as $$\{n/1\}$$ and $$\{n\}$$.

### Lengths in a Regular 11-gon

In Sect. 2 we mentioned that scientific results on a regular 11-gon are not very well-known because it is not constructible by typical means. Here we show some—for us, previously unknown—results that have been obtained by our method, implemented in the free dynamic geometry tool GeoGebra.

### Theorem 3.4

A regular 11-gon is defined by points A, B, C, $$\ldots$$, J, K. Diagonals CE, CF, CG, CH, DF, DK and HK are drawn. Then intersection points L, M, N and O are defined as shown in Fig. 4. The following properties hold:

• $$b=c$$,

• $$d=e$$,

• Triangles CLM and CON are congruent,

• $$a=l$$ (that is, $$AB=DL$$).

### Proof

By using the method described above, all of these statements can be mechanically proved in a straightforward way. $$\square$$

## Automated Discovery of Theorems

Obtaining new results randomly is one of the possible aims when observing regular polygons. To make discovery systematic it can also be important to make sure that all cases were observed when finding conclusions by exhaustion. Now we consider all different setups as a set $${\mathcal {S}}$$, and we try to number them consecutively. In other words, a bijective map

\begin{aligned} S:\{0,1,2,\ldots ,s-1\}\rightarrow {{\mathcal {S}}} \end{aligned}

is to be found. If such a map exists, we obtain some programmatic benefits for the processing of the cases:

1. 1.

A database $$D:\{0,1,2,\ldots ,s-1\}\rightarrow \{\text {true},\text {false}\}$$ can be maintained. Here for each $$k\in {\mathbb {N}}_0, k<s$$ there is an explicitly defined construction setup $$S(k)\in {{\mathcal {S}}}$$, and it can be saved as a database entry D(k) if the check about a possible theorem on the kth construction was already performed or not. If the computation loop needs to be suspended or stopped due to the high amount of computations for a given k, it can be restarted at the same value k in a next loop, independently from the first run. Here we note that the number of different setups can be quite large (depending on n), and the full check of all cases may take several hours or days.

2. 2.

This also supports parallel or distributed computing. The number of cases k can be then split and the setups can be divided among several processors or computers.

3. 3.

The distributed computation can also be controlled via a centralized Internet application that communicates with the clients, assigns the task to them, collects the results, and updates the central database. Of course, not only the success of the performed computations should be stored, but also their results, by using a map $$D':\{0,1,2,\ldots ,s-1\}\rightarrow \ldots$$ that has a sophisticated output data structure that can include the interestingness of the obtained theorem as well, for example.

This idea is well-known from various public projects, including the Great Internet Mersenne Prime Search at http://mersenne.org, that uses CPU time to find new Mersenne primes, available since 1996. Today, also, harnessing the idle time of the user’s processor is very popular in mining, for example, bitcoins, directly (on the user’s own decision) or indirectly (by programs that abuse the available resources, as hidden applications on malicious websites and other malware, see https://bitcoin.org/bitcoin.pdf and https://news.bitcoin.com/hackers-target-400000-computers-with-mining-malware/). This kind of technology is reported to be well-tested and very successful. Two success stories are Jonathan Pace’s and Patrick Laroche’s, two GIMPS volunteers who contributed for more than 14 years, and 4 months, respectively. They discovered the 50th and 51th known Mersenne primes in December 2017 and December 2018, $$2^{77,232,917}-1$$, and $$2^{82,589,933}-1$$, and both won an amount of \$3000 reward.

The concept of enumeration has been partially implemented in a software tool that is freely available at https://github.com/kovzol/RegularNGons. Item 1 is already working properly, while items 2 and 3 may be addressed as future work.

### A Bijective Mapping?

In our approach we assume that a regular n-gon is to be studied. It has $$\left( {\begin{array}{c}n\\ 2\end{array}}\right)$$ diagonals (including the sides). From these we select two different ones, d and e (the order of selection does not matter) to designate their intersection point R. That is, the number of possible selections are $$\left( {\begin{array}{c}\left( {\begin{array}{c}n\\ 2\end{array}}\right) \\ 2\end{array}}\right)$$. On the other hand, to designate another intersection point S from another combination of the diagonals, we finally have

\begin{aligned} \left( {\begin{array}{c}\left( {\begin{array}{c}\left( {\begin{array}{c}n\\ 2\end{array}}\right) \\ 2\end{array}}\right) \\ 2\end{array}}\right) \end{aligned}
(4.1)

different selections for the segment RS. When expanding the formula (4.1) we learn that the number of cases is

\begin{aligned} \frac{n^8-4n^7+2n^6+8n^5-15n^4+12n^3+12n^2-16n}{128}\sim \frac{n^8}{128}, \end{aligned}

that is, s is equal to $$n^8/128$$ asymptotically.

It would be useful to find a formula for S(k) to compute RS quickly. For the first step we will construct another map

\begin{aligned} c:\left\{ 0,1,2,\ldots ,\left( {\begin{array}{c}m\\ 2\end{array}}\right) -1\right\} \rightarrow \left( {\begin{array}{c}\{0,1,2,\ldots ,m-1\}\\ 2\end{array}}\right) \end{aligned}

where $$\left( {\begin{array}{c}\{0,1,2,\ldots ,m-1\}\\ 2\end{array}}\right)$$ stands for the set of 2-combinations of the set $$\{0,1,2,\ldots ,m-1\}$$. Here we will assume that

\begin{aligned} \begin{array}{ccclc} c(0)=\{0,1\},&{}\quad c(1)=\{0,2\}, &{}\quad c(2)=\{0,3\}, &{}\ldots , &{}\quad c(m-2)=\{0,m-1\}, \\ c(m-1)=\{1,2\}, &{}\quad c(m)=\{1,3\}, &{}\quad c(m+1)=\{1,4\}, &{}\ldots , &{}\quad c(2m-4)=\{1,m-1\}, \\ c(2m-3)=\{2,3\},&{}&{}&{}\ldots ,&{} \end{array} \end{aligned}

$$\ldots$$, and finally $$c\left( \left( {\begin{array}{c}m\\ 2\end{array}}\right) -1\right) =\{m-2,m-1\}$$. To compute c quickly, we consider the inverse map $$c^{-1}$$. It is clear that $$c^{-1}(k,k+1)=(m-1)+(m-2)+\cdots +(m-k)$$, that is, $$\frac{(m-1)+(m-k)}{2}\cdot k=-\frac{1}{2}k^2+k\cdot \frac{2m-1}{2}=p$$.

Let us now assume that p is given, and k is to be computed. Clearly $$-\frac{1}{2}k^2+k\cdot \frac{2m-1}{2}-p=0$$, and using the quadratic equation solver formula,

\begin{aligned} k=\frac{\frac{1-2m}{2}\pm \sqrt{\left( \frac{2m-1}{2}\right) ^2-2p}}{-1}= m-\frac{1}{2}\mp \sqrt{\left( m-\frac{1}{2}\right) ^2-2p}. \end{aligned}

Here obviously the subtraction should be chosen. By some further simple calculations finally we obtain the formula $$c(p)=\{k,l\}$$ where

\begin{aligned} k&=\left\lfloor {m-\frac{1}{2}-\sqrt{\left( m-\frac{1}{2}\right) ^2-2p}}\right\rfloor , \end{aligned}
(4.2)
\begin{aligned} l&=\frac{2p+k^2-(2m-3)\cdot k}{2}+1. \end{aligned}
(4.3)

This formulaFootnote 2 can be used then multiple times for $$m=\left( {\begin{array}{c}\left( {\begin{array}{c}n\\ 2\end{array}}\right) \\ 2\end{array}}\right)$$, $$m=\left( {\begin{array}{c}n\\ 2\end{array}}\right)$$ and $$m=n$$.

#### Example

Let $$n=5$$, then $$s=\left( {\begin{array}{c}\left( {\begin{array}{c}\left( {\begin{array}{c}5\\ 2\end{array}}\right) \\ 2\end{array}}\right) \\ 2\end{array}}\right) =990$$. We are interested in, say, the 678th case when observing all possible segments RS.

1. 1.

First we compute $$\left( {\begin{array}{c}\left( {\begin{array}{c}5\\ 2\end{array}}\right) \\ 2\end{array}}\right) =45=m_1$$. That is, we search for c(678). By using formulas (4.2) and (4.3), we get $$k=19$$ and $$l=33$$.

2. 2.

Now we search for the 19th and 33th combinations of a set with $$\left( {\begin{array}{c}5\\ 2\end{array}}\right) =10=m_2$$ elements. Using the same formulas, we get $$k=2,l=5$$ and $$k=4,l=8$$ values for $$p=19$$ and $$p=33$$, respectively.

3. 3.

Finally we search for the 2nd, 5th, 4th and 8th combinations of a set with $$5=m_3$$ elements. Using the same formulas again, we get $$k=0,l=3$$, $$k=1,l=3$$, $$k=1,l=2$$ and $$k=2,l=4$$ values for $$p=2,5,4$$ and 8, respectively.

Lastly we conclude that the 678th case describes when $$A=P_0$$, $$B=P_3$$, $$C=P_1$$, $$D=P_3$$, $$E=P_1$$, $$F=P_2$$, $$G=P_2$$, $$H=P_4$$. Now R is defined as the intersection of $$P_0P_3$$ and $$P_1P_3$$, that is $$R=P_3$$. And S is defined as the intersection of $$P_1P_2$$ and $$P_2P_6$$, that is $$S=P_2$$, so RS describes the side $$P_2P_3$$ which is an uninteresting case.

In fact, unfortunately, different cases can describe geometrically the same situation. For example, any point can be re-designated as the intersection point of two lines that already include it. Figure 5 shows such an example: the case 677 results in the same geometric output as case 678. On the other hand, in a regular hexagon the center can be constructed by intersecting any two of the three longest diagonals. These issues leads to the problem that some situations are covered by more than one setup and therefore computed multiple times needlessly.

### A Symbolic Implementation

This automated “mining” algorithm has been recently implemented in the software tool RegularNGons.

The following input parameters can be used to fine tune its output:

• $$n=\ldots$$ defines the number of vertices in the regular polygon.

• s and e define the starting and ending cases (both are non-negative integers, less than the formula (4.1)).

• By adding $$m=\ldots$$ or $$M=\ldots$$ the minimal and maximal degrees of outputs can be controlled, respectively. By default $$m=1$$ and $$M=2$$, that is, either linear results or quadratic surds are mined.

• The parameter u will force searching for results given as parameters. For example, $$u=2$$ considers only the outputs that are of $$q=2$$.

• The option $$S=0$$ tries to avoid checking cases that were already checked in a symmetrically equivalent position. When this is set, only the $$A=0$$, $$B\le n/2$$ cases will be checked. (The software tool uses the indices of the points, that is, 0 stands for $$P_0$$, 1 for $$P_1$$, and so on.)

• When using $$f=1$$, once a length is found, no more results will be printed that have the same length.

• The user may request to find lengths that are close to a given decimal number, but they are just approximately the same. The parameter $$a=\ldots$$ is to be set to the sought decimal. (See Sect. 4.6 for some examples.) By using the parameter E an error limit can be defined.

• The option $$z=\ldots$$ allows saving and retreiving results later by using an external server.

The software tool runs in a modern web browser, for example, Google Chrome 64. It uses the Giac computer algebra system to compute eliminations (its WebAssembly  version is used in an embedded way), and GeoGebra to visualize the obtained results on-the-fly—finally (or during the run) the results can be saved as a GeoGebra file (or stored on an external server as well).

The timing for a complete run for a given n-gon depends on the magnitude of n. For smaller n values the complete run can be performed in seconds or minutes. For bigger n values, a complete run may take several hours, or days, or even more. Some, yet unresolved memory issues in Giac may require multiple runs for bigger n values—this problem may be worked around with the option z.

A typical partial output of RegularNGons is the following, when using inputs $$n=7$$, $$S=0$$ and $$f=1$$:

This result will be recalled later in Theorem 4.15.

### A Numerical Implementation in GeoGebra

There is also a numerical implementation provided as a GeoGebra web applet at https://www.geogebra.org/m/zvxf6hbq. It can visualize different cases for different $$n\le 24$$ and perform a numerical search in $${\mathcal {R}}_n$$ (see Figs. 16 and 17 in Sect. 4.7 later). In this tool the polytope must be set with a concrete value for $$\{n/k\}$$, therefore all the algebraically non-distinguishable cases can be separately investigated.

A numerical check is usually much faster than its symbolic counterpart. However, the symbolic check computes all algebraically non-distinguishable cases at the same time, whilst the numerical check requires multiple runs for each geometrically different polytope.

Practically, both tools are useful and can be utilized to study two sides of the same coin.

### Some Results

We will find the following definition useful when presenting the statements that can be mined by using RegularNGons.

### Definition 4.1

• Points of the first kind of a regular n-gon are its vertices. We denote this set by $${{\mathcal {P}}}_1$$.

• Segments of the first kind of a regular n-gon are its sides and diagonals. We denote this set by $${{\mathcal {S}}}_1$$.

• Points of the k-th kind of a regular n-gon are the intersection points of its segments of the $$(k-1)$$-th kind. We denote this set by $${{\mathcal {P}}}_k$$.

• Segments of the k-th kind of a regular n-gon are the segments defined by its points of the (k)-th kind. We denote this set by $${{\mathcal {S}}}_k$$.

By using this notion, in this paper we consider segments of the second kind of a regular n-gon. We remark that it makes sense to study segments of higher kinds in a regular n-gon. It is easy to see that a recursive formula can be given to determine the number of possible cases for the various kinds of points and segments of a regular n-gon:

### Proposition 4.2

• $$|{{\mathcal {P}}}_1|=n$$.

• $$|{{\mathcal {S}}}_1|=\left( {\begin{array}{c}|{{\mathcal {P}}}_1|\\ 2\end{array}}\right)$$.

• $$|{{\mathcal {P}}}_k|\le \left( {\begin{array}{c}|{{\mathcal {S}}}_{k-1}|\\ 2\end{array}}\right)$$.

• $$|{{\mathcal {S}}}_k|=\left( {\begin{array}{c}|{{\mathcal {P}}}_{k}|\\ 2\end{array}}\right)$$.

### Proof

By construction, these formulas are obvious. In the third property an inequality can occur because sometimes the same point can be reached via multiple ways of intersecting segments (recall, for example, the situation in Fig. 5). $$\square$$

Let us focus now on a technical statement, that is, all newly constructed sets contain the previous ones:

### Proposition 4.3

• $${{\mathcal {P}}}_1\subseteq {{\mathcal {P}}}_2\subseteq {{\mathcal {P}}}_3\subseteq \cdots$$

• $${{\mathcal {S}}}_1\subseteq {{\mathcal {S}}}_2\subseteq {{\mathcal {S}}}_3\subseteq \cdots$$

### Proof

Let $$P\in {{\mathcal {P}}}_k$$ and consider two additional elements $$Q_1,Q_2\in {{\mathcal {P}}}_k$$. Now $$PQ_1, PQ_2\in {{\mathcal {S}}}_k$$ and therefore $$P=PQ_1\cap PQ_2\in {{\mathcal {P}}}_{k+1}$$.

Analogously, let $$s\in {{\mathcal {S}}}_k$$ and consider two additional elements $$u_1,u_2\in {{\mathcal {S}}}_k$$. Now $$Q_1:=s\cap u_1, Q_2:=s\cap u_2\in {{\mathcal {P}}}_{k+1}$$ and therefore $$s=Q_1Q_2\in {{\mathcal {S}}}_{k+1}$$. $$\square$$

### Proposition 4.4

Let $$\alpha \in {\mathbb {R}}$$ be the length of a segment of the k-th kind. Then the degree of the minimal polynomial of $$\alpha$$ over $${\mathbb {Q}}[x]$$ divides $$\varphi (n)$$.

### Proof

Footnote 3 Let $$\varepsilon$$ be the following n-th root of 1:

\begin{aligned} \varepsilon =\cos \left( \frac{2\pi }{n}\right) + i\sin \left( \frac{2\pi }{n}\right) . \end{aligned}

Consider the field $$T={\mathbb {Q}}(\varepsilon )$$. It is well known that the degree of the field extension $$T/{\mathbb {Q}}$$ is $$\varphi (n)$$ (see [13, Proposition 8.3] for a proof).

Let $$K=T\cap {\mathbb {R}}$$. It is clear that

\begin{aligned} 2\cos \left( \frac{2\pi }{n}\right) =\varepsilon +{\bar{\varepsilon }}\in K \end{aligned}

and

\begin{aligned} \varepsilon \cdot {\bar{\varepsilon }}=1. \end{aligned}

By using Vieta’s formulas we obtain that $$\varepsilon$$ is a root of the quadratic polynomial

\begin{aligned} p=x^2-2\cos \left( \frac{2\pi }{n}\right) x+1 \end{aligned}

that has degree 2 over K. Since $$\varepsilon \not \in K$$, it is clear that p is a minimal polynomial of $$\varepsilon$$ over K, that is, $$[T:K]=2$$.

By using the multiplicativity formula for fields T, K and $${\mathbb {Q}}$$ we obtain that

\begin{aligned}{}[T:{\mathbb {Q}}]=[T:K]\cdot [K:{\mathbb {Q}}], \end{aligned}

that is,

\begin{aligned}{}[K:{\mathbb {Q}}]=\varphi (n)/2. \end{aligned}

On the other hand, it is clear that all points in $${\mathcal {P}}_1$$ are elements of T. By having points $$z_1$$, $$z_2$$, $$z_3$$ and $$z_4$$ of $${\mathcal {P}}_1$$ it is clear that the intersection of $$z_1z_2$$ and $$z_3z_4$$ is also an element of T, because the intersection formula

\begin{aligned} z=\frac{((\overline{z_2}-\overline{z_1})z_1-(z_2-z_1)\overline{z_1})(z_4-z_3)- ((\overline{z_4}-\overline{z_3})z_3-(z_4-z_3)\overline{z_3})(z_2-z_1)}{(z_4-z_3)(\overline{z_2}-\overline{z_1})-(z_2-z_1)(\overline{z_4}-\overline{z_3})} \end{aligned}

contains only the basic operations and conjugations (see https://math.stackexchange.com/q/1352567 for a derivation of the formula), and according to $$\varepsilon ^{n-1}={\overline{\varepsilon }}$$, T is closed under conjugations as well.

By using this idea multiple times, by induction, we finally get that all points in $${\mathcal {P}}_k$$ are elements of T. Therefore, the distance $$\alpha$$ between points $$z',z''\in {\mathcal {P}}_k$$ can be computed by the formula

\begin{aligned} \alpha ^2=(z'-z'')\cdot \overline{z'-z''}\in T, \end{aligned}

but $$\alpha ^2$$ is also a real number, so it is an element of $$T\cap {\mathbb {R}}=K$$.

Now we learn that $$\alpha ^2$$ has a minimal polynomial of degree $$\varphi (n)/2$$ with rational coefficients. This means that $$\alpha$$ has a minimal polynomial of degree $$\varphi (n)$$ with rational coefficients. $$\square$$

### Proposition 4.5

All lengths appearing as segments of the k-th kind in a regular pentagon having unit side length, are either rational numbers or quadratic or quartic surds.

### Proof

Since $$\varphi (5)=4$$, this is a clear consequence of Proposition 4.4. $$\square$$

Now we can present some geometric results:

### Theorem 4.6

Given a regular 7-gon, there are 42 segments of its second kind that are of length 2, shown in Fig. 6.

### Proof

By exhausting all $$|{{\mathcal {S}}}_2|=21945$$ cases, there exist exactly the cases as presented. (The running time on a modern PC was about 1 h and 15 min). $$\square$$

The 42 different cases can be classified into 3 substantially different groups, shown in green, red and magenta in Fig. 6. Because of symmetry, each substantially different segment have 6 rotated copies and a mirrored copy with 6 other rotated copies. In total there are $$7+7=14$$ elements of the groups. In the figure only 2 representatives are colored in each group (they are mirror images), the others are all blue.

### Theorem 4.7

Given a regular 7-gon, and consider the segment $$q=1$$ of its second kind. Then:

1. 1.

There is a side AE of the 7-gon such that AE and RS are parallel such that EARS is a parallelogram;

2. 2.

for this AE, the lines AS and ER are parallel diagonals of the 7-gon,

unless RS is chosen from the red segments in Fig. 7.

### Proof

Again, by exhaustion. $$\square$$

It is easy to see that a kind of converse of this theorem holds in all regular polygons, independently of n. That is, the following very simple theorem can be stated:

### Theorem 4.8

Given a regular n-gon. Let us consider any side AE, and parallel diagonals $$d=AB$$ and $$f=EF$$; and, in addition, the diagonal $$e=CD=g=GH$$ which is parallel to AB. Now by choosing $$R=d\cap e$$, $$S=f\cap g$$, $$q=1$$.

### Proof

Due to parallelism, EARS is clearly a parallelogram, and therefore $$q=|AE|=1$$. $$\square$$

By using elementary combinatorics, the number of possible cases can easily be counted. Also, taking an arbitrary diagonal instead of side AE in Theorem 4.8 we obtain similar theorems on lengths that are not unit long, but the same as the length of some diagonal.

### Correspondence Between Elimination and the Minimal Polynomial of the Expected Length of RS

In this subsection we give a formal presentation of the concepts of this paper. All statements use the following setup:

Let $$RS_k$$ be a segment of the second kind in $$\{n/k\}$$. Let $$q_k\in {\mathbb {R}}^+$$ the length of $$RS_k$$, and let $$t_k(a)$$ be the minimal polynomial of the length $$q_k$$ over $${\mathbb {Q}}[a]$$. Also, let $$t_k'(a)$$ be the minimal polynomial of $$-q_k$$ over $${\mathbb {Q}}[a]$$. Furthermore, consider an algebraic translation of the algebraic setup with the points $$P_0(x_0,y_0),\ldots ,P_{n-1}(x_{n-1},y_{n-1})$$ and $$R(x_r,y_r)$$ and $$S(x_s,y_s)$$ and hypotheses $$h_1,h_2,\ldots ,h_{2n+7}$$ where

\begin{aligned} h_1=p_c(x),\ h_2=x^2+y^2-1,\ h_3=x_0,\ h_4=y_0,\ h_5=x_1-1,\ h_6=y_1, \end{aligned}

and $$h_7,\ldots ,h_{2n+2}$$ describe the vertices of the regular n-gon as given in (2.3) and (2.4), moreover $$h_{2n+3},\ldots ,h_{2n+6}$$ describe the collinearities as given in (3.1) and (3.2), finally

\begin{aligned} h_{2n+7}=a^2-\left( \left( x_r-x_s\right) ^2+\left( y_r-y_s\right) ^2\right) . \end{aligned}

Also, let $$H=\langle h_1,h_2,\ldots ,h_{2n+7}\rangle$$ and $${\mathcal {I}}=H\cap {\mathbb {Q}}[a]$$. We refer to this geometric construction as $${\mathcal {C}}(RS_k)$$.

### Definition 4.9

We say that $${\mathcal {C}}(RS_k)$$ is non-degenerate, if for all $$1\le k<n/2$$ all geometric steps according to the hypotheses $$h_1,h_2,\ldots ,h_{2n+7}$$ have a unique geometrical meaning. (That is, no intersection of parallel or identical lines has to be performed.)

### Proposition 4.10

Let $${\mathcal {C}}(RS_k)$$ be non-degenerate. Then:

1. 1.

$${\mathcal {I}}$$ is an ideal generated by a polynomial t that has only real roots. ($${\mathcal {I}}=\langle t\rangle$$.)

2. 2.

For each root $$\alpha$$ there is another root $$-\alpha$$.

3. 3.

For each positive root $$\alpha$$ there is a k such that $$q_k=\alpha$$.

4. 4.

For each k there is a positive root $$\alpha$$ such that $$q_k=\alpha$$.

5. 5.

$$\deg t\le \varphi (n)$$.

### Proof

1. 1.

Let us consider the degrees of the different hypotheses. According to Proposition 2 there are $$\varphi (n)$$ possibilities for (xy) when using $$h_1$$ and $$h_2$$, and all of them correspond to a valid situation geometrically, that is, x and y are real numbers, independently of which possibility is considered. The hypotheses $$h_3,\ldots ,h_{2n+2}$$ are all linear and introduce just one more variable for each. The hypotheses $$h_{2n+3}$$ and $$h_{2n+4}$$ are also linear and introduce two more variables, the same is true for $$h_{2n+5}$$ and $$h_{2n+6}$$. Finally, $$h_{2n+7}$$ is quadratic and introduces only one variable, but clearly there is a freedom of choice for the sign of a. This means that a can stand for only a real number: no complex root can be introduced during setting the hypotheses. After elimination, a still remains real.

2. 2.

$$h_{2n+7}$$ ensures this property.

3. 3.

The algebraic hypotheses describe a concrete geometric case.

4. 4.

For each concrete geometric case there is an algebraic description.

5. 5.

Because of axial symmetry of $$\{n/k\}$$ and $$\{n/(n-k)\}$$, $${\mathcal {C}}(RS_k)$$ and $${\mathcal {C}}(RS_{n-k})$$ produce the same lengths $$q_k$$ and $$q_{n-k}$$ for a certain k. This means that the $$\varphi (n)$$ possibilities for x and y correspond to at most $$\varphi (n)/2$$ different values q. But also $$-q$$ has to be represented in t. That is, t can have at most $$\varphi (n)$$ different roots. $$\square$$

In fact, we can generalize the result in the following way: $$RS_k$$ can also be a segment of a different kind, because axioms 2 and 3 introduce only linear equations, and only the metric equation is quadratic in the final step.

Now, when n and RS are fixed, consider all possible constructions $${\mathcal {C}}(RS_k)$$ and the lengths $$q_k$$ that belong to them. All are described with the polynomial t: they are roots of it. Also, $$-q_k$$ are the remaining roots of t. This means that t has no other roots than $$q_k$$ and $$-q_k$$. Now, because different $$\pm q_k$$ values are indistinguishable in the algebraic sense, they need to share the same minimal polynomial.

### Proposition 4.11

Let $${\mathcal {C}}(RS_k)$$ be non-degenerate. Then: If $$t_k\sim t_k'$$, then $$t\sim t_k \sim t_k'$$ and t is irreducible over $${\mathbb {Q}}[a]$$. Otherwise $$t\sim t_k\cdot t_k'$$. (In other words, t is a minimal polynomial of $$q_k$$, or it is the product of the minimal polynomials of $$q_k$$ and $$-q_k$$).

A reformulation of this result is the next

### Proposition 4.12

Let $${\mathcal {C}}(RS_k)$$ be non-degenerate. Then: If $$t_k$$ and $$t_k'$$ differs, then there is a primary decomposition of H such that

\begin{aligned} H=\langle t_k,h_1,h_2,\ldots ,h_{2n+7}\rangle \cap \langle t_k',h_1,h_2,\ldots ,h_{2n+7}\rangle . \end{aligned}

(That is, if the elimination produces a reducible polynomial t, then the theorem $$H\Rightarrow t$$ can also be written in the form $$H\Rightarrow t_k\vee t_k'$$).

This result helps in finding theorems that are true on parts. See  for more details.

Now let us assume that $${\mathcal {C}}(RS_k)$$ is non-degenerate and let $${\mathcal {I}}=\langle t\rangle$$. Now, for each root $$\alpha >0$$ of t let $$K_\alpha$$ be the set of numbers k such that $$k\in {\mathbb {N}}$$, $$\gcd (n,k)=1$$, $$k<n/2$$, and $$q_k=\alpha$$.

It is clear that

\begin{aligned} \sum _{\begin{array}{c} t(\alpha )=0 \\ \alpha >0 \end{array}}|K_\alpha |=|{\mathcal {R}}_n|=\varphi (n)/2, \end{aligned}

that is, the number of appearances of the roots of t cover the number of possible polytopes in $${\mathcal {R}}_n$$.

We conjecture the following:

### Proposition 4.13

Let $${\mathcal {C}}(RS_k)$$ be non-degenerate. Then: For each root $$\alpha _1>0$$ and $$\alpha _2>0$$ of t

\begin{aligned} |K_{\alpha _1}|=|K_{\alpha _2}| \end{aligned}

holds. That is, the distribution of the appearing lengths is uniform among the various polytopes in $${\mathcal {R}}_n$$.

From this conjecture and Proposition 4.4 it immediately follows that

### Proposition 4.14

For each root $$\alpha >0$$ of t

\begin{aligned} |K_\alpha |=\varphi (n)/\deg t \end{aligned}

holds. If $$\deg t = 2$$, then the positive root of t appears uniquely in all polytope counterparts in $${\mathcal {R}}_n$$. In other words, the degree of t explicitly determines the number of appearances of all roots among the polytopes in $${\mathcal {R}}_n$$.

Some of the above statements are illustrated in the following examples. Similarly to Sect. 3, from now on we will use the factors $$t_1$$ and $$t_2$$ if the obtained t is reducible to $$t_1\cdot t_2$$.

### Example 1

Let $$n=5$$ and consider case 33: $$A=0$$, $$B=1$$, $$C=0$$, $$D=2$$, $$E=1$$, $$F=2$$, $$G=3$$, $$H=4$$. Then the obtained polynomial after elimination is $$t=q^4-10q^2+5$$ which is irreducible over $${\mathbb {Q}}$$ but has the roots $$\pm \sqrt{\pm 2\sqrt{5}+5}$$. Both positive roots (3.0776 and 0.7265 approximately) are present once, the first one in $$\{5\}$$ and the other one in $$\{5/2\}$$. See Fig. 8. Here we learn that

\begin{aligned} K_{\sqrt{2\sqrt{5}+5}}=\{1\}\quad \text {and}\quad K_{\sqrt{-2\sqrt{5}+5}}=\{2\}. \end{aligned}

### Example 2

By considering $$n=24$$, case 48, the following output is mined by RegularNGons (note that $$\varphi (24)=8$$): $$A=0$$, $$B=1$$, $$C=0$$, $$D=2$$, $$E=0$$, $$F=1$$, $$G=2$$, $$H=8$$,

\begin{aligned} t=4q^8-72q^6+288q^4-324q^2+81, \end{aligned}

and the possible positive q values are

\begin{aligned} \frac{-\sqrt{3}+\sqrt{6}+3}{2}, \frac{\sqrt{3}-\sqrt{6}+3}{2}, \frac{\sqrt{3}+\sqrt{6}+3}{2}, \frac{\sqrt{3}+\sqrt{6}-3}{2} \end{aligned}

that belong to $$\{24\}$$, $$\{24/7\}$$, $$\{24/5\}$$, $$\{24/11\}$$, respectively (see Figs. 91011 and 12). That is,

\begin{aligned} K_{\frac{-\sqrt{3}+\sqrt{6}+3}{2}}=\{1\},\quad K_{\frac{\sqrt{3}-\sqrt{6}+3}{2}}=\{7\},\quad K_{\frac{\sqrt{3}+\sqrt{6}+3}{2}}=\{5\},\quad K_{\frac{\sqrt{3}+\sqrt{6}-3}{2}}=\{11\}. \end{aligned}

### Example 3

When checking $$n=23$$, case 70, the outputs are (note that $$\varphi (23)=22$$): $$A=0$$, $$B=1$$, $$C=0$$, $$D=2$$, $$E=0$$, $$F=1$$, $$G=3$$, $$H=13$$,

\begin{aligned} t= & {} q^{22}-228q^{20}+5618q^{18}-52167q^{16}+221675q^{14}-490131q^{12}\\&+590069q^{10}-378575q^8+117198q^6-13963q^4+503q^2-1. \end{aligned}

Here are some approximation of possible values of $$\alpha$$: 0.0459, 0.2424, 0.3734, 0.7426, 1.0002, 1.1919, 1.3209, 1.4892, 3.0158, 3.2263, 14.1901. Notably, the 5th value is very close to 1. This result (among many others) supports creating new, tricky problem assignments on disproving facts that are visually not decidable. On the other hand, by searching for good approximations some remarkable numerical results can also be achieved, say, by finding close values to non-algebraic numbers (see Sect. 4.7 for some examples on approximating $$\pi$$).

\begin{aligned} \begin{aligned} t_1=q^{11}-24q^{10}+174q^9-543q^8+703q^7-5q^6-861q^5+679q^4-34q^3-107q^2+17q+1,\\ t_2=q^{11}+24q^{10}+174q^9+543q^8+703q^7+5q^6-861q^5-679q^4-34q^3+107q^2+17q-1, \end{aligned} \end{aligned}

we learn that the 11 positive roots take place in such a way that the 1st, 3rd and 5th one (3 roots) are present in $$t_2$$, and the other ones (8 roots) are in $$t_1$$. We conclude that from the hypotheses either $$t_1$$ or $$t_2$$ follows in the algebraic approach. In other words, $$t_1$$ (as well $$t_2$$) may be true just on parts (see  for more details).

### Example 4

Let us consider the regular heptagon again, case 124: $$A=0$$, $$B=1$$, $$C=0$$, $$D=2$$, $$E=1$$, $$F=3$$, $$G=2$$, $$H=6$$. Here all variants in the regular star-heptagons result in the same $$\alpha =\sqrt{2}$$. We note that the degree of t is here just 2 ($$t=q^2-2$$), as described in Proposition 4.14. See also Fig. 13.

### Example 5

When $$n=13$$ we usually obtain polynomials of degree 12. (Since $$\varphi (13)=12$$, there are $$12/2=6$$ different elements in $${\mathcal {R}}_{13}$$.)

1. 1.

But, for example, in case 117 we get $$A=0$$, $$B=1$$, $$C=0$$, $$D=2$$, $$E=0$$, $$F=2$$, $$G=4$$, $$H=6$$ and the polynomial $$t=q^6-14q^4+q^2-1$$. The approximate values for $$\alpha _1\approx 0.3772$$, $$\alpha _2\approx 0.7261$$ and $$\alpha _3\approx 3.6510$$ are delivered by

• $$\{13/4\}$$ and $$\{13/6\}$$,

• $$\{13/2\}$$ and $$\{13/3\}$$,

• $$\{13\}$$ and $$\{13/5\}$$,

respectively. Thus

\begin{aligned} K_{\alpha _1}=\{4,6\},\ K_{\alpha _2}=\{2,3\},\ K_{\alpha _3}=\{1,5\}. \end{aligned}
2. 2.

On the other hand, in case 70,357 we obtain $$A=0$$, $$B=1$$, $$C=2$$, $$D=4$$, $$E=2$$, $$F=4$$, $$G=3$$, $$H=12$$ and the polynomial $$t=q^4-7q^2+9$$. The exact values for the positive roots are $$\alpha _1=\frac{\sqrt{13}-1}{2}\approx 1.3207$$ and $$\alpha _2=\frac{\sqrt{13}+1}{2}\approx 2.3207$$, and they are delivered by

• $$\{13\}$$, $$\{13/3\}$$ and $$\{13/4\}$$,

• $$\{13/2\}$$, $$\{13/5\}$$ and $$\{13/6\}$$,

respectively. Thus

\begin{aligned} K_{\alpha _1}=\{1,3,4\},\ K_{\alpha _2}=\{2,5,6\}. \end{aligned}
3. 3.

Finally, in case 75,070 we get $$A=0$$, $$B=1$$, $$C=2$$, $$D=6$$, $$E=0$$, $$F=5$$, $$G=4$$, $$H=12$$ and the polynomial $$t=q^2-3$$. The only positive root is $$\alpha =\sqrt{3}$$, and this will be delivered in $${\mathcal {R}}_{13}$$ uniformly:

\begin{aligned} K_{\alpha }=\{1,2,3,4,5,6\}. \end{aligned}

This example supports Propositions 4.44.13 and 4.14.

Finally we present a result which can be proven by exhaustion:

### Theorem 4.15

• In a regular heptagon the only rational lengths in $${\mathcal {S}}_2$$ are 1 and 2, and the only quadratic surd is $$\sqrt{2}$$.

• In a regular nonagon the only rational lengths in $${\mathcal {S}}_2$$ are 1, 2 and 3, and the only quadratic surds are $$\sqrt{3}$$ and $$\sqrt{7}$$.

• In a regular 11-gon the only rational lengths in $${\mathcal {S}}_2$$ are 1, 2, and the only quadratic surd is $$\sqrt{3}$$.

As a consequence of Proposition 4.14 it is clear that these lengths will be delivered uniformly in all cases in $${\mathcal {R}}_{n}$$ as well.

### Approximate Results in Regular 11-gons

By using the $$a=\ldots$$ option in RegularNGons, one may obtain some “almost”-results that can be interesting when creating tricky problem assignments. Here some results are listed—most of them involve regular star-polygons.

### Example 6

Let us consider the case $$n=11$$. By observing case 30,781, we get $$A=0$$, $$B=1$$, $$C=2$$, $$D=5$$, $$E=4$$, $$F=6$$, $$G=8$$, $$H=10$$ that produces $$q^{10}-53q^8+732q^6-2807q^4+3073q^2-947$$. It has a root 0.9990910 which is near 1. By using the numerical software tool again (see Sect. 4.3), we learn that this case belongs to $$\{11/3\}$$.

Let us consider case 31,507 now: $$A=0$$, $$B=1$$, $$C=2$$, $$D=6$$, $$E=1$$, $$F=3$$, $$G=6$$, $$H=10$$. Here the polynomial $$q^{10}-81q^8+1465q^6-4142q^4+2825q^2-67$$ can be obtained that has a root 1.0003614 which is closer to 1. This case belongs to $$\{11/2\}$$.

In addition, in case 50,867: $$A=0$$, $$B=1$$, $$C=4$$, $$D=6$$, $$E=2$$, $$F=7$$, $$G=5$$, $$H=8$$ yields $$q^{10}-64q^8+1029q^6-6085q^4+13831q^2-8713$$ which has a root 1.0001111, even closer to 1. The case belongs to $$\{11/4\}$$.

### Example 7

Again, assuming $$n=11$$, case 40,220, we get $$A=0$$, $$B=1$$, $$C=3$$, $$D=5$$, $$E=1$$, $$F=2$$, $$G=6$$, $$H=9$$: $$q^{10}-130q^8+886q^6-2147q^4+2116q^2-727$$. One of the roots is 1.66665066 which is very close to 5/3. This case belongs to $$\{11/3\}$$.

### Example 8

By searching for “almost”-zero results it is possible to create challenging questions like the following one: “Are the diagonals of a regular 11-gon concurrent as seen in Fig. 14?”

Actually, it can be rather difficult to verify such questions in a precise way. One possibility is to perform some deeper level of zooming in a DGS (here in GeoGebra) and conclude visually that the given diagonals are not concurrent (see Fig. 15). A better and more general way is to explicitly compute the distance of the intersection points of each two of the diagonals. This can be mechanically performed by the means shown in this paper: first a numerical search can be done (Figs. 16 and 17) and it will be obtained that the cases 166,853 and 167,359 describe the geometric situation, and then, using the symbolic counterpart we learn that the minimal polynomials of the searched lengths are $$q^{10}-36q^8+360q^6-645q^4+254q^2-1$$ and $$q^{10}-31q^8+259q^6-728q^4+433q^2-1$$, respectively.

### Approximating $$\pi$$

By using the same idea, several approximations on the transcendent number $$\pi$$ can be found among the segments of the second kind in regular polygons. Table 3 shows the best possible results for $$n<12$$ using the “minimal polynomial” t obtained via elimination. Note that for $$n=5$$ we obtain Example 1.

For $$n\ge 12$$ there are some more accurate results.

For $$n=12$$ two substantially different cases can be found, both are the same approximations as Kochański’s seventeenth century result in , $$\sqrt{120-18\sqrt{3}}/3\approx 3.141533338$$, which is a 4-digits approximation of $$\pi$$, see  for more details. Case 43,261 results in a regular star-12-gon, $$\{12/5\}$$ (see Fig. 19 and https://www.geogebra.org/m/jnZSeBnq), and case 52,958 in a regular 12-gon (see Fig. 18 and https://www.geogebra.org/m/qFvtny2G).

For $$n=13$$ there is no better approximation than $$3.1415877\ldots$$ that is produced in several setups, for example, in case 83,459 in $$\{13/3\}$$. It is the root of the polynomial $$x^{12}-115x^{10}+3048x^8-25161x^6+55723x^4-32118x^2+2809$$ (Fig. 19).

For $$n=14$$ the best approximation is $$3.141768\ldots$$ for case 1,438,411 in $$\{14/3\}$$ (among other cases).

For $$n=15$$ the best approximation is $$3.14159829\ldots$$ for case 381,653 in $$\{15/2\}$$ (Fig. 20). The approximation is a root of the polynomial $$x^8-441x^6+5141x^4-9081x^2+3331$$ (it is irreducible over $${\mathbb {Q}}$$), namely

\begin{aligned} \frac{\sqrt{441-187\sqrt{5}+3\sqrt{6\cdot (6805-3041\cdot \sqrt{5})}}}{2}. \end{aligned}

This formula has been generated by WolframAlpha. There is no appearance of this length in a regular 15-gon (only in a regular star polygon).

For $$n=16$$ the best known approximation is $$3.1415511\ldots$$ for case 220,100 in $$\{16/3\}$$. This length appears also in $$\{16\}$$ in case 266,067 (Fig. 21). Since this approximation is somewhat better than Kochański’s constant, and constructing a regular 16-gon is not much more difficult than drawing a regular 12-gon, by using only a compass and a straightedge, we obtain a surprisingly easy method to have another geometric approximation of $$\pi$$. The minimal polynomial of the obtained number is $$x^8-52x^6+874x^4-5516x^2+9809$$, it is irreducible over $${\mathbb {Q}}$$, and the exact form of the number is

\begin{aligned} \sqrt{13-\sqrt{2}-\sqrt{68-46\sqrt{2}}}. \end{aligned}

This result was produced by WolframAlpha.

Obtaining further results will get computationally more difficult, because of the high number of possible cases. This also means that at the moment the result above for $$n=16$$ is yet incomplete. Also, computing one case for higher n is usually harder computationally since more variables are involved.

### Other Examples

Some other results can be found at https://www.geogebra.org/m/AXd5ByHX. The software tool RegularNGons can be launched on-line at http://prover-test.geogebra.org/~kovzol/RegularNGons/. An example run can be started to request solving the case $$n=5$$ by invoking the URL http://prover-test.geogebra.org/~kovzol/RegularNGons/?n=5.

## Conclusion and Future Work

We presented an automated way on obtaining various new theorems on regular polygons, based on the work in [4, 24, 28, 29]. Enumerating the possible cases was an important detail in our work, we mapped the first non-negative numbers to the possible cases bijectively, however, some cases in our definitions still yield the same segment RS. This issue could be addressed later.

Further theorems can be developed by considering segments of higher kinds, not just of the second. The number of cases to check—according to Proposition 4.2—grows rapidly. For the third kind, it is asymptotic to $$n^{16}/2^{15}$$, and is more than 119 billions for $$n=5$$. That is, there can be lots of new theorems to explore, even if not all of them are of interest. On the other hand, all new results remain in the same set of algebraic numbers according to Proposition 4.4.

The high number of cases calls for distributed computing. Our further plan is to extend our software tool to be a centralized system that assigns interesting tasks to the contributors’ computers. By this way the idle computer time could be used to “mine” new geometry theorems.

Also, there are unexpected results on the structure of the appearing polynomials in the elimination step. Using algebraic geometry methods in solving the question on the appearing lengths is successful, but some fine details cannot be handled without determining the positive real roots of a polynomial explicitly. The used methods point also forward to possible example uses in statements that are true just on parts.

Finally, we highlight that a conjecture given in Proposition 4.13 still requires a proof.

1. 1.

See also https://oeis.org/A181872/a181872.pdf that proposes an algorithm to compute the minimal polynomial of $$\sin \frac{2\pi }{n}$$. Further information on the topic can be found in  and .

2. 2.

An anonymous reviewer pointed out that this process can be simplified by considering the ordering in the following way: Let $$c(0)=\{1,0\}$$, $$c(1)=\{2,0\}$$, $$c(3)=\{2,1\}$$, $$\ldots$$ This way $$\left( {\begin{array}{c}k\\ 2\end{array}}\right) \le p<\left( {\begin{array}{c}k+1\\ 2\end{array}}\right)$$ leads to $$k=\left\lfloor {\frac{1+\sqrt{1+8p}}{2}}\right\rfloor$$, $$l=p-\left( {\begin{array}{c}k\\ 2\end{array}}\right)$$. Both formulas are simpler than above and independent from m.

3. 3.

This proof is based on a personal communication with Ágnes Szendrei and Gábor Czédli, authors of .

## References

1. 1.

Bagai, R., Shanbhogue, V., Zytkow, J., Chou, S.: Automatic theorem generation in plane geometry. Lect. Notes Artif. Intell. 689, 415–424 (1993)

2. 2.

Bankoff, L., Garfunkel, J.: The heptagonal triangle. Math. Mag. 46, 7–19 (1973)

3. 3.

Chen, X., Song, D., Wang, D.: Automated generation of geometric theorems from images of diagrams. Ann. Math. Artif. Intell. 74, 333–358 (2015)

4. 4.

Chou, S.C.: Mechanical Geometry Theorem Proving. Springer, Berlin (1987)

5. 5.

Chou, S., Gao, X., Zhang, J.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reason. 25, 219–246 (2000)

6. 6.

Colton, S., Bundy, A., Walsh, T.: On the notion of interestingness in automated mathematical discovery. Int. J. Hum. Comput. Stud. 53, 351–375 (2000)

7. 7.

Coxeter, H.S.M.: Regular Polytopes, 3rd edn. Dover Publications, Mineola (1973)

8. 8.

Czédli, G., Szendrei, Á.: Geometriai szerkeszthetőség. Polygon, Szeged (1997)

9. 9.

Gao, H., Goto, Y., Cheng, J.: A set of metrics for measuring interestingness of theorems in automated theorem finding by forward reasoning: a case study in NBG set theory. Lect. Notes Comput. Sci. 9243, 508–517 (2015)

10. 10.

Gleason, A.M.: Angle trisection, the heptagon, and the triskaidecagon. Am. Math. Mon. 95, 185–194 (1988)

11. 11.

Gurtas, Y.Z.: Chebyshev polynomials and the minimal polynomial of $$\cos (2\pi /n)$$. Am. Math. Mon. 124(1), 74–78 (2017)

12. 12.

Haas, A., Rossberg, A., Schuff, D.L., Titzer, B.L., Gohman, D., Wagner, L., Zakai, A., Bastien, J., Holman, M.: Bringing the web up to speed with WebAssembly. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 185–200. Association for Computing Machinery (2017)

13. 13.

Hungerford, T.W.: Algebra, 12th edn. Springer, Berlin (2003)

14. 14.

Kapur, D.: Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399–408 (1986)

15. 15.

Kochański, A.A.: Observationes cyclometricae adfacilitandam praxin accomodatae. Acta Erud. 4, 394–398 (1685)

16. 16.

Kovács, Z.: Another (wrong) construction of $$\pi$$. CoRR, arXiv:1806.02218 (2018)

17. 17.

Kovács, Z.: Finding and proving new geometry theorems in regular polygons with dynamic geometry and automated reasoning tools. In: Rabe, F., Farmer W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, vol. 11006, pp. 164–177 (2018)

18. 18.

Kovács, Z.: Discovering geometry theorems in regular polygons. In: Fleuriot, J., Wang, D., Calmet, J. (eds) 13th International Conference, AISC 2018, September 16–19, 2018, Proceedings, Lecture Notes in Artificial Intelligence, vol. 11110, pp. 155–169 (2018)

19. 19.

Kovács, Z.: Mining geometry theorems in a regular polygon. In: Li, H. (eds) Proceedings of the 12th International Conference on Automated Deduction in Geometry, pp. 26–45 (2018)

20. 20.

Kovács, Z., Recio, T., Vélez, M.P.: Detecting truth, just on parts. Revista Matemática Complutense (2018). https://doi.org/10.1007/s13163-018-0286-1

21. 21.

Lehmer, D.H.: A note on trigonometric algebraic numbers. Am. Math. Mon. 40(3), 165–166 (1933)

22. 22.

Lenat, D.: Automated theory formation in mathematics. Contemp. Math. 29, 287–314 (1984)

23. 23.

Pierpont, J.: On an undemonstrated theorem of the disquisitiones arithmeticæ. Bull. Am. Math. Soc. 2(3), 77–83 (1895)

24. 24.

Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23(1), 63–82 (1999)

25. 25.

Sethuraman, B.: Rings, Fields, and Vector Spaces: An Introduction to Abstract Algebra via Geometric Constructibility. Springer, Berlin (1997)

26. 26.

Wang, D., Huang, B., Chen, X.: On $$n$$-sectors of the angles of an arbitrary triangle. In: Li, H. (eds) Proceedings of the 12th International Conference of Automated Deduction in Geometry, ADG 2018, pp. 117–133 (2018)

27. 27.

Wantzel, P.: Recherches sur les moyens de reconnaître si un problème de géométrie peut se résoudre avec la règle et le compas. J. Math. Pures Appl. 1(2), 366–372 (1837)

28. 28.

Watkins, W., Zeitlin, J.: The minimal polynomial of $$\cos (2\pi /n)$$. Am. Math. Mon. 100(5), 471–474 (1993)

29. 29.

Wu, W.-T.: On the decision problem and the mechanization of theorem-proving in elementary geometry. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years, pp. 213–234. American Mathematical Society, Providence (1984)

## Acknowledgements

Open access funding provided by Johannes Kepler University Linz. The author was partially supported by a Grant MTM2017-88796-P from the Spanish MINECO (Ministerio de Economia y Competitividad) and the ERDF (European Regional Development Fund). Many thanks to the two anonymous reviewers who helped improving the text in a definitive way. The author is grateful to Ágnes Szendrei, Gábor Czédli, Gábor Ancsin, Tomás Recio, M. Pilar Vélez, Francisco Botana and the GeoGebra Team for their valuable comments and suggestions.

## Author information

Authors

### Corresponding author

Correspondence to Zoltán Kovács.