Se dice (porque hay asertos que tendríamos que creer prima facie) que una IA junto con un agente verificador lograron resolver un problema de Erdös; no uno cualquiera, sino uno de los interesantes. Si esto sigue así, entonces Math Inc. (u otras compañías) podrían patentar demostraciones. No es imposible ni inusitado: Elwyn Berlekamp patentó varios algoritmos relacionados con la decodificación de códigos algebraicos, y un algoritmo de este tipo es, en esencia, una demostración de que cierta decodificación es posible.
¿Y qué sucederá entonces? Con suerte sabremos que ciertos teoremas, quizá tan importantes como los de los problemas del milenio, son verdaderos, pero será muy difícil conocer sus demostraciones. Tal vez algunas sean verdaderamente muy complicadas, digamos que de complejidades que excedan millones o tal vez decenas de millones de líneas de código "golfeado" (así le dicen cuando está reducido respecto a una "primera pasada") en Lean o algún otro lenguaje de verificación. Y no solamente no podríamos acceder a ellas sino que, aunque accediéramos, no sería realista esperar que podríamos entenderlas como para comunicarlas.
En mi opinión, es intolerable que la matemática funcione así.
¿Qué alternativas habría? De entrada lograr alguna IA pública que pueda generar formalizaciones, y no importaría que sea algo "lenta". Habría que financiarla. Habrá que buscar cómo. Pero, además, habrá de todas maneras que entender cómo funciona lo que obtenga. Eso requiere que de verdad se ponga la comunidad matemática "libre" a trabajar en esa exposición. También habrá que buscar y encontrar cómo financiar eso.
Tal debe ser la resistencia. Y que viva, sin duda.
