Búsqueda · 19 momentos en 15 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetdemostración wiles en lenguaje leanconjetura yimura formas modularesafirmaciones ribet implicancia teoremaformalización demostración teorema fermatWilesYimura TaniyamaRibetFrancis VillatoroLeanÚltimo teorema de FermatTomonori TotaniUniversidad de TokioGaiaPlanckArchivo de Datos Públicos
Yimura Taniyama
Con
0:000:301:001:302:002:303:003:15
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.
…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…
Significado #1 · Palabras #1
Héctor Socas introduce a Tomonori Totani, un investigador japonés de la Universidad de Tokio, destacando su nombre peculiar y su trayectoria en estudios de cosmología.
Habla: Héctor SocasSignificado #5investigador tomonori totani universidad tokiocosmología galaxias activas tomonori totanidatos misión gaia archivo público…grandes de Fermilat y la interpretación es delicada y va a requerir bastante más validación; o sea, que es un estudio interesante, revolucionario todavía no, va a haber que seguir profundizando en esto. El trabajo, como digo, lo firma un investigador que se Llama, a ver si lo digo bien: Tomonori Totani, que es japonés, como su propio nombre indica, de la Universidad de Tokio. La verdad es que el nombre es curioso, parece de un personaje, no sé, de Dragon Ball o algo así: Tomonori Totani y es un profesor de la Universidad de Tokio, un investigador con una carrera bastante asentada en estudios de cosmología, creo que también de galaxias activas y bueno, trabaja con el Archivo de Datos Públicos porque todas estas misiones, igual que Gaia, igual que Planck, pues los datos están en internet a disposición de quien quiera usarlos. Pero es un trabajo, insisto, de un único autor, lo cual está bien; no pasa nada, se puede. Yo también a veces tengo papers de un único autor, pero no hay que, bueno, quizás puede ser un primer paso, pero habrá que ver luego más validaciones de esto, porque en…
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 #1demostración wiles en lenguaje leanconjetura yimura formas modularesafirmaciones ribet implicancia teoremaformalización demostración teorema fermat…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…