Búsqueda · 21 momentos en 12 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetteorema fermat demostrado técnicasbelleza demostraciones problemas resueltosúltimo teorema de FermatFrancis VillatoroWilesYimura TaniyamaRibetLeanTerence TaoHéctor SocasJuan Carlos GilInteligencia Artificial
Formalización demostración teorema Fermat
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro expresa su falta de satisfacción al saber que el teorema de Fermat ha sido demostrado, enfatizando su interés en comprender los métodos y técnicas utilizados para llegar a esa conclusión.
…¿Entender esa demostración? De tratar de entender los elementos y el juego de ideas que se ha llevado en esa demostración, esa es la belleza y el placer de la demostración. El saber por saber que algo es verdad, saber que uno más uno es igual a dos, pues para Mí no me genera ningún tipo de placer, o sea, saber que el teorema de Fermat se ha demostrado; pues ya está, pues el último teorema de Fermat. Pero quiero saber cómo se ha demostrado, con qué técnicas, qué camino se ha seguido, qué problemas se han resuelto que antes no se podían resolver, ¿no? Entonces, esa es la belleza de las demostraciones. Y eso se pierde un poco con las demostraciones que dependen mucho de programas de ordenador. Sobre todo cuando un ordenador ha tenido que probar, yo qué sé, miles de millones de casos o millones de casos. Y no se les ha escapado a uno. O sea, ¿cómo estoy seguro de que no se les ha escapado a uno? Ahí volvemos al no estar del todo seguro, porque son…
Significado #2 · Palabras #1
Francis Villatoro expresa su falta de satisfacción al saber que el teorema de Fermat ha sido demostrado, enfatizando su interés en comprender los métodos y técnicas utilizados para llegar a esa conclusión.
Habla: Francis VillatoroSignificado #2 · Palabras #1teorema fermat demostrado técnicasbelleza demostraciones problemas resueltos…¿Entender esa demostración? De tratar de entender los elementos y el juego de ideas que se ha llevado en esa demostración, esa es la belleza y el placer de la demostración. El saber por saber que algo es verdad, saber que uno más uno es igual a dos, pues para Mí no me genera ningún tipo de placer, o sea, saber que el teorema de Fermat se ha demostrado; pues ya está, pues el último teorema de Fermat. Pero quiero saber cómo se ha demostrado, con qué técnicas, qué camino se ha seguido, qué problemas se han resuelto que antes no se podían resolver, ¿no? Entonces, esa es la belleza de las demostraciones. Y eso se pierde un poco con las demostraciones que dependen mucho de programas de ordenador. Sobre todo cuando un ordenador ha tenido que probar, yo qué sé, miles de millones de casos o millones de casos. Y no se les ha escapado a uno. O sea, ¿cómo estoy seguro de que no se les ha escapado a uno? Ahí volvemos al no estar del todo seguro, porque son…
Francis Villatoro explica cómo la inteligencia artificial generativa está cambiando la forma en que los matemáticos abordan las demostraciones, contrastando con el uso limitado de demostradores automáticos en el pasado.
Habla: Francis VillatoroSignificado #10inteligencia artificial generativa matemáticosdemostradores automáticos uso limitadoformalizar demostraciones ordenador matemático…de 200 páginas que supuestamente demuestra que una máquina es capaz de demostrar que eso es correcto; pero te quedas como diciendo, me falta algo. Y es el problema que tenemos ahora mismo en matemáticas: es que está habiendo una revolución con el tema de La inteligencia artificial generativa y es que hasta hace muy poquito tiempo, un matemático le daba miedo formalizar en ordenador las demostraciones. Hay demostradores automáticos desde hace 50 años, 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ú…
Juan Carlos Gil comenta sobre la validez de las demostraciones formales en un lenguaje específico para matemáticas, contrastándolas con métodos tradicionales como la prueba por fuerza bruta.
Habla: Juan Carlos GilSignificado #9demostración formal lenguaje ad hocprueba por fuerza bruta juan carlos gil…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 problema más famoso es el de los cuatro colores, todavía no tenemos. Una demostración a mano del teorema de los cuatro colores. Es verdad, ¿cuántas hojas tenía eso? Era increíble. El código era terrible, o sea, es una cosa absolutamente... no recuerdo el número de casos, pero eran millones de casos que había que estudiar uno a…
Francis Villatoro explica el proceso de formalización de la demostración de Wiles sobre el último teorema de Fermat en Lean, un lenguaje de verificación matemática, destacando la enorme cantidad de conocimiento matemático previo involucrado.
Habla: Francis VillatoroSignificado #1 · Palabras #2terence 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 fermatterence tao usa lean inteligencia artificiallean formaliza demostraciones matemáticas sencillasinteligencia artificial sugiere conexiones matemáticas tao…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 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…