Sturmfels' counterexample
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.