O papel dos computadores nas demostracións matemáticas

A ferramenta básica e clásica dos matemáticos é un anaco de papel e un lapis. Na maioría dos casos eses dous instrumentos son suficientes para elaborar unha demostración matemática. Mais algúns teoremas resístense a ser probados desta elegante maneira e precisan do uso de computadores, como no caso do “teorema das catro cores” que, logo de 150 anos de incerteza, ven de ser demostrado definitivamente por un técnico de Microsoft. Definitivamente?

En matemáticas a frase “parece que” non sirve para nada: enunciados e afirmacións deben ser demostrados mediante argumentacións de afiada precisión que eliminen toda dúbida posíbel. Nunha demostración matemática utilízanse unha serie de pasos que, baseados en axiomas e regras lóxicas aceptados universalmente –por exemplo: se A é certo, e A implica B, entón B tamén é certo–, progrésase pouco a pouco cara unha conclusión final.

Sempre hai solución
Un dos grandes descubrimentos do pensamento humano é que calquera disputa sobre a validez dunha demostración matemática sempre pode resolverse. Sempre, aínda que fagan falla 150 ou 500 anos. É cuestión de dedicarlle o tempo preciso para que florezan as ideas e os camiños correctos. Este feito de que todas as disputas poidan, en principio, ser resoltas é algo que fai únicas ás matemáticas; pola contra, economistas, biólogos, astrónomos, filósofos e físicos poden pasar anos discutindo sobre diversas teorías sen chegar a ter a certeza da existencia dunha demostración definitiva.

Hai teoremas que se demostran facilmente –como o Teorema de Pitágoras– e outros que se fan moi famosos entre matemáticos e afeccionados pola dificultade para encontrar unha proba que os ratifique ou rexeite definitivamente. Por exemplo o chamado “último teorema de Fermat”, enunciado no século XVII polo matemático francés Pierre de Fermat e demostrado en 1993 logo de moitos intentos frustrados. Fermat deixou escrito na marxe dun libro o enunciado do teorema, de aparencia sinxela, afirmando ademais que el tiña unha demostración marabillosa, mais demasiado longa para escribila no borde do libro (…cuius rei demonstrationem mirabilem sane detexi. Hanc marginis exigitas non caperet). Cansada de tanto esperar, a universidade alemá de Gotinga ofreceu 100.000 marcos para quen fose capaz de resolver o misterio antes de 2007. A demostración definitiva chegou en 1993 da man de Andrew Wiles, un matemático de Princeton que dedicou toda a súa vida ao problema. O artigo de Wiles ocupa unhas 100 páxinas.

Cando non abonda coa elegancia
As demostracións matemáticas acostuman a ter unha fermosura intrínseca; unha boa demostración é simple e elegante –matematicamente elegante–, certeira, sen reviravoltas, transparente e sólida. Tamén pode haber demostracións pouco agraciadas, non por transgredir as regras matemáticas, senón por ter un esqueleto demasiado crecho, basto e escuro, con complicacións innecesarias e excesivos bucles. Mais tamén hai algúns teoremas que non poden ser demostrados coa elegancia que todos os matemáticos gustarían e que requiren argumentacións e operacións extremadamente laboriosas. Algunhas poden ocupar artigos de 100 páxinas, mais outras nin sequera iso. O “teorema das catro cores” resultou ser deste último tipo –dos “indemostrábeis a man”–, de tal xeito que foi o primeiro teorema importante demostrado grazas á axuda dos computadores. Mais, poden os computadores sustituir ao papel e lapis dos matemáticos? Esta é unha das principais controversias nas matemáticas de hoxe en día. Vexamos esta colorida historia.

A cor das matemáticas
O teorema das catro cores di que calquera mapa pode ser coloreado utilizando tan só catro cores sen que existan dúas rexións contiguas –que compartan un mesmo borde– coa mesma cor. Foi proposto en 1852 por Francis Guthrie e exposto á “London Mathematical Society” en 1878 polo matemático Arthur Cayley. En 1879 a revista Nature publicou un traballo de Alfred Bray Kempe coa suposta demostración, polo que foi moi loado. Mais logo de 11 anos de reinado, Percy John Heawood probou que a demostración era incorrecta: o teorema volvía a estar sen resolver.

Unha persoa pode pasar toda a vida pintando mapas deste xeito e darse conta de que realmente o teorema é probabelmente certo, mais para estar absolutamente seguro de que se cumpre en todos os casos posíbeis é preciso a demostración matemática. Tras moitos anos de intentos, o teorema das catro cores foi resolto en 1976 por dous matemáticos da Universidade de Illinois, Kenneth Appel e Wolfgang Haken, mais non todos quedaron contentos: para chegar á conclusión definitiva utilizaron un complicado método no cal a maior parte dos cálculos foron feitos por computadores. Entón xurdiu a dúbida: podemos confiar nos programas informáticos e nos procesadores dos ordenadores na elaboración dunha demostración matemática? Algúns matemáticos non aceptaron esta proba porque, debido ao enorme número de cálculos que precisa, non pode ser verificada a man; ademais, carece de elegancia matemática. “Unha boa demostración matemática é como un poema, e isto é un directorio telefónico!” dixeron algúns.

Matemáquinas
Temos entón un problema coas demostracións que precisan dunha cantidade enorme de cálculos; até é posíbel que non exista maneira de demostrar o teorema das catro cores con lapis e papel, levaría moito máis tempo co que dura unha vida humana. Debemos confiar o traballo aos computadores? Estas máquinas teñen a vantaxe de que poden realizar cálculos longos e tediosos sen protestar. Ademais, son perfectas para realizar algoritmos: un proceso de computación no cal, a partir dun valor de entrada e seguindo uns pasos perfectamente definidos, prodúcese un valor de saída. Un algoritmo é, por exemplo, o proceso que realizamos para resolver a man unha división: cada un dos pasos está definido sen ambigüidade e conduce sempre a un resultado específico (por certo, a verba “algoritmo” ven de “al-Khowârizm”, nome do matemático persa Abu Ja’far Mohammed ibn Mûsa al-Khowârizm, que no século IX escribiu un importante libro titulado “Kitab al jabr w’al-muqabala”. A verba “álxebra” procede das verbas “al jabr” que aparecen nese título).

Até hai pouco non estaba clara a posibilidade de verificar afirmacións matemáticas utilizando a grande potencia e escasa poesía dos computadores, mais a recente demostración “definitiva” do teorema das catro cores polo técnico de Microsoft Georges Gonthier –cun apelido curiosamente moi parecido ao da persoa que propuxo o problema Francis Guthrie– pode rematar con esta polémica. Gonthier ven de demostrar o teorema –o traballo aínda non está publicado en ningunha revista científica– utilizando un “asistente matemático”, unha tecnoloxía para ordenadores desenvolvida nos últimos 30 anos que permite verificar que as operacións feitas por unha destas máquinas segue de maneira rigorosa as regras da lóxica. Gonthier utilizou un asistente chamado Coq desenvolvido por Inria –o instituto francés para investigación en ciencia computacional–.

Segundo Gonthier, non hai razón para crer que os humanos son máis precisos que os computadores para facer demostracións matemáticas. Polo de agora non hai unha proba ao teorema das catro cores que poida ser feita a man por un humano, ao mellor nunca chega ese momento. O teorema considérase probado.

LIGAZONS

Four colors theorem
Proof and beauty. The Economist
Last doubts removed about the proof of the Four Color Theorem

The Coq proof assistant

Último teorema de Fermat

Pierre de Fermat