Búsqueda · 24 momentos en 10 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetpruebas matemáticas lean equivalentes tradicionalesfactor de 10 pruebas lean vs papeldemostraciones lean mejorando tamañoterence tao lidera nueva visión matemáticodemostraciones wiles lean última versiónúltimo teorema fermat escrito en leanLeanFrancis VillatoroJuan Carlos GilRamanujanTerence TaoWilesÚltimo Teorema de Fermat
Factor de 10 pruebas Lean vs papel
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro explica cómo las pruebas matemáticas generadas con Lean son equivalentes a las tradicionales, aunque actualmente ocupan más espacio en formato digital.
…ayuda a explorar el código, ¿cómo se llama? Lint Lint, L-A-N, es el demostrador más famoso ahora mismo, y es un metademostrador. Te permite trabajar con un lenguaje bastante próximo al humano, pero es un lenguaje formal, ¿verdad? Si no me equivoco, Francis. Con lo cual, una vez que tienes la prueba, es equivalente a una prueba matemática tradicional con todos los símbolos matemáticos. Ahora mismo el factor es del orden de un factor de 10. Es decir, si en hojas de papel, a mano, a ti te ha cubierto, yo que sé, 100 páginas, en Lean vas a obtener algo que lo puedes escribir en unas 1.000 páginas. y está mejorando, ¿eh? Se está mejorando para reducir ese tamaño y que un matemático entonces ya puede leer esa demostración, es quita por Lean. Se tiene que acostumbrar; hay que acostumbrarse a eso, ¿no? Entonces ahora mismo está liderando esa nueva manera de ver la labor del matemático Tao y estamos autorizando que muchísima gente se esté planteando en serio el sistemáticamente pasar todas las demostraciones. Ahora mismo uno de los temas, por ejemplo, la demostración de Wiles, el último teorema de Fermat, está ahora mismo escribiéndose en Lean. Ahora mismo eso puede costar del orden de un año, ¿por qué? Porque hay que pasar toda la demostración de Wiles, pero además todo lo publicado previo en lo que se basa en Wiles. Porque Wiles se basa en 30 años de matemática, entonces tienes que codificar una barbaridad de conocimiento de matemática. La conjetura de…
Significado #1 · Palabras #1
Francis Villatoro describe cómo el uso de herramientas como Lean permite detectar errores incluso en demostraciones matemáticas complejas realizadas por figuras destacadas como Terence Tao.
Habla: Francis VillatoroSignificado #12lean detección errores demostraciones taoterence tao demostración matemática leanlean certificación demostración matemáticalean validación demostraciones matemáticasdemostrador automático artículo matemáticorevisores artículo mundo detalle…de Tao, de Terence Tao, el matemático más famoso de la actualidad? Que se encontró una pequeña sutileza en una de sus demostraciones. Uy, aquí hay un pequeño error y nadie se había dado cuenta hasta el momento. Es verdad que esas demostraciones las ven 4 o 5. Matemáticos en el mundo. El resto de los matemáticos confiamos en que está bien demostrado; no entramos en los detalles, pero se detectó, gracias a pasar esa demostración a Lean, se detectó un error que rápidamente dijo: esto lo resuelvo yo con la punta al nabo, y lo arregló en un momentillo y lo arregló, ¿vale? Y ya está certificado por Lean. Y ahora está habiendo una corriente en matemáticas de decir: todo matemático en su carrera tiene que aprender a utilizar este tipo de herramientas porque dentro de una serie de años, puede que sean 10 años, a todos los matemáticos se les va a exigir que todas las demostraciones estén en Lean y estén validadas por un ordenador. Un demostrador automático va a tener que garantizar que tu artículo es correcto, matemáticamente correcto, no porque tú lo digas o porque lo digan los dos o tres revisores que han visto tu artículo, que puede que sean las únicas personas en el mundo que acaben leyéndose en detalle, no, no, porque una máquina diga que tu resultado es correcto. Y esa es una tendencia que ahora está. Liderando Terence Tao, que está colaborando con Google DeepMind, que tiene unos programas de generación automática de pruebas y a él le están pagando, le están financiando muy bien porque, por cierto, el señor Trump le quitó su proyecto de investigación y al…
Juan Carlos Gil explica la diferencia entre el uso de Lean para verificar demostraciones matemáticas y los métodos tradicionales, como la prueba por fuerza bruta o simetría.
Habla: Juan Carlos GilSignificado #2 · Palabras #2lean verificación demostraciones matemáticasprueba por fuerza bruta teoremas matemáticossimetría cumplimiento teoremas matemáticos…él está publicitando toda esta línea que está trabajando ahora, que son cosas de los últimos meses. Está vendiendo los resultados de manera absolutamente increíble, te pone todo el chateo con la inteligencia artificial. Te lo publica junto con el código. Lean y la demostración de que todo ha funcionado. Pero ojo, que eso es un código de un lenguaje que han desarrollado para hacer pruebas formales. Claro, es para demostrar que una demostración es correcta. El otro tipo de pruebas tradicionales matemáticas, de teoremas matemáticos, era probar por fuerza bruta o utilizando simetría y tal, pues que se cumplía en todos los casos. Me parece, vamos, nada que ver. Esta demostración formal con un lenguaje ad hoc que sepa matemáticas, a mí me parece lícita. Mientras que la otra siempre te queda, como decía Héctor, pero ¿no se les habrá olvidado el caso del subcaso del tercer caso? Sí, el…
Francis Villatoro reflexiona sobre el futuro de las matemáticas y cómo los verificadores automáticos están transformando la disciplina.
Habla: Francis VillatoroPalabras #5verificadores automáticos matemáticasasignatura herramientas matemáticas carrerarevistas validación máquina matemática…de casos, pero eran millones de casos que había que estudiar uno a uno y se estudiaban por ordenador, con una serie de propiedades que tenían que cumplir, entonces cada caso había que estudiarlo y siempre estaba con la duda de si se ha dejado algún caso. Acababa obteniéndose una prueba con ese tipo de verificadores automáticos y ahora está de moda. Entonces, el futuro dentro de 10, 15 años es que hay una asignatura en la carrera de matemáticas para aprender a usar estas herramientas y que todo se haga de esta manera. O sea, y que las revistas digan: esto es verdad solo si la máquina lo dice. Y para que la máquina lo diga, tú tienes que haber pasado todo lo que tú has dicho, todo lo que tú has escrito en papel, a la máquina. Pero déjame que lo vuelva a decir, que no sé si yo mismo lo he entendido bien, o sea, no. Es que Tao esté haciendo inteligencia artificial generativa, inventándose cosas, no; la herramienta le ayuda a explorar el código, ¿cómo se llama? Lint Lint, L-A-N, es el demostrador más famoso ahora mismo, y es un metademostrador. Te permite trabajar con un…
Francis Villatoro explica cómo las pruebas matemáticas generadas con Lean son equivalentes a las tradicionales, aunque actualmente ocupan más espacio en formato digital.
Habla: Francis VillatoroSignificado #1 · Palabras #1pruebas matemáticas lean equivalentes tradicionalesfactor de 10 pruebas lean vs papeldemostraciones lean mejorando tamañoterence tao lidera nueva visión matemáticodemostraciones wiles lean última versiónúltimo teorema fermat escrito en lean…ayuda a explorar el código, ¿cómo se llama? Lint Lint, L-A-N, es el demostrador más famoso ahora mismo, y es un metademostrador. Te permite trabajar con un lenguaje bastante próximo al humano, pero es un lenguaje formal, ¿verdad? Si no me equivoco, Francis. Con lo cual, una vez que tienes la prueba, es equivalente a una prueba matemática tradicional con todos los símbolos matemáticos. Ahora mismo el factor es del orden de un factor de 10. Es decir, si en hojas de papel, a mano, a ti te ha cubierto, yo que sé, 100 páginas, en Lean vas a obtener algo que lo puedes escribir en unas 1.000 páginas. y está mejorando, ¿eh? Se está mejorando para reducir ese tamaño y que un matemático entonces ya puede leer esa demostración, es quita por Lean. Se tiene que acostumbrar; hay que acostumbrarse a eso, ¿no? Entonces ahora mismo está liderando esa nueva manera de ver la labor del matemático Tao y estamos autorizando que muchísima gente se esté planteando en serio el sistemáticamente pasar todas las demostraciones. Ahora mismo uno de los temas, por ejemplo, la demostración de Wiles, el último teorema de Fermat, está ahora mismo escribiéndose en Lean. Ahora mismo eso puede costar del orden de un año, ¿por qué? Porque hay que pasar toda la demostración de Wiles, pero además todo lo publicado previo en lo que se basa en Wiles. Porque Wiles se basa en 30 años de matemática, entonces tienes que codificar una barbaridad de conocimiento de matemática. La conjetura de…
Francis Villatoro describe una actitud anterior entre los matemáticos hacia el uso de Lean, un lenguaje de verificación matemática, comparándola con la actual valoración que se le está dando.
Habla: Francis VillatoroSignificado #4matemáticos rechazan leanramanujan frente a leanrevisión artículo dos años…que abarco en mis matemáticas y me parece fascinante lo que está haciendo. O sea, y ya te digo, está generando una tendencia en la que muchos matemáticos están empezando a valorar esto porque hace un año y medio el 99,9% de los matemáticos puede asegurar que Se negaba rotundamente a usar Lean. Eso es de inútiles, solo los inútiles requieren formalizar y que la máquina les diga que lo han hecho bien. No, no, no: aquí el matemático de pro tiene que mirárselo página a página y si para revisar un artículo hay que dedicarse dos años de revisión, pues le dedicamos dos años de revisión. Y ahora me imaginaba a Ramanujan con el link este delante; os imagináis. Ramanujan era otra cosa; es que Ramanujan no sabía demostrar, no era capaz de demostrar, no valoraba demostrar. Era un matemático que se dedicaba a jugar con desarrollos convergentes y divergentes y a operar con ellos, y era muy bueno, muy rápido haciendo…