Búsqueda · 20 momentos en 7 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetlean verificación demostraciones matemáticasprueba por fuerza bruta teoremas matemáticossimetría cumplimiento teoremas matemáticosLeanJuan Carlos GilTerence TaoChatGPTFrancis VillatoroRamanujanWilesÚltimo Teorema de FermatYimura TaniyamaRibet
Lean verifica demostración problema Matemático
Con
0:000:301:001:302:002:303:003:15
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.
…é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…
Significado #1 · Palabras #13
Francis Villatoro explica cómo la Inteligencia Artificial Generativa, como ChatGPT, está automatizando el proceso de transferir demostraciones matemáticas escritas a mano a un formato digital para su verificación.
Habla: Francis VillatoroPalabras #6chatgpt construye demostraciones leantransferencia automatizada demostraciones matemáticasdemostrador automatico verifica errores…pero muy poca gente los usaba. ¿Por qué? Porque dedicar tiempo a pasar tu demostración escrita a mano a un demostrador automático requería años de trabajo para después que resulte que el demostrador automático diga: pues sí, no te has equivocado, es correcta. Pero ahora mismo con la Inteligencia Artificial Generativa, ChatGPT y compañía podemos automatizar ese proceso. Las demostraciones en Lean, L-A-N, es fácil, claro; el ChatGPT más o menos te la construye y tú tienes que estar como, es tu demostración, tú tienes que estar controlando 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…
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 #4 · Palabras #8lean 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 #1 · Palabras #13lean 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 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 #12pruebas 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 leandemostración wiles en lenguaje leanconjetura yimura formas modularesafirmaciones ribet implicancia teoremaformalización demostración teorema fermat…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 Yimura Taniyama primero de las formas modulares y las L-series y todo eso, después las afirmaciones que eran Ribet y todos esos que mostraban cuál era la implicancia mutua entre las conjeturas y el teorema. 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…
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 #14 · Palabras #18matemá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…