- Zoltán Kovács
In 1989 Sturmfels remarked that there are theorems in elementary geometry which are true when using analytical approach by complex coordinates, but not true when these coordinates are real numbers. His example is the Sylvester-Gallai theorem for 9 points. He gives a proof about the statement if there is a set of 9 points (having complex coordinates) in a given configuration defining 11 lines as triplets, then there will be a 12th line consisting also of triplets. His remark may be a problem in automated theorem proving in elementary geometry since usual algebraic geometry methods like Wu's method or the Gröbner basis method allow complex coordinates for the realization of a theorem. If there is a theorem which is true for complex coordinates but false for real coordinates, then an automated theorem prover can conclude wrong results in the Euclidean geometry. In the following example we will show that Sturmfels' example can be, luckily, well handled in an automated prover, too.
- Sturmfels proposes to construct a system having 9 points denoted by 1, 2, ..., 9. Points 123, 147, 159, 168, 249, 258, 267, 348, 357, 369, 456 and 789 should be collinear. Here we define 123 and 897 as two base lines first (click to Step 2): yet only 13 and 87 are shown.
- In Step 3 we intersect lines 17 and 38 in point 4 since 148 and 348 are collinearity requirements.
- In Step 4 we constrain the point 2 as a point on line 13 since 123 is a collinearity requirement. We create intersection 24 and 87 since 249 and 789 are collinearity requirements, too.
- In Step 5 we intersect lines 19 and 28 in point 5 since 159 and 258 are collinearity requirements.
- In Step 6 we intersect lines 27 and 39 in point 6 since 267 and 369 are collinearity requirements, too.
- Now by using Pappus' hexagon theorem, points 546 are collinear (Step 7).
- There are only two missing requirements: 168 and 357. From the Sylvester-Gallai theorem we know that both cannot be satisfied at the same time in the Euclidean plane. So let us try to satisfy only one of them, say 357. In Step 8 we connected points 37 and we are searching for a suitable position for 5 to lie on the green line.
- We may have the feeling that 357 will never be collinear since line 37 is on the right side of the figure, but point 5 is on the left side, and line 249 is "between them".
- In Step 9 we can see the possible positions of point 5 when point 2 is moving on line 13. Let us drag point 2 on line 13 to investigate the positions of point 5 (red curve).
- We can also drag points 1, 3, 8 and 7 and investigate the changing red curve. It seems to be a parabola, but sometimes it changes to an ellipse or a hyperbola. But it never reaches the green line.
- Visually it can be verified well that no configurations of the free points and semi-free point can allow the red curve to reach the green line (except in degenerate cases). This means that 11 lines can never be defined lying on triplets of the 9 points.
- As a consequence, Sturmfels' original statement "if in a set of nine points in the projective complex plane 11 of the 12 triples in [the given configuration] collinear, then so is the twelfth" is correct not only for complex coordinates but for real coordinates as well, since the hypothesis is never true, thus the consequence is also correct. In other words, this statement causes no real trouble in automated theorem proving. The only remark here is that one has to be careful not to assume a contradictory configuration of possibly existing 11 lines.