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…
Francis Villatoro explica cómo los matemáticos aficionados trabajaron en una conjetura llamada propiedad de Rupert, tras observar fenómenos similares a los del cubo RGB en otros poliedros.
Habla: Francis VillatoroPalabras #10propiedad rupert poliedrosmatemáticos aficionados conjetura rupertcontraejemplo propiedad ruperto español…que ocurre con el icosaedro, que ocurre con el dodecaedro. Y después ya empezaron a complicar a poliedros más complicados, que mezclan caras de diferentes tipos. Y prácticamente en todos los que se estudiaban ocurre. Entonces tú decías: ¿esto ocurre siempre? Entonces se conjeturó que todos los poliedros cumplían con esta propiedad, a la que se llamó propiedad de Rupert, o de Ruperto en español. Claro, una conjetura; hay dos maneras de trabajar con ella, de resolver el problema de la conjetura, o de mostrar que es verdad y todo. Hubo mucho trabajo, sobre todo de matemáticos aficionados, para tratar de demostrar que era verdad o de encontrar un contraejemplo. Y aquí es donde se acaba de publicar un contraejemplo. Dos matemáticos austríacos que no son matemáticos profesionales en el sentido de que estén en una institución, pero sí son gente que está asociada al campo de la matemática, son gente que trabaja y vive de haber hecho la carrera de matemáticas, pero no…
Francis Villatoro explica cómo Jakob Steininger y Sergei Jurkevich han encontrado un nuevo poliedro que cumple con la hipótesis de Rupert y han publicado una demostración matemática en un artículo de 35 páginas.
Habla: Francis VillatoroSignificado #15algoritmo para atacar el problema rupertpoliedro hipótesis rupertartículo demostración matemática steininger jurkevichconjetura poliedros prueba rupert…si no lleva por detrás una demostración matemática y estos dos señores no fueron capaces de demostrar en 2021 y desde entonces ningún otro matemático ha sido capaz de demostrar que ese rhombicócido de caedro realmente no cumpla con la propiedad de Roper Entonces ellos han seguido trabajando porque a ellos, claro. O sea, era una conjetura de que la otra conjetura era falsa. Eso es, un poco así. Bueno, han seguido trabajando, mejorando por un lado su algoritmo y por otro lado mejorando su manera de atacar el problema. Y han Encontrado un nuevo poliedro que ahora sí el programa les dice que cumple con la hipótesis de Rupert. Y han sido capaces de demostrar matemáticamente que lo cumple. Ahora sí, se ha publicado el 27 de agosto de 2025; es un artículo de 35 páginas con la demostración. Francis, que no lo cumple, que has dicho. Exactamente, que no cumple, que no cumple con la prueba de Rupert. O sea, que es un contraejemplo a la conjetura. La conjetura de que todo poliedro la tiene que cumplir. Entonces, este es un... bueno, le llaman Norped... Norped... Norpedron, ahora sí Déjame un poco, es un juego de palabras, es un juego de palabras un poco sutil en inglés, que es bastante divertido en mi opinión, le llaman no percedron, no en inglés, pero se puede leer como nope,…
Francis Villatoro explica que, además de la conjetura de Rappert, existe otra conjetura sobre los posibles contraejemplos, sugiriendo que estos serían objetos intermedios entre un cubo y una esfera.
Habla: Francis VillatoroSignificado #9 · Palabras #7conjetura rappert contraejemplosobjetos intermedios cubo esferanorropertedros nopertedros región concretacontraejemplo cubo esferadeformaciones objeto poliedrotamaño región espacio poliedros…está acompañada con un software que hay que ver también; hay que validarlo. Validar software en matemáticas suele ser complicado y requiere un trabajo muy fino de los revisores, pero en cualquier caso es una cuestión puramente anecdótica y lo que nos aclara. Es una cosa importante. Aparte de la conjetura de Rappert, había otra conjetura que decía que si se encontraban contraejemplos, probablemente serán objetos intermedios entre el cubo y la esfera y que marcarían una pequeña región en la que se encuentran esos objetos. O sea, se ha conjeturado que los objetos, estos norropertedros o nopertedros, como queramos llamarle, definen una región muy concreta dentro de lo que es la transición entre el cubo y la esfera. Y eso es ahora el problema nuevo abierto que habrá que resolver. Ya tenemos un contraejemplo, ya sabemos que esa región no está vacía, que ahí hay más de un objeto; pequeñas deformaciones en este objeto conducen a objetos parecidos, que también cumplen con esta propiedad, pero hay que ver hasta cuándo, ¿no? O sea, qué tamaño hay que, de alguna manera, cuantificar qué tamaño tiene esta región de todo el espacio de posibles poliedros, que se encuentra, digamos, entre formas tipo cubo y formas tipo esfera, para ver un poco… Para continuar trabajando en esto, pero eso es una labor fundamentalmente para matemáticos aficionados y bueno, estos han tenido ya. Su pequeño 15 minutos de gloria porque Cuanta Magazine, que bueno, les ha publicado un articulito. Cuanta Magazine recibe financiación de fondos privados para divulgar ciencia y bueno, hay varios articulistas especializados en matemáticas que están…
Juan Carlos Gil expresa su decepción al descubrir un contraejemplo a una conjetura matemática popular, comparando la experiencia con otras situaciones similares. Menciona la belleza del ejemplo del cubo y la rareza de que un poliedro no quepa dentro de sí mismo.
Habla: Juan Carlos GilSignificado #11cubo ejemplo bonitopoliedro cabe dentro sí mismoencaje práctico perfectouniverso hecho para copiar…te cuenta también la historia de los investigadores, etc. O sea, está bastante divertido. Una pregunta: cuando una conjetura así visual que todo el mundo puede entender y que lleva años y que hay mucha gente detrás, de repente se encuentra un contraejemplo, a mí me da un bajón, me ha pasado con otras. Es una pena, ¿no? ¿Os imagináis un poliedro que cabe dentro, que se puede hacer un túnel para que quepa dentro de sí mismo? Ya solo el ejemplo del cubo es muy bonito. No se ha encontrado ninguno, lo habían probado con varios y varios se habían encontrado que sí, que caben. Lo normal es que quepa, lo raro es el no Rupert Pedro Sí, el ejemplo más ajustado, conocido, creo que era que la diferencia era como 0,50, un 2 Eso es, es que estaba... Era un encaje prácticamente perfecto Es que parece que nuestro universo estaba hecho para que copiese todo, Jorín Y eso de... Una pregunta personal, Francis. ¿Una pregunta privada como matemático? No, porque recordé esto que hablabas de las pruebas por computadora, o las pruebas, como dicen los matemáticos, asistidas por computadoras, ¿no? Al menos en inglés la traducción sería esa.…
Gastón Giribet relaciona la discusión sobre una demostración de la conjetura de Kepler, que involucra apilar esferas en generalizaciones dimensionales de tetraedros, con el debate anterior sobre demostraciones asistidas por computadora.
Habla: Gastón GiribetPalabras #18conjetura de kepler apilar esferasdemostraciones asistidas por computadora tetraedroscómputo casos infinitos…esas huevadas a mí no me vengan. Pero era la primera vez que la revista se abría, hace 20 años, a la posibilidad de empezar a publicar esas cosas. Se notaba en MacPherson que él no parecía estar muy de acuerdo; no parecía mostrar su aquiescencia con esa idea. Pero en ese momento se estaba discutiendo acerca de una de las demostraciones sobre la conjetura de Kepler, que en algún sentido tiene un espíritu parecido a esto: las formas óptimas de apilar esferas en generalizaciones dimensionales de los tetraedros. Entonces, esas demostraciones también eran asistidas por computadora; uno podía probar, no sé, probaba algo y si estaba seguro con 124 casos o con 1026 casos, entonces probaba los infinitos. Pero esos 1020 y tantos casos había que hacerlo por computadora. Entonces, vos siendo matemático, pero siendo más afín a otras ciencias en las cuales el cálculo, el cómputo es importante, ¿vos cómo te sentís acerca de las demostraciones asistidas por computadora? Acá viene lo personal. Bueno, a nivel personal, al matemático de toda la vida lo que nos gusta es disfrutar de la comprensión de la demostración; o sea, el avance en matemáticas es un avance a base de comprender objetos, de comprender cosas. Hay una serie de…
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…