Resolución automática de problemas de geometría de olimpiada

Question

Advertencia: Sólo soy un aficionado a los fundamentos de las matemáticas.

Mi comprensión de esta página de Wikipedia sobre la axiomatización de la geometría plana de Tarski (y especialmente la discusión sobre la decidibilidad) es que "la geometría plana es decidible".

El Olimpiada Internacional de Matemáticas 2019 ocurrió recientemente, y había dos preguntas de geometría plana en él (problemas 2 y 6). Sus soluciones parecen realmente intimidantes. Sin embargo, incluso como estudiante pensaba que uno debería ser capaz de resolver estas preguntas, en teoría, simplemente "escribiendo las coordenadas de todo y haciendo el álgebra". El trabajo de Tarski, que confieso libremente que no entiendo del todo, podría incluso reivindicar mi opinión.

La pregunta: ¿Existe un algoritmo para resolver este tipo de cuestiones, o lo he entendido mal? Si es así, ¿es este algoritmo realmente factible de ejecutar en la práctica hoy en día (en un ordenador, por ejemplo) para los problemas de nivel de la OMI? En otras palabras, ¿existen programas informáticos que tomen como entrada una pregunta de geometría plana de "nivel olímpico" (por ejemplo, los problemas 2 y 6 de la OMI de este año) y que realmente den una solución?

Actualmente no me preocupa demasiado si la solución es legible por los humanos - podría ser simplemente una prueba formal en algún tipo de teoría de tipos o algo así, pero la salida sería algún objeto que algún experto podría argumentar coherentemente que es una solución de algún tipo.

La razón por la que lo pregunto es que estuve hablando con algunos informáticos sobre varios objetivos en el proyecto a largo plazo de conseguir que los ordenadores hagan matemáticas "mejor que los humanos", y tener un programa informático que pueda resolver problemas de OMI por sí mismo era un hito sugerido.

Answer 1

Podría decirse que el llamado " método del área " de Chou, Gao y Zhang representa el estado del arte en el campo de las pruebas automáticas de los problemas de geometría de tipo olímpico. Su libro Pruebas mecánicas en geometría presenta más de 400 teoremas demostrados por su programa informático. Muchas de las pruebas son legibles para el ser humano, o casi.

El método del área es menos potente que la eliminación de cuantificadores de Tarski-Seidenberg en el sentido de que no todos los enunciados demostrables por este último son demostrables por el método del área, pero el método del área tiene la ventaja de mantenerse más cerca de la naturaleza "sintética" de (la gran mayoría de) los problemas de la Olimpiada.

Answer 2

Hay un método bastante general (aunque no siempre suficiente) para aplicar su intuición de que uno podría traducir todo al álgebra y luego resolverlo allí.

Esencialmente, se introducen coordenadas para los puntos, se codifican todas las hipótesis como igualdades polinómicas entre coordenadas, se hace lo mismo con la tesis, y luego se intenta demostrar que la tesis está en el ideal generado por las hipótesis (o incluso su radical) utilizando las bases de Gröbner. Por supuesto, la cuestión aquí es que la Nullstellensatz clásica no se sostiene para $\mathbb{R}$ por lo que la tesis puede sostenerse aunque no se encuentre en el radical del ideal generado por las hipótesis. Utilizando el Nullstellensatz real, puede ser posible adaptar la técnica, pero no lo he pensado mucho.

Para poner un ejemplo concreto, digamos que se quiere demostrar la fórmula de Heron. Sea $T$ sea un triángulo con longitud de lado $a, b, c$ y el área $s$ . Se eligen coordenadas para los vértices de $T$ para que sean $(0, 0), (a, 0), (x, y)$ (esta bonita elección de coordenadas no es necesaria en un ordenador, pero simplifica la discusión para los humanos). Entonces las hipótesis son:

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

La tesis es la fórmula de Heron $16 s^2 = (a + b - c)(c + a - b)(b + c - a)(a + b + c)$ .

Lo que se hace es considerar el ideal $I \subset \mathbb{R}[a, b, c, x, y, s]$ generado por $b^2 - x^2 - y^2$ , $c^2 - (a - x)^2 - y^2$ y $2s - ay$ y utilizar las bases de Gröbner para comprobar que $16 s^2 - (a + b - c)(c + a - b)(b + c - a)(a + b + c) \in \sqrt{I}$ .

De hecho, como la tesis no implica $x, y$ se puede calcular $I \cap \mathbb{R}[a, b, c, s]$ - de nuevo utilizando las bases de Gröbner- y descubrir que está generada por la ecuación que expresa la fórmula de Heron.

EDITAR

Lo anterior puede aplicarse de forma muy eficiente. He utilizado anillos una biblioteca Scala eficiente para realizar cálculos polinómicos, y lo siguiente

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)

dio la respuesta true es de aproximadamente un segundo en mi portátil.