Convertir tazas de té en soluciones basadas en datos
El famoso matemático húngaro Alfred Renyi dijo que los matemáticos eran máquinas que transformaban las tazas de café en teoremas, pienso que esta cita ha alimentado la imagen bohemia que se tiene de los matemáticos la cual no negaré.
La única manera como los matemáticos logran un teorema es mediante una demostración matemática, una demostración matemática es un conjunto ordenado de enunciados que o son trivialmente ciertos, parte de nuestros axiomas o pueden deducirse utilizando principios lógicos elementales.
Los códigos que escriben los científicos de datos, los desarrolladores de software pero también los archivos de excel que todos utilizamos satisfacen una definición similar. En lugar de café podríamos imaginar que los analistas están convirtiendo tazas de té en líneas de código que después se transformarán en soluciones para un problema ya sea mediante:
- Un análisis estructurado de la información
- Un modelo matemático predictivo
- Un programa computacional
Sabemos que los estudiantes del Colegio de Matemáticas Bourbaki podrían beneficiarse de comprender las reglas básicas (inclusive si lo pensamos como gimnasia intelectual) de las demostraciones matemáticas con el objetivo de mejorar sus habilidades al estructurar un código o una base de datos.
En este texto hablaremos sobre la correspondencia de Curry-Howard la cual formaliza la relación entre los lenguajes de programación y las demostraciones matemáticas así como de la propuesta que tenemos en el Colegio de Matemáticas para ayudarle a nuestros estudiantes a estructurar mejor sus códigos o bases de datos.
Nos gustaría agradecerles particularmente por el seguimiento que le han dado a este nuestro Boletín del Colegio de Matemáticas Bourbaki porque hemos llegado con esta edición a las 100, la primera la publicamos hace exactamente 964 días.
La correspondencia de Curry-Howard
Aunque estrictamente hablando las matemáticas y la ciencia de la computación son dos áreas distintas, con sus propias intuiciones, intenciones y dificultades, existe un poderoso diccionario que permite relacionarlas.
En 1934 el célebre matemático Haskell Curry intuyó que las demostraciones matemáticas eran sospechosamente similares a los códigos con los más tarde se programarían las computadoras que todos utilizamos.
Notemos lo increíble de esta observación por las fechas cuando se hizo pues en ese entonces los desarrolladores de software y su intuición no existían. Algunos años más tarde el también matemático William Alvin Howard logró demostrar formalmente cómo construir esta correspondencia utilizando el cálculo lambda.
En el formalismo del cálculo lambda es posible demostrar esta correspondencia. Gracias a esta correspondencia es posible verificar software y demostraciones matemáticas. Poder verificar si una demostración matemática es correcta es uno de los problemas más complicados que existen y en los últimos años se han logrado grandes avances por ejemplo utilizando Coq o Lean.
Grupo de lectura en Bourbaki: Los Elementos de Euclides
La colección de libros Los Elementos escrita por el matemático griego Euclides es uno de los textos más importantes en matemáticas pues contiene el primer tratamiento axiomático de cualquier área en matemáticas.
Debido a esto a partir del mes de octubre vamos a tener una sesión semanal de aproximadamente 45 minutos en la que vamos a demostrar los profesores y estudiantes las proposiciones de los primeros 4 libros de Euclides. Nuestra propuesta es continuar esto durante más de dos años terminando en Diciembre del 2026.
El objetivo de este grupo es que los estudiantes aprendan pero también practiquen los detalles minuciosos de las demostraciones matemáticas aprendiendo de uno de los libros más detallados en este aspecto.
¿Cómo participar en estas sesiones?
En el Colegio de Matemáticas Bourbaki enseñamos con detalle las matemáticas y todos los perfiles y necesidades son bienvenidos, para ser parte de este grupo de lectura es necesario ser un estudiante o ex-estudiante del Colegio de Matemáticas Bourbaki. Compartimos con ustedes algunos de nuestros temarios.
- Especialización en Deep Learning (02 de Septiembre 2024, 49 semanas) Temario.
- Aplicaciones Financieras de ML & AI (16 de Septiembre 2024, 12 semanas). Temario. Sesión informativa.
- Track de Ciencia de Finanzas Cuantitativas (16 de Septiembre 2024, 49 semanas).
- Machine Learning & AI for the Working Analyst (11 de Octubre 2024, 12 semanas). Temario.
- Track de Ciencia de Datos (11 de Octubre 2024, 49 semanas). Temario.
- Matemáticas para la Ciencia de Datos (11 de Octubre, 49 semanas). Temario.
