Búsqueda · 17 momentos en 5 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetterence tao demostración matemáticasutileza error prueba taodemostración tao vista por cuatrolean 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 detalleterence tao google deepmindgeneración automática pruebasfinanciación proyecto terence taodonald trump investigación universidadLeanTerence TaoWilesÚltimo Teorema de FermatInteligencia ArtificialJuan Carlos GilLintFrancis VillatoroNatureMastodonGoogle DeepMindDonald TrumpRamanujan
Terence Tao demostración matemática Lean
Con
0:000:301:001:302:002:303:003:15
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.
…que lo haya hecho todo bien, que no haya ningún resquicio, pero en pocos días puedes transferir tu demostración en papel a una demostración por ordenador, pasársela al demostrador automático y el demostrador automático te dice sí, no te has equivocado. ¿O ha pasado con demostraciones 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 instituto que tenía en su universidad le quitaron la financiación. ¿Y qué ha hecho Tao? En algún momento llegó a decir: pues me voy a Europa. Pero después dijo: ¿irme a Europa? Hablo con Google, que me financie Google. Y le está financiando Google, ¿vale? Con dos cojones. Ahora mismo, Google DeepMind está financiando a Tao,…
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 #1 · Palabras #1terence tao demostración matemáticasutileza error prueba taodemostración tao vista por cuatrolean 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 detalleterence tao google deepmindgeneración automática pruebasfinanciación proyecto terence taodonald trump investigación universidad…que lo haya hecho todo bien, que no haya ningún resquicio, pero en pocos días puedes transferir tu demostración en papel a una demostración por ordenador, pasársela al demostrador automático y el demostrador automático te dice sí, no te has equivocado. ¿O ha pasado con demostraciones 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 instituto que tenía en su universidad le quitaron la financiación. ¿Y qué ha hecho Tao? En algún momento llegó a decir: pues me voy a Europa. Pero después dijo: ¿irme a Europa? Hablo con Google, que me financie Google. Y le está financiando Google, ¿vale? Con dos cojones. Ahora mismo, Google DeepMind está financiando a Tao,…
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 #7terence tao google deepmind demostracionespublicación nature herramientas inteligencia artificialresultados matemáticos mastodon taointeligencia artificial chateo códigolean verificación demostraciones matemáticasprueba por fuerza bruta teoremas matemáticossimetría cumplimiento teoremas matemáticos…¿vale? Con dos cojones. Ahora mismo, Google DeepMind está financiando a Tao, que Tao use las herramientas de interés artificial más avanzadas del mundo, que no están disponibles para nadie más que para él, porque está cogiendo el state of the art y los que Están publicando lo van a publicar en Nature, a lo grande, y está pasando demostraciones extremadamente complicadas a este tipo de herramientas de manera muy rápida. Habla en Mastodon, é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 explica que Terence Tao está liderando una nueva forma de ver la labor del matemático y que se están considerando sistemáticamente pasar todas las demostraciones a Lean.
Habla: Francis VillatoroSignificado #3 · Palabras #2terence tao inteligencia artificial generativalint demostrador más famosolenguaje formal cercano al humanopruebas 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…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 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 reflexiona sobre cómo Terence Tao está impulsando una revolución en la demostración matemática, anticipando que los matemáticos jóvenes adoptarán estas técnicas en las próximas décadas.
Habla: Francis VillatoroSignificado #2 · Palabras #5terence tao usa lean inteligencia artificiallean formaliza demostraciones matemáticas sencillasinteligencia artificial sugiere conexiones matemáticas taoterence tao revoluciona demostración matemáticamatemáticas jóvenes adoptarán técnicas taodemostración en matemáticas próxima décadaterence tao matemáticas revolucionariasvaloración creciente enfoque taotendencia entre matemáticos taomatemáticos rechazan leanramanujan frente a leanrevisión artículo dos años…Todo eso ahora mismo lo están formalizando y los rumores eran que era inminente que acabaran, o sea que puede ser para mediados del año que viene o para finales del año que viene que lo tengan listo y entonces podrás certificar que no hubo ningún error. y ahora mismo incluso Tao está haciendo otra cosa que es también maravillosa que es desarrollar nuevas demostraciones apoyado en los códigos de Lean. O sea, conforme tú estás buscando ideas para demostrar algo, las vas formalizando en ejemplos más o menos sencillos en Lean y la inteligencia artificial te va ayudando a ver nuevas ideas. entonces Tao ya tiene varios ejemplos en los que la inteligencia artificial le ha dado a la hora de formalizar en el Lean lo que le estaba escribiendo una idea que él no tenía, una conexión con esto no había pensado, pero ahora que lo pienso pues es una buena idea y entonces está acelerando ese proceso de búsqueda de ideas a la hora de demostrar y ya tiene varios ejemplos y son absolutamente fascinantes, claro eso ahora mismo lo puede hacer pues Dios En matemáticas, Terence Tao, pero que ya no es un niño, que ya no tiene 30 años, que ya tiene sus 50 a largo, pero probablemente eso lo aprendan a hacer los matemáticos jóvenes en las próximas décadas y lo haga todo el mundo, por lo que promete una enorme revolución a lo que es la demostración en matemáticas. A mí me parece muy valiente por parte de Tao, yo soy muy equipo Tao, pero poquísimo 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…