21- Proof assistants

Hoy hablaremos de un tema muy desconocido, incluso entre matemáticos: los llamados "proof assistants".

Veamos una pequeña demostración de un teoremilla: "Existen infinitos números primos".

Supongamos que no fuese cierto: existe un número n y números p1, p2, ..., pn tales que {p1, p2,..., pn} es el conjunto de TODOS los primos existentes. Ahora construimos un número multiplicándolos todos y sumando 1.

P = p1*p2*...*pn + 1

Este número no es múltiplo ni de p1, ni de p2, ni de ningún otro número de la lista de primos gracias al "+1" que hemos añadido al final. Por lo tanto, tiene que tratarse de un primo también.  Pero, por otra parte, P es mayor que cualquiera de los pi's, así que no puede ser ninguno de ellos. Así, hemos descubierto otro primo que no estaba en la lista. Contradicción, pues habíamos supuesto que ésos eran todos los números primos. Y, así, por Reducción al Absurdo, concluimos que la lista de números primos es infinita. QED.

Y ahora que hemos visto esta demostración, te pregunto: ¿es correcta?

... ¿Cómo que si es correcta? ¿A qué te refieres?

Pues a eso mismo, ¿la aceptarías como válida? Sí, ¿no? Se trata de una demostración muy sencilla y cada paso se puede seguir sin problema. Pero, ¿qué ocurriría si el razonamiento tuviera 700 líneas y los pasos no estuvieran tan claros? Sería posible que alguno de ellos fuera erróneo. ¿Cómo lo podríamos detectar? Hmm... ¿Leyéndola una y otra vez hasta que encontrásemos algo que no sonase bien? ¡Sería como encontrar una aguja en un pajar!

Este ejemplo no está muy alejado de la realidad, pues algo similar ocurrió con un teorema muy famoso, el de "los cuatro colores". Dicho de forma sencilla, el enunciado del teorema afirma que dado cualquier mapa con regiones dibujadas, se pueden pintar dichas regiones con cuatro colores únicamente de forma que no haya dos regiones adyacentes del mismo color. Pues bien, en 1976 y 1996 se presentaron distintas demostraciones del teorema, que hasta entonces no era más que una conjetura, pero se basaban en un ordenador que comprobaba un número extremadamente grande de casos (con su correspondiente tiempo computacional extremadamente grande). Muchos matemáticos no aceptaron esto porque lo que hacía el ordenador no podía ser comprobado. Una década más tarde, en 2005, un matemático llamado George Gonthier logró una demostración del teorema usando un proof assistant y la comunidad matemática aceptó finalmente el resultado.

Los proof assistants son programas cuya base es un fortísimo campo de la lógica, la teoría de tipos (sí, la mencioné el otro día hablando de Russell). Estos softwares son capaces de comprobar cada paso de una demostración e incluso, si se trata de algo sencillo, de hacer la demostración ellos mismos.

Hay muchos proof assistants. Por ejemplo, el que usó Gonthier se llama "Coq", y también existen "Isabella", "HOL Light", "Mizar",...

Como curiosidad, en mi tesis de máster, empleé Coq para demostrar que la ley europea de transporte por carretera tenía vacíos legales y que un camionero podría (no sería lógico que quisiera hacerlo. Pero por poder, podría...) cometer ilegalidades (descansando menos de la cuenta durante un año y un día), aunque la policía no sería nunca capaz de demostrarlo.

Coq ("gallo" en francés) nació en Francia de la mano de Thierry Coquand en 1989, aunque aún se sigue investigando y desarrollando nuevas funcionalidades. Mientras hacía mi trabajo sobre la ley, me solía quejar de que era muy tiquismiquis, le tienes que dar todo masticado (hasta el punto de tener que demostrarle que 0<3, por ejemplo). Pero precisamente en esto se basa su precisión. Te obliga a revisar cada uno de los pasos y no dar ningún "salto de fe".

Otro día, tal vez dé un ejemplo de una pequeña demostración en Coq y de los problemas (no todo es del color de rosa) que puede plantear este tipo de software. Lo dejo aquí por hoy, que no quiero que te marees con tanta cosa.