Búsqueda · 35 momentos en 18 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetmillones de casos teorema colorescódigo terrible teorema coloresLeanJuan Carlos GilPhotoshopRGBFrancis VillatoroWilesYimura TaniyamaRibetÚltimo teorema de FermatHalesAnnals of MathematicsKepler
Código terrible teorema colores
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro comenta sobre una demostración manual del teorema de los cuatro colores, destacando su extensión considerable y la complejidad del código utilizado.
…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 uno y se estudiaban por ordenador, con una serie de propiedades que tenían que cumplir, entonces cada caso había que estudiarlo y siempre estaba con la duda de si se ha dejado algún caso. Acababa obteniéndose una prueba con ese tipo de verificadores automáticos y ahora está de moda. Entonces, el futuro dentro de 10, 15 años es que hay una asignatura en la carrera de matemáticas para aprender a usar estas herramientas y que todo se haga de esta…
Significado #1 · Palabras #1
Francis Villatoro continúa explicando un problema matemático relacionado con una apuesta, haciendo referencia a cómo se representa un cubo RGB en programas de diseño gráfico como Photoshop.
Habla: Francis VillatoroSignificado #11cubo colores rgb photoshopvértice opuesto cubo rgbprograma diseño gráfico photoshop…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 alineas con el vértice opuesto. ¿Y cuál es la imagen que tienes? Pues lo que tienes es que el cubo son tres rombos. ¿Y qué forman esos tres rombos? Un hexágono, entonces tú ves un hexágono de colores con todos los colores primarios colocados en los, o sea, tienes los colores primarios y sus complementarios, ¿no? Y tienes…
Francis Villatoro menciona el trabajo de Hales sobre la conjuntura de Kepler, destacando que fue publicado en Annals of Mathematics y consistió en gigabytes de código.
Habla: Francis VillatoroPalabras #18conjuntura de kepler trabajo halesannals of mathematics publicación halesgigabytes código conjuntura kepler…una posición, bueno, no importa, pero resolviste tu problema. O algunas personas pueden decir, sí, pero ¿cuánto de eso es entender? ¿Y qué es física si no entender la naturaleza? Tú has comentado el caso de la demostración de la conjuntura de Kepler, ¿no? El trabajo famoso de Hales desde el 98. Ese acabó, fue el tema que tú has comentado, ¿no? Acabó publicándose en Anas Mathematics. El problema que tenía es que eran gigabytes de código. O sea, que no eran, no estamos hablando de un código de cien líneas o de mil líneas. Era un código con un tamaño tremendo, súper matematizado y súper no sé qué, donde se podía colar un error en cualquier lugar. Eso generaba una cierta tensión, una cierta duda. Pero la belleza de la matemática es comprender. entonces, si tú tienes un código, si una máquina comprende por ti, has perdido el gran elemento de belleza que tienen las matemáticas es decir, ya es una matemática fea, porque está entendiendo a alguien por ti…
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 GilPalabras #7lean 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 comenta sobre una demostración manual del teorema de los cuatro colores, destacando su extensión considerable y la complejidad del código utilizado.
Habla: Francis VillatoroSignificado #1 · Palabras #1millones de casos teorema colorescódigo terrible teorema colores…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 uno y se estudiaban por ordenador, con una serie de propiedades que tenían que cumplir, entonces cada caso había que estudiarlo y siempre estaba con la duda de si se ha dejado algún caso. Acababa obteniéndose una prueba con ese tipo de verificadores automáticos y ahora está de moda. Entonces, el futuro dentro de 10, 15 años es que hay una asignatura en la carrera de matemáticas para aprender a usar estas herramientas y que todo se haga de esta…
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 #16demostració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…