Tabla de contenido
Asistentes de demostración: cuando la matemática se vuelve código
Los asistentes de demostración como Lean convierten la matemática en código verificable. El juego gratis con el que tu hijo puede probar que 2+2=4 desde cero.
Los asistentes de demostración existen, son gratis y uno de ellos corre en un navegador. El Natural Number Game te pide que demuestres que 2 + 2 = 4, empezando casi de cero, y se niega a dejarte saltar un paso. A la mayoría de los adolescentes le resulta insoportable unos veinte minutos y después no puede parar.
Esa experiencia vale más hoy que hace cinco años. Cuando los sistemas de IA producen demostraciones de cien páginas que son correctas cerca de la mitad de las veces, entender qué hace realmente la verificación mecánica deja de ser un interés de nicho y se vuelve una forma de pensar.
Puntos clave
- Lean es un demostrador interactivo de teoremas: escribes la demostración en un lenguaje formal y el software rechaza cualquier paso que no se siga de lo anterior.
- El Natural Number Game (NNG4) es gratis, de código abierto bajo Apache 2.0, corre en el navegador en adam.math.hhu.de y arranca desde los axiomas de Peano.
- El Liquid Tensor Experiment demostró que la formalización funciona a nivel de investigación: el desafío de Peter Scholze de diciembre de 2020 se completó en Lean el 14 de julio de 2022.
- Formalizar toma más tiempo que escribir una demostración informal, y por eso las demostraciones hechas por IA se acumulan más rápido de lo que alguien puede verificarlas.
- La habilidad transferible es distinguir “este argumento me convenció” de “todos los pasos de este argumento son válidos”.
Qué hacen exactamente los asistentes de demostración
Un asistente de demostración es software que revisa argumentos matemáticos de forma mecánica. Enuncias un teorema en el lenguaje formal del sistema, después das la demostración como una secuencia de movimientos, y en cada paso el software sabe exactamente qué ya estableciste y qué te falta. Si intentas afirmar algo que no se sigue, no lo acepta.
Lean, hoy en su cuarta versión mayor, es el que prendió entre los matemáticos en actividad. El servidor de juegos de Lean es una puerta de entrada; la razón más profunda de su adopción es Mathlib, una biblioteca construida por la comunidad que contiene una porción grande de la matemática de grado y posgrado ya formalizada, así que puedes apoyarte en resultados existentes en vez de partir de axiomas cada vez.
La distinción clave, y la que vale enseñar, es entre convincente y válido. Una demostración en papel es convincente: persuade a un lector experto de que el resultado se sostiene, con pasos de rutina comprimidos en frases como “claramente” y “se sigue que”. Una demostración formal es válida: cada inferencia está explicitada al punto en que una máquina sin ninguna intuición matemática puede confirmarla.
Esa brecha es donde se esconden los errores. El artículo de Terence Tao de enero de 2025 en las Notices of the American Mathematical Society sostiene que los demostradores interactivos están cambiando la práctica matemática mientras plantean preguntas epistemológicas reales sobre qué es una demostración. Esas preguntas no están cerradas.
Demostración en papel y demostración formal
| Propiedad | En papel | Formal en Lean |
|---|---|---|
| Audiencia | Un lector humano experto | Una máquina sin intuición |
| Pasos de rutina | Comprimidos (“claramente”, “se sigue”) | Cada paso explícito |
| Detección de errores | Depende de la atención del árbitro | Mecánica; un paso malo no compila |
| Tiempo para producirla | Línea base | Históricamente mucho más |
| Qué errores siguen siendo posibles | Huecos lógicos, supuestos no dichos | Formalizar el enunciado equivocado |
| Legibilidad | Pensada para humanos | Difícil de leer; pensada para el verificador |
| Reutilización | Citada por otros artículos | Importable como dependencia de biblioteca |
| Costo de verificación | Semanas de tiempo experto | Segundos, una vez formalizada |
Las dos últimas filas son por qué esto importa científica y comercialmente. Un teorema formalizado es un componente reutilizable; uno informal es un documento que alguien tiene que volver a leer. Y la verificación se vuelve casi gratis después de la parte costosa.
La fila que quiero que los papás noten es la de qué errores siguen siendo posibles. Una demostración en Lean que compila es lógicamente hermética, pero solo demuestra el enunciado que efectivamente escribiste. Si formalizas el teorema equivocado, Lean lo verifica encantado. Es exactamente el mismo modo de falla que un código que pasa sus pruebas mientras resuelve el problema equivocado.
El Liquid Tensor Experiment, en simple
En diciembre de 2020, Peter Scholze, medallista Fields, hizo algo poco común. Él y Dustin Clausen habían demostrado un teorema sobre “espacios vectoriales líquidos” que permitiría meter el análisis funcional y la geometría compleja dentro de su marco de matemática condensada. El argumento era lo bastante sutil como para que Scholze mismo no estuviera del todo seguro, así que pidió públicamente a la comunidad de demostración formal que lo verificara.
La comunidad lo tomó como el Liquid Tensor Experiment y trabajó en Lean. Se completó el 14 de julio de 2022, unos dieciocho meses después. Nature y Quanta Magazine lo cubrieron.
Pasaron dos cosas que vale explicarle a un adolescente. Primera: uno de los mejores matemáticos vivos les pidió a desconocidos que revisaran su trabajo porque no estaba seguro. Segunda: lo revisaron y se sostuvo. Así se ve la honestidad intelectual en la cima de un campo, y es una historia mejor sobre la matemática que cualquier relato de “genio”.
Cómo enseñarle esto a tu hijo
El concepto es que una demostración es una cadena donde cada eslabón tiene que aguantar, no una historia que suena bien.
De 5 a 8 años: el juego del “porque”
Haz una afirmación con la que tu hijo no esté de acuerdo y justifícala paso a paso, dejándolo decir “¿por qué?” después de cada paso. “Tenemos que salir ahora.” ¿Por qué? “Porque el bus pasa a las 8.” ¿Y por qué importa eso? “Porque si lo perdemos, el próximo es a las 9.”
Después inviertan. Él hace una afirmación y tú preguntas “¿por qué?” hasta que se queda sin respuestas. Quedarse sin respuestas es la lección: llegó a un supuesto, que es lo que es un axioma.
De 9 a 12 años: sin atajos
Dale una tarea simple con una regla: cada instrucción tiene que ser algo que puedas hacer sin pensar. Servirse un vaso de agua pasa a tener ocho pasos, no uno. Cuando diga “toma un vaso”, tú preguntas “¿de dónde?”.
Así se siente formalizar. La monotonía es el contenido: lo que para un humano es un paso, para una máquina son muchos, y cada uno de esos pasos es un lugar donde podría esconderse un error.
De 13 en adelante: jugar el Natural Number Game
Mándalo a adam.math.hhu.de y que arranque el Natural Number Game. Es la versión en Lean 4 de un juego originalmente construido por Kevin Buzzard y colaboradores en el Imperial College de Londres, distribuido bajo Apache 2.0, y corre en el navegador sin instalar nada.
El juego arranca con axiomas al estilo de Peano y te pide demostrar cosas que sabes desde los cinco años, como que 2 + 2 = 4. Su primera reacción va a ser que es absurdo. Cerca del cuarto nivel va a darse cuenta de que nunca supo por qué 2 + 2 = 4, solo que da. Ese momento es todo el punto.
Pon un límite de 45 minutos la primera vez. La frustración es productiva pero tiene techo.
La pregunta que debes hacer: “¿Cuál paso de tu argumento se negaría a aceptar una computadora?”
¿Y en América Latina?
Esto es más accesible en la región de lo que parece, y ahí está lo interesante.
El Natural Number Game corre en el navegador, no pide instalar nada, es gratis y funciona en una computadora modesta o incluso en un celular decente. Eso importa en un contexto donde, según los datos de PISA 2025, el 63% de los estudiantes colombianos asiste a escuelas con falta de materiales educativos y, según el informe argentino de Argentinos por la Educación con investigadores del MIT, solo 6 de cada 10 estudiantes tiene computadora en casa, y en hogares de bajos ingresos baja a 3 de cada 10.
El otro lado del argumento es la demanda. En resolución de problemas computacional, el dominio nuevo de PISA 2025, la región rindió mejor de lo esperado: México 453, Chile 466, Uruguay 462, Perú 436, contra puntajes de ciencias bastante más bajos. Ese dominio evalúa construir, experimentar de forma sistemática, analizar datos y depurar. Jugar el Natural Number Game entrena una versión exigente de exactamente eso.
Y hay un punto de oportunidad que vale decir en voz alta: el cuello de botella global de la matemática con IA es la verificación, no la generación. Quien sepa verificar tiene una habilidad escasa, y aprenderla no depende de vivir en Boston.
Por qué esto importa más en 2026
El cuello de botella de la verificación es hoy la restricción real del campo. Thomas Bloom, que mantiene la base de datos de problemas de Erdős, le dijo a Quanta que están llegando artículos generados por IA de 100 a 200 páginas como supuestas soluciones y que “ningún humano lo ha leído”.
La verificación mecánica es la respuesta obvia, y no está lista. Formalizar una demostración informal todavía requiere trabajo sustancial, a veces más que escribir la original. Quanta reporta que las herramientas se usan con cuentagotas: Nat Sothanaphan usó el demostrador Aristotle para certificar la coherencia lógica de una demostración, y Liam Price usó revisiones repetidas con instancias nuevas del modelo. Ninguna se generaliza.
Así que la pregunta viva en matemáticas ahora mismo es si la traducción a sistemas formales se puede automatizar. Si se puede, el cuello de botella se abre y la matemática generada por IA se vuelve confiable a escala. Si no, las demostraciones van a seguir acumulándose sin verificar. Es una pregunta genuinamente abierta, y un chico que pasó una tarde en Lean entiende lo que está en juego mejor que la mayoría de los adultos que leen los titulares. Los tres métodos en uso están en cómo verifican los matemáticos una demostración de 125 páginas.
Qué hacer en casa
”Compiló” es una pregunta distinta de “está bien”
Sea Lean, una hoja de cálculo o un script de Python, las dos preguntas son distintas: ¿corre sin error?, y ¿responde la pregunta que querías hacer? Los chicos que interiorizan esa distinción depuran mejor toda la vida.
Déjalo chocar contra la pared
El Natural Number Game está diseñado para frustrar. Un adolescente que empuja tres niveles aprende algo que ninguna explicación entrega: que “obvio” no es lo mismo que “demostrado”.
Conéctalo con el código que ya escribe
Si tu hijo escribe algo de código, la demostración formal es una extensión natural: un sistema de tipos revisando tu programa es la misma idea que un asistente revisando tu argumento. El terreno común está en pensamiento computacional vs. programación.
Pregunta qué paso carga el peso
En cualquier argumento, uno o dos pasos hacen el trabajo real y el resto es contabilidad. Encontrar el paso que carga el peso es cómo un árbitro lee un artículo, y es una habilidad que sirve para leer cualquier cosa.
Lo que no conviene hacer
No le presentes Lean como un camino laboral. La verificación formal es un campo chico, y la mayoría de quienes lo aprenden lo usan para pensar mejor, no para conseguir empleo. La venta honesta es que es la lección más clara disponible sobre qué significa verificar, en un momento en que ese concepto está haciendo mucho trabajo.
Qué observar en los próximos 3 meses
- Semana 4: tu adolescente terminó al menos un mundo del Natural Number Game, o dijo en voz alta que nunca supo por qué 2 + 2 = 4.
- Señales de alerta en el mes 2: “es obviamente cierto” como sustituto de un argumento. Ese es el hábito que rompe la demostración formal.
- Autoevaluación del mes 3: sigue el avance en formalización automática. Si traducir demostraciones informales a Lean se vuelve mucho más barato, el cuello de botella se afloja y la matemática con IA cambia de carácter.
Preguntas frecuentes
¿Qué es Lean y quién lo usa?
Lean es un demostrador interactivo de teoremas, hoy en su cuarta versión, que usan matemáticos para escribir demostraciones que una computadora revisa mecánicamente. Su atractivo viene en buena parte de Mathlib, una biblioteca comunitaria con mucha matemática de grado y posgrado ya formalizada.
¿Un chico puede aprender de verdad un asistente de demostración?
Sí, con el Natural Number Game. Corre en el navegador en adam.math.hhu.de sin instalar nada, es gratis y de código abierto bajo Apache 2.0, y arranca desde los axiomas de Peano con metas tan elementales como demostrar que 2 + 2 = 4.
¿Lean garantiza que una demostración es correcta?
Garantiza que cada inferencia se sigue de los axiomas y de resultados previos, así que una demostración en Lean que compila es lógicamente válida. Lo que no puede garantizar es que hayas formalizado el enunciado que querías. Es el mismo modo de falla que un código que pasa las pruebas resolviendo el problema equivocado.
¿La demostración de Erdős de la IA se verificó en Lean?
No públicamente. OpenAI dice que matemáticos externos revisaron la demostración y escribieron un artículo acompañante, que es arbitraje humano y no verificación formal. No se anunció ninguna formalización en Lean de esa demostración.
¿Por qué no todos formalizan sus demostraciones?
Porque toma mucho más tiempo que escribir una demostración informal, a veces más que la investigación original. Ese costo es la razón del cuello de botella de verificación, y si la formalización automática puede reducirlo es una de las preguntas abiertas del campo.
Sobre el autor
Ricky Flores es el fundador de HiWave Makers e ingeniero eléctrico con más de 15 años de experiencia desarrollando tecnología de consumo en Apple, Samsung y Texas Instruments. Escribe sobre cómo los niños aprenden a construir, pensar y crear en un mundo saturado de tecnología. Lee más en hiwavemakers.com.
Fuentes
- Lean Prover Community. “Natural Number Game 4 (NNG4).” GitHub. https://github.com/leanprover-community/NNG4
- Lean Community. (2022, 14 de julio). “Completion of the Liquid Tensor Experiment.” https://leanprover-community.github.io/blog/posts/lte-final/
- Tao, T. (2025, enero). “Machine-Assisted Proof.” Notices of the American Mathematical Society, 72(1), 6–13. https://www.ams.org/notices/202501/rnoti-p6.pdf
- Kakaes, K. (2026, 3 de agosto). “Why the legendary Erdős problems are falling to AI.” Quanta Magazine. https://www.quantamagazine.org/why-the-legendary-erdos-problems-are-falling-to-ai-20260803/
- Lean Game Server. “Lean 4 Games.” https://adam.math.hhu.de/
- Argentinos por la Educación y MIT. (2026, 15 de enero). “Inteligencia artificial en la educación: desafíos y perspectivas.” https://www.diariodecuyo.com.ar/argentina/ia-en-las-escuelas-un-informe-destaca-los-beneficios-y-desafios-del-uso-sin-planificacion-1820537.html
- OECD. (2026). “PISA 2025 Results (Volume I): Future-Ready Students.” OECD Publishing. https://www.oecd.org/en/publications/pisa-2025-results-volume-i_73451bc5-en.html
