En una sola setmana han arribat tres notícies que, posades juntes, fan pensar. L'empresa PSI diu que un sistema d'IA ha demostrat una conjectura de computació quàntica oberta des del 2008, i que el verificador Lean n'ha donat la prova per bona. Axiom Math ha traduït a uns setze milions de línies de codi verificable les més de 7.600 pàgines del Stacks Project, una obra de referència de geometria algebraica. I Google DeepMind ha comprovat formalment el programa que xifra els missatges de Signal amb sis milions de línies de proves. En tots tres casos, la garantia final no la dona cap persona, sinó un programa.
No és una pregunta nova. El 1976, Kenneth Appel i Wolfgang Haken van demostrar el teorema dels quatre colors, que diu que n'hi ha prou amb quatre colors per pintar qualsevol mapa sense que dos països veïns coincideixin. Una part essencial de la prova era una comprovació per ordinador de centenars de configuracions que cap matemàtic no podia revisar a mà. Tres anys després, el filòsof Thomas Tymoczko va publicar a «The Journal of Philosophy» un article cèlebre, «The Four-Color Problem and Its Philosophical Significance», on sostenia que acceptar aquell resultat obligava a canviar el concepte mateix de demostració: per primera vegada, una veritat matemàtica descansava sobre un experiment.
Tymoczko recollia una idea de Ludwig Wittgenstein, que a les «Observacions sobre els fonaments de la matemàtica» havia escrit que una demostració ha de ser abastable d'una mirada, que l'hem de poder seguir i reproduir. Per a Wittgenstein, una prova no és només una cadena de passos correctes: és una imatge que ens convenç, una cosa que veiem. Si el que hi ha és un llistat que cap ull humà no recorrerà, potser tenim una garantia, però costa dir que tinguem una demostració en el sentit en què els matemàtics l'han entès des d'Euclides. La qüestió és si aquesta diferència importa o és una nostàlgia.
Hi ha bones raons per pensar que no és nostàlgia. El 1994, el matemàtic William Thurston, medalla Fields, va escriure un assaig molt citat, «On proof and progress in mathematics», on defensava que l'objectiu de la matemàtica no és produir enunciats certs, sinó fer avançar la comprensió humana. Thurston explicava que algunes de les seves demostracions havien estat acceptades sense que gairebé ningú no les entengués, i que això havia deixat un camp sencer aturat: els resultats hi eren, però no se'n podia construir res perquè les idees no havien passat d'una ment a una altra. Un teorema que ningú no entén és, en part, un teorema mort.
Ara bé, l'argument té una altra cara. Les demostracions humanes també fallen, i de vegades durant anys. Quan Thomas Hales va demostrar la conjectura de Kepler sobre la manera més eficient d'apilar esferes, els revisors de la revista van acabar dient que n'estaven segurs al noranta-nou per cent, i Hales va dedicar més d'una dècada a formalitzar-la perquè un programa la comprovés pas per pas. En aquest cas, la màquina no va substituir la comprensió, sinó que va donar la certesa que els lectors humans, després d'anys de feina, no podien oferir. La verificació formal pot ser un aliat de la comprensió, no un rival.
El que canvia ara és l'escala i l'origen. Fins fa poc, una persona entenia la idea i la màquina en comprovava els detalls. A partir d'ara, pot ser que la màquina trobi la idea, l'escrigui en milions de línies i la verifiqui ella mateixa, i que nosaltres arribem al final per signar un resultat que no hem concebut. No és casual que, en el cas de PSI, un grup de Stanford estigui escrivint una exposició més breu per als experts: la comunitat necessita traduir la prova al seu propi llenguatge. Aquest treball de traducció, lent i poc vistós, pot acabar sent la part més humana de la matemàtica del futur.
Potser aquesta és la lliçó que va més enllà de les matemàtiques. En molts camps confiarem cada vegada més en resultats que no podem seguir: diagnòstics, prediccions, codi que protegeix les nostres converses. La certesa que ens donarà la màquina serà, en alguns casos, més sòlida que la nostra. Però una societat no viu només de saber que les coses són certes, sinó d'entendre per què ho són, de poder-les explicar i discutir. La pregunta que ens deixen aquestes demostracions il·legibles no és si ens podem fiar de les màquines, sinó si encara voldrem fer l'esforç d'entendre allò que ja ens hauran garantit.