50
$\begingroup$

Warning: I am only an amateur in the foundations of mathematics.

My understanding of this Wikipedia page about Tarski's axiomatization of plane geometry (and especially the discussion about decidability) is that "plane geometry is decidable".

The 2019 International Maths Olympiad happened recently, and there were two plane geometry questions in it (problems 2 and 6). Their solutions look really intimidating! However even as a student I felt that one should be able to solve these questions, in theory, by just "writing down coordinates of everything and doing the algebra". Tarski's work, which I will freely confess that I do not understand fully, might even vindicate my view.

The question: Is there an algorithm for solving these kinds of questions, or have I misunderstood? If so, is this algorithm actually feasible to run in practice nowadays (on a computer say) for IMO-level problems? In other words -- are there computer programs which will take as input a planar geometry question of "olympiad level" (for example problems 2 and 6 in this year's IMO) and actually output a solution?

Currently I am not too bothered about whether the solution is human-readable -- it could just be a formal proof in some kind of type theory or something, but the output would be some object that some expert could coherently argue was a solution of some sort.

The reason I'm asking is that I was talking to some computer scientists about various goals in the long-term project of getting computers to do mathematics "better than humans", and having a computer program which could solve IMO problems by itself was a suggested milestone.

$\endgroup$
20
  • 12
    $\begingroup$ Essentially all the usual Euclidean geometry questions could be reformulated as first-order sentences in the language of Tarski's geometry. And thus be solved by a decision algorithm for this theory. The exceptions are problems that talk about polygons with arbitrary amount of vertices rather than configurations that could be described by fixed amount of points. The decision problem is known to be NExpTime-hard. However, it doesn't mean that it is impossible to make algorithm that in practice solves some reasonable class of problems, although I am not aware of any practical algorithms here. $\endgroup$ Aug 3, 2019 at 17:45
  • 6
    $\begingroup$ My question is whether there is currently a feasible algorithm (and also whether I had misunderstood Tarski's work). I am more than happy to be told my question is not on topic, and would not be offended if it gets bumped to MSE or closed. I am looking for answers, I am not looking to cause trouble. I completely take your point about a 1 rep user. I built my rep up here talking about number theory but I am now interested in other things which are definitely of more marginal interest to the community here. $\endgroup$ Aug 3, 2019 at 18:13
  • 5
    $\begingroup$ Tarski's method gives a way of translating a problem in Elementary Plane Geometry (in the technical sense made precise by his axioms for geometry) into a problem about real-closed fields, and the first-order theory of real-closed field is decidable, using the Tarski-Seidenberg theorem which allows for quantifier elimination. (Presumably the statements you have in mind about properties picking out one of the two points of circle intersections are statements expressible in terms of field ordering.) But algorithms for eliminating quantifiers have complexity unbounded by stacks of exponentials. $\endgroup$
    – Todd Trimble
    Aug 4, 2019 at 0:13
  • 13
    $\begingroup$ @KevinBuzzard Just de-lurking to say that I, for one, would be more than happy to see you ask questions like these and get answers. I can't see the comments you're responding to but I hope that their deletion indicates that the authors thought twice $\endgroup$
    – Yemon Choi
    Aug 4, 2019 at 0:15
  • 12
    $\begingroup$ While the time complexity of Tarski's algorithm was not bounded by any stack of exponentials, the modern way of eliminating quantifiers for real-closed fields is cylindrical algebraic decomposition, which is only double exponential. Mathematica has an implementation of this. Apparently, there is also an algorithm for eliminating existential quantifiers (projecting a semialgebraic set) that only takes exponential time, but this is not available in Mathematica or any other major CAS, and the only implementation I could find of it hit a bug on every nontrivial example I tried. $\endgroup$ Aug 4, 2019 at 2:12

2 Answers 2

39
$\begingroup$

Arguably, the so-called "area method" of Chou, Gao and Zhang represents the state of the art in the field of machine proofs of Olympiad-style geometry problems. Their book Machine Proofs in Geometry features over 400 theorems proved by their computer program. Many of the proofs are human-readable, or nearly so.

The area method is less powerful than Tarski–Seidenberg quantifier elimination in the sense that not every statement provable by the latter is provable by the area method, but the area method has the advantage of staying closer to the "synthetic" nature of (the vast majority of) Olympiad problems.


EDIT (February 2022): OpenAI has announced some success with solving (some) formal math olympiad problems. They did not restrict themselves to geometry problems.

$\endgroup$
3
5
$\begingroup$

There is a pretty general method (although not always sufficient) to apply your intuition that one could translate everything into algebra and then solve it there.

Essentially, you introduce coordinates for your points, encode all your hypothesis as polynomial equalities between coordinates, do the same for the thesis, and then try to prove that the thesis is in the ideal generated by the hypotheses (or even its radical) using Gröbner bases. Of course, the issue here is that the classical Nullstellensatz does not hold for $\mathbb{R}$, so the thesis may hold even if it does not lie in the radical of the ideal generated by the hypotheses. Using the real Nullstellensatz, it may be possible to adapt the technique, but I did not give it much thought.

To make a concrete example, say you want to prove Heron's formula. Let $T$ be a triangle with side length $a, b, c$ and area $s$. You choose coordinates for the vertices of $T$ so that they are $(0, 0), (a, 0), (x, y)$ (this particular nice choice of coordinates is not necessary on a computer but simplifies the discussion for humans). Then the hypotheses are:

  • $b^2 = x^2 + y^2$
  • $c^2 = (a - x)^2 + y^2$
  • $2s = a y$.

The thesis is Heron's formula $16 s^2 = (a + b - c)(c + a - b)(b + c - a)(a + b + c)$.

What you do is consider the ideal $I \subset \mathbb{R}[a, b, c, x, y, s]$ generated by $b^2 - x^2 - y^2$, $c^2 - (a - x)^2 - y^2$ and $2s - ay$, and use Gröbner bases to check that $16 s^2 - (a + b - c)(c + a - b)(b + c - a)(a + b + c) \in \sqrt{I}$.

In fact, since the thesis does not involve $x, y$, one can compute $I \cap \mathbb{R}[a, b, c, s]$ - again using Gröbner bases - and discover that it is generated by the equation expressing Heron's formula.

EDIT

The above can actually be implemented very efficiently. I used rings, an efficient Scala library to perform polynomial computations, and the following

implicit val ring = MultivariateRing(Q, Array("a", "b", "c", "x", "y", "s"))
val h1 = ring("b^2 - x^2 - y^2")
val h2 = ring("c^2 - (a - x)^2 - y^2")
val h3 = ring("2 * s - a * y")
val t = ring("16 * s^2 - (a + b - c) * (c + a - b) * (b + c - a) * (a + b + c)")
val I = Ideal(ring, Seq(h1, h2, h3))
I.contains(t)

gave the answer true is about a second on my laptop.

$\endgroup$
9
  • $\begingroup$ Looks like there should be lot more identities. $\endgroup$
    – Turbo
    Aug 7, 2019 at 10:59
  • $\begingroup$ Did you do these calculations? Using which system? How long did they take? $\endgroup$ Aug 7, 2019 at 11:30
  • $\begingroup$ I have a gut feeling that some olympiad problems will not be solvable in this way because they might involve assertions about only some roots. (a+b-c)(c+a-b)(b+c-a)(a+b+c) is a polynomial function of a^2, b^2 and c^2, so issues of sign do not show up. What about an analogous question where it's essential that b is chosen to be the positive square root, and where the claimed equation does not hold if the negative one is chosen? I think that's why Groebner bases are not sufficient here but I do not know a good toy example. $\endgroup$ Aug 7, 2019 at 11:34
  • 1
    $\begingroup$ For what it’s worth, this can also be done easily enough by hand. We have $2ax=a^2+b^2-c^2$, so $(2ab)^2=(2ax)^2+(2ay)^2=(a^2+b^2-c^2)^2+16s^2$, and the result follows by rearranging and factoring the differences of squares. $\endgroup$
    – Matt F.
    Aug 7, 2019 at 12:51
  • 1
    $\begingroup$ We need a better toy example. $\endgroup$ Aug 7, 2019 at 18:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.