Los matemáticos se rinden ante la IA: dejan de leer las demostraciones que ya no entienden
Wir müssen wissen – wir werden wissen
Hace un siglo, Hilbert soñó con una máquina que decidiera toda verdad matemática; Gödel y Turing demostraron que era imposible, pero de paso crearon la computación. Hoy los agentes de IA, apoyados en Lean, hacen realidad ese sueño, y el autor, informático, advierte un peligro: igual que muchos ya no leen el código generado por IA, los matemáticos podrían dejar de comprender sus propias demostraciones. Renunciar a pensar es el verdadero riesgo.
Como informáticos, deberíamos fijarnos en lo que ocurre en las matemáticas: negarse a leer el código de un programa que supera todas las pruebas —incluso la verificación formal— equivale a ignorar la demostración en cuanto la IA resuelve un teorema en Lean.
- dragontamer
> En oposición al necio ignorabimus, nuestro lema será Wir müssen wissen – wir werden wissen ("Debemos saber – sabremos").
Para quienes quieran llegar antes a la traducción. En mi opinión, es un poco injusto mantener el significado del título y la tesis de todo el blogpost hasta el séptimo párrafo.
- t0mek
> Debemos adoptar la misma actitud en la computación: usar abstracciones, refactorizar, refinar el alcance, inventar y adoptar lenguajes de más alto nivel, hasta que podamos sostener el código en la cabeza.
Quiero creer que esto es cierto. Pero como contraejemplo, ¿necesitamos sostener en la cabeza el código máquina o el ensamblador generados a partir de nuestros programas en C o Golang? ¿O más bien el código Golang es una abstracción de alto nivel que ya es suficientemente buena?
Si ese es el caso, ¿significa que deberíamos ir aún más lejos y tratar los documentos de diseño como el código adecuado para sostener en la cabeza y tratar el programa Golang como un derivado? ¿O quizá los documentos de diseño también son demasiado de bajo nivel y la vibra general de "créame una app, no cometas errores" ya es suficiente?
¿Cuál es el nivel de abstracción correcto? ¿Cómo encontrarlo?
- user2342
"¡Muss man wissen!"