En una publicación de blog muy interesante, Felix Breuer ha argumentado que la cultura matemática necesita valorar más que solo probar teoremas. En particular, identifica cuatro áreas de importancia: comunicar las matemáticas, probar el teorema colaborativo, implementar software matemático y formalizar las matemáticas. Recomiendo leer la publicación completa, pero también quiero citar la explicación de Breuer sobre el último de estos:
Formalización de las matemáticas. En mi opinión, formalizar las matemáticas es lo más importante que debe suceder si queremos que las matemáticas escalen. Con “formalizar las matemáticas” me refiero a un gran proceso que incluye todo lo siguiente.
- El desarrollo de los lenguajes y herramientas necesarias para que la formalización de definiciones matemáticas, teoremas y pruebas sea factible para el matemático promedio.
- Esto tendrá que ir de la mano con el desarrollo de sistemas de prueba automáticos que pueden automáticamente “llenar los vacíos” presentes en cualquier artículo de investigación.
- La creación de una infraestructura que permite compartir y descubrir artículos matemáticos formales en diferentes sistemas de prueba y lenguajes matemáticos formales.
- Y, finalmente, la formalización de (casi) todas las matemáticas.
No hace falta decir que este es un trabajo más que suficiente para generaciones (¡plural!) De matemáticos. Todavía tenemos un largo camino por recorrer en las cuatro áreas indicadas por los cuatro puntos anteriores. Y a pesar de que se está trabajando en todas estas áreas, este trabajo no es tan conocido como debería. Freek Wiedijk tuvo la amabilidad de darme una breve gira el otoño pasado, y planeo escribir un blog sobre esto en el futuro cercano.
He aquí por qué creo que el proyecto de formalizar las matemáticas es crucial. Nosotros, como humanos, no podemos hacer frente a la gran cantidad de producción matemática que se producirá en el siglo XXI. Por lo tanto, tenemos que enseñar a las computadoras cómo descubrir teoremas para nosotros que sean relevantes para las preguntas que nos interesan. De lo contrario, el trabajo de la mayoría de los matemáticos desaparecerá en la oscuridad más rápido de lo que cualquiera pueda sentirse cómodo.
La comunicación de las matemáticas, la demostración del teorema colaborativo, la implementación de software matemático y la formalización de las matemáticas, por supuesto, están estrechamente relacionadas. ¿Por qué no deberíamos soñar con recursos electrónicos compuestos que sean accesibles y comprensibles para todo tipo de lectores diferentes, en los que trabajemos en colaboración y que combinen textos expositivos con explicaciones detalladas y software utilizable con matemáticas formalizadas? Este sueño ciertamente no es nuevo y es compartido por muchos. ¿Cómo debería ser este valiente nuevo mundo de las matemáticas en detalle y cómo lo construimos? El proceso de explorar estas preguntas será realmente interesante. Mi punto aquí es que para llegar allí tenemos que renunciar a la creencia de que la demostración matemática es de lo que se trata la investigación matemática.
