Búsqueda · 17 momentos en 10 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetpropiedad roper en poliedrosjakob steininger programa informáticosergei jurkevich orientaciones preferencialesespacio de orientaciones poliedrorombicosido decaedro contraejemplo ropermatemáticos exigen demostración rigurosapropiedad de rupert poliedrosalgoritmo para atacar el problema rupertpoliedro hipótesis rupertartículo demostración matemática steininger jurkevichconjetura poliedros prueba rupertconjetura de rupert no percedronjuego de palabras norpedron inglésno rupert pedro poliedroconjetura de rupert pedroadaptación nombre español rupert pedrosólido con cara de 15 ladosforma esférica triangulitosanécdota mauricio lesto subsidiofirma falsificada curva derechaburocracia para subsidio desconocidopoliedro cara inferior irrelevanteartículo poliedro firma radiadafalsificar poliedro directamente inventadodemostración matemática poliedro roperespacio de orientaciones algoritmopoliedro ejemplo 2021 sin demostraciónFrancis VillatoroJakob SteiningerSergei Jurkevichpropiedad de RupertRupertInglésEspañolJuan CarlosNo Rupert Pedropropiedad de RoperCuanta MagazineJuan Carlos Gilpríncipe Rupertosiglo XVIICarlos I de InglaterraRupertoHéctor SocasCoffee Break: Señal y RuidoLeanMartin GarnerScientific AmericanWilesYimura TaniyamaRibetÚltimo teorema de FermatJohn WallisMauricio LestoGastón Giribet
Conjetura poliedros prueba Rupert
Con
0:000:301:001:302:002:303:003:15
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.
…y Sergei Jurkevich, que se conocieron de estudiantes en la Olimpiada de Matemáticas y que han seguido colaborando en varios problemas así de matemática recreativa, uno de ellos este. Ellos desarrollaron en 2021 un programa de ordenador para comprobar. Si un poliedro, visto desde todas las posibles caras, eso requiere definir lo que llaman una especie de orientaciones preferenciales; es decir, dado un poliedro se construye una especie de espacio de orientaciones en las que tú garantizas de que mirando en esta orientación pequeñas variaciones en esta orientación hacen que el poliedro siga manteniendo esa propiedad, la propiedad de Roper. Entonces logran para definir dado un poliedro un espacio, digamos otro poliedro de orientaciones que son hechos de triángulos y chequean en cada uno de esos triángulos si se cumple o no se cumple la propiedad de Roper y encontraron. en 2021 un primer candidato a demostrar que era un poliedro que no cumplía con la condición de Roper, que era el rombicosido decaedro, que tiene 62 triángulos, tiene triángulos cuadrados y pentágonos, regulares. pero los matemáticos somos como somos y no nos gusta que se nos diga hemos encontrado un contraejemplo 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, como no, nope, ¿no? Como dicen a veces en eso, entonces es el no percedron, porque no cumple la cosa Es por Rupert, cambiar Rupert por Noper Exacto, Rupert por Noper, pero el Noper, como empieza por N-O-P-E es Noper, ¿no? Y es divertido Yo creo que en español le tendremos que llamar No Rupert Pedro No Rupert Pedro, bueno, sí, en español sería más natural llamarlo No Rupert Pedro por el tema de que en español asociamos el apellido pero bueno, es un sólido que tiene como una cara de 15 caras, perdón, tiene la cara superior de 15 lados, después tiene como triangulitos que hacen una forma así como esférica y después tiene la cara de abajo que yo no sé por qué razón en el artículo nos dicen cuántas caras Mira que te dije que no necesitaras describirlo Bueno, hay que intentar describirlo, ¿vale? O sea, es un poliedro con 90 vértices, 240 vistas, 152 caras. No se me acordaba a mi amigo Mauricio Lesto, en que una vez estábamos haciendo una burocracia para un subsidio, no voy a decir de dónde, para que no tengamos que devolver el dinero y me dijo: falsifica mi firma, digo, bueno, dale; estábamos acostumbrados a hacer eso. Me dice: bueno, te digo cómo es, hace una curva más o menos abierta para la derecha. Digo, vos me estás jodiendo. Es muy raro. O sea, él es un chico normal. Es muy raro esto que hizo. Digo, yo pensé que era un chiste. Pero uno me decía: bueno, ahora pegarle una vuelta para abajo. Pero medio abrupta. Nunca había oído eso. Radiar una firma. Es que es buenísimo. Sí, sí, sí. Lo habitual es falsificarla directamente; te la inventas y ya está. Ay, ay, ay. Bueno, en cualquier caso. Es un poliedro, ¿vale? Y la cara superior tiene 15 lados y la cara inferior, que en los dibujitos no se ve, pero que en el artículo tampoco pone cuántas caras tiene. Pero bueno, parece como que es irrelevante realmente para los autores del artículo; es irrelevante realmente la figura. Lo relevante es la demostración matemática; se basa en combinar ese espacio de orientaciones que ellos han definido previamente con un razonamiento matemático riguroso. Entonces demuestran que bajo ciertas condiciones en el poliedro, si el algoritmo dice que no cumple con la propiedad de Roper, es que es verdad que no la cumple. Algo que no pueden demostrar para el otro ejemplo que tenían en 2021, que es parecido pero es diferente; y con ese todavía no han logrado afinar una demostración que garantice que ahí el algoritmo funcione. Entonces, bueno, todo esto por supuesto se acaba de publicar; los detalles de la demostración no parecen complicados de entender, pero yo no puedo asegurar que esté correcta, ¿vale? Habrá que esperar a que se publique en alguna revista y verificar que realmente es correcta, pero tiene buena pinta, ¿vale? Tiene buena pinta y está acompañada con un software que hay que ver también; hay que validarlo. Validar software en matemáticas suele…
Significado #1 · Palabras #1
Héctor Socas propone a Francis Villatoro elegir entre dos temas: uno de curiosidad matemática y otro relacionado con el cerebro, sugiriendo priorizar el primero para la discusión actual.
Habla: Héctor SocasPalabras #11curiosidad matemática rupertocerebro tema para la semanaruperto elección de francis villatoro…dicen que no es para tanto; entonces el que tenga que tomar las decisiones, que igual no es científico de idea, pues no les hago caso y es peligroso. Gracias a la entrada de Ortega, pero ni ustedes mismos se ponen de acuerdo, más soberbios. Bueno, algo así. Francis, nos quedan dos temas tuyos: uno que parece más simpático, más curiosidad matemática, y otro, pues quizás más que tiene que ver con el cerebro. ¿Cuál te gustaría para contar ahora y cuál dejamos para la semana que viene? Yo voto por el Ruperto, si puede ser. Por el Ruperto, venga, pues hablo del Ruperto. Vale, venga, pues vamos con el Ruperto, que es una cosa que a mí también me llamó mucho la atención De hecho, esto tengo que dar las gracias que me lo envió nuestro oyente Kim Forner Como un artículo que había visto por ahí que le despertó curiosidad Y es un…
Francis Villatoro explica un problema matemático relacionado con una apuesta entre una persona anónima y el príncipe Ruperto, sobrino de Carlos I de Inglaterra.
Habla: Francis VillatoroPalabras #16apuesta príncipe ruperto carlos icubo agujero otro cubosombra cubos idénticos…nos lo podrá explicar bien pero eso que tiene que, bueno, explícalo tú, venga, no voy a introducir más Sí, bueno, estos cuestiones que aparecen en matemáticas que tienen una cierta historia y que, bueno, se recuerda más el asunto por la historia que otra cosa Se supone que parte de una apuesta entre una persona que ahora es anónima, no sabemos quién es, contra el famoso príncipe Ruperto, que era sobrino de Carlos I de Inglaterra, y entonces uno apostó contra el otro que si yo tengo un cubo y tengo otro cubo idéntico, yo puedo hacerle un agujero a uno de los cubos por el cual quepa el otro cubo. O sea, los dos cubos son idénticos, son el mismo cubo. Esto se ve por la sombra, ¿vale? Todos hemos recordado, bueno, todos los que conozcan, todos los que hayan utilizado Photoshop o cualquier programa de diseño gráfico, habrán recordado que el cubo de colores RGB, que es un cubo, que tienes el rojo, azul y verde, se suele dibujar visto desde uno de los vértices. Tú coges uno de los vértices del cubo y lo…
Francis Villatoro continúa explicando un problema matemático relacionado con una apuesta entre el príncipe Ruperto y un individuo anónimo, contextualizándola en el siglo XVII.
Habla: Francis VillatoroSignificado #10 · Palabras #12apuesta príncipe ruperto siglo xviihexágono regular más grande cubomatemático popularizó apuesta realjohn wallis anécdota matemática históricagobernante ruperto sin antibióticos…como un hexágono en la pantalla. Y si ponéis el cubo correspondiente a ese hexágono, o sea, cogéis el lado del hexágono y ponéis un cuadrado, que sería la sombra del cubo en forma de cuadrado, veréis que el cuadrado es un pelín más pequeño que el hexágono. Ese hexágono que tiene un lado igual que cada cara del cubo es un hexágono regular que es un pelín, un 4% más grande que el cubo. Conocida, y ya os digo, esta historia de Ruperto es del siglo XVII, de 1680 o 90, por ahí. Es que Ruperto ganó la apuesta; él dijo que sí cabía, ¿no? Exactamente. Y el rey ganó. Y el rey ganó, y esto lo popularizó un matemático. John Wallis, muy famoso de la época, que comentó la anécdota, ¿vale? No sabemos si la anécdota es real o no, pero bueno. Y esto era de un rey en la época en la que no había ni antibiótico ni nada. Así que cada vez que ustedes creen que su gobernante está haciendo pelotudeces, imagínense la cosa que hacía Ruperto y todo el mundo le parecerá trabajador. Por lo menos hacía matemáticas. Bueno, esto Wallis, en el Caso concreto del hexágono, es muy fácil de demostrar; cualquier chaval que sepa un poquito de trigonometría te calcula rápidamente que se observa que claramente la sombra de una cara del cubo es más pequeña y cabe dentro de la sombra del cubo colocado así…
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 VillatoroSignificado #2 · Palabras #2matemáticos aficionados cubo rgbtetraedro icosaedro dodecaedroscientific american matemática recreativamartin garner sólidos regulares poliedrospropiedad rupert poliedrosmatemáticos aficionados conjetura rupertcontraejemplo propiedad ruperto español…la sombra de una cara del cubo es más pequeña y cabe dentro de la sombra del cubo colocado así con los dos contravértices alineados. Claro, la cuestión es: ¿y esto ocurre con otros objetos? Pues sorprendentemente, eso ya es una cosa a posteriori, cuando Empezaron a desarrollarse los ordenadores y se puso de moda la matemática recreativa en revistas como Scientific American, etc.; el famoso Martin Garner, pues muchos matemáticos aficionados, pues se les ocurrió ver si con otros sólidos regulares, otros poliedros, también ocurría. Y se supone que sí, que ocurre con el tetraedro, 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 #1 · Palabras #1propiedad roper en poliedrosjakob steininger programa informáticosergei jurkevich orientaciones preferencialesespacio de orientaciones poliedrorombicosido decaedro contraejemplo ropermatemáticos exigen demostración rigurosapropiedad de rupert poliedrosalgoritmo para atacar el problema rupertpoliedro hipótesis rupertartículo demostración matemática steininger jurkevichconjetura poliedros prueba rupertconjetura de rupert no percedronjuego de palabras norpedron inglésno rupert pedro poliedroconjetura de rupert pedroadaptación nombre español rupert pedrosólido con cara de 15 ladosforma esférica triangulitosanécdota mauricio lesto subsidiofirma falsificada curva derechaburocracia para subsidio desconocidopoliedro cara inferior irrelevanteartículo poliedro firma radiadafalsificar poliedro directamente inventadodemostración matemática poliedro roperespacio de orientaciones algoritmopoliedro ejemplo 2021 sin demostración…y Sergei Jurkevich, que se conocieron de estudiantes en la Olimpiada de Matemáticas y que han seguido colaborando en varios problemas así de matemática recreativa, uno de ellos este. Ellos desarrollaron en 2021 un programa de ordenador para comprobar. Si un poliedro, visto desde todas las posibles caras, eso requiere definir lo que llaman una especie de orientaciones preferenciales; es decir, dado un poliedro se construye una especie de espacio de orientaciones en las que tú garantizas de que mirando en esta orientación pequeñas variaciones en esta orientación hacen que el poliedro siga manteniendo esa propiedad, la propiedad de Roper. Entonces logran para definir dado un poliedro un espacio, digamos otro poliedro de orientaciones que son hechos de triángulos y chequean en cada uno de esos triángulos si se cumple o no se cumple la propiedad de Roper y encontraron. en 2021 un primer candidato a demostrar que era un poliedro que no cumplía con la condición de Roper, que era el rombicosido decaedro, que tiene 62 triángulos, tiene triángulos cuadrados y pentágonos, regulares. pero los matemáticos somos como somos y no nos gusta que se nos diga hemos encontrado un contraejemplo 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, como no, nope, ¿no? Como dicen a veces en eso, entonces es el no percedron, porque no cumple la cosa Es por Rupert, cambiar Rupert por Noper Exacto, Rupert por Noper, pero el Noper, como empieza por N-O-P-E es Noper, ¿no? Y es divertido Yo creo que en español le tendremos que llamar No Rupert Pedro No Rupert Pedro, bueno, sí, en español sería más natural llamarlo No Rupert Pedro por el tema de que en español asociamos el apellido pero bueno, es un sólido que tiene como una cara de 15 caras, perdón, tiene la cara superior de 15 lados, después tiene como triangulitos que hacen una forma así como esférica y después tiene la cara de abajo que yo no sé por qué razón en el artículo nos dicen cuántas caras Mira que te dije que no necesitaras describirlo Bueno, hay que intentar describirlo, ¿vale? O sea, es un poliedro con 90 vértices, 240 vistas, 152 caras. No se me acordaba a mi amigo Mauricio Lesto, en que una vez estábamos haciendo una burocracia para un subsidio, no voy a decir de dónde, para que no tengamos que devolver el dinero y me dijo: falsifica mi firma, digo, bueno, dale; estábamos acostumbrados a hacer eso. Me dice: bueno, te digo cómo es, hace una curva más o menos abierta para la derecha. Digo, vos me estás jodiendo. Es muy raro. O sea, él es un chico normal. Es muy raro esto que hizo. Digo, yo pensé que era un chiste. Pero uno me decía: bueno, ahora pegarle una vuelta para abajo. Pero medio abrupta. Nunca había oído eso. Radiar una firma. Es que es buenísimo. Sí, sí, sí. Lo habitual es falsificarla directamente; te la inventas y ya está. Ay, ay, ay. Bueno, en cualquier caso. Es un poliedro, ¿vale? Y la cara superior tiene 15 lados y la cara inferior, que en los dibujitos no se ve, pero que en el artículo tampoco pone cuántas caras tiene. Pero bueno, parece como que es irrelevante realmente para los autores del artículo; es irrelevante realmente la figura. Lo relevante es la demostración matemática; se basa en combinar ese espacio de orientaciones que ellos han definido previamente con un razonamiento matemático riguroso. Entonces demuestran que bajo ciertas condiciones en el poliedro, si el algoritmo dice que no cumple con la propiedad de Roper, es que es verdad que no la cumple. Algo que no pueden demostrar para el otro ejemplo que tenían en 2021, que es parecido pero es diferente; y con ese todavía no han logrado afinar una demostración que garantice que ahí el algoritmo funcione. Entonces, bueno, todo esto por supuesto se acaba de publicar; los detalles de la demostración no parecen complicados de entender, pero yo no puedo asegurar que esté correcta, ¿vale? Habrá que esperar a que se publique en alguna revista y verificar que realmente es correcta, pero tiene buena pinta, ¿vale? Tiene buena pinta y está acompañada con un software que hay que ver también; hay que validarlo. Validar software en matemáticas suele…
Francis Villatoro explica el problema abierto que surge tras la demostración de la existencia de contraejemplos a la conjetura de Rupert, relacionados con poliedros intermedios entre un cubo y una esfera.
Habla: Francis VillatoroSignificado #8 · Palabras #5contraejemplo cubo esferadeformaciones objeto poliedrotamaño región espacio poliedrosartículo cuanta magazine poliedro rupertdivulgación ciencia fondos privados cuantamagazineinvestigadores historia artículo cuanta magazinecubo ejemplo bonitopoliedro cabe dentro sí mismoencaje práctico perfectouniverso hecho para copiar…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 reivindicando resultados muy interesantes y además merece la pena leer el artículo de Quanta Magazine sobre este nuevo objeto geométrico, porque 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.…
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 #12lean 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 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 #14demostració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…