Búsqueda · 28 momentos en 14 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetlean validación demostraciones matemáticasdemostrador automático artículo matemáticorevisores artículo mundo detalleLeanFrancis VillatoroRamanujanAnnals of MathematicsPrincetonRobert MacPhersonCuanta MagazineJuan Carlos GilMartin GarnerScientific American
Revistas validación máquina matemática
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro describe una nueva tendencia en matemáticas donde se espera que todos los matemáticos aprendan a usar herramientas como Lean para validar sus demostraciones.
…no entramos en los detalles, pero se detectó, gracias a pasar esa demostración a Lean, se detectó un error que rápidamente dijo: esto lo resuelvo yo con la punta al nabo, y lo arregló en un momentillo y lo arregló, ¿vale? Y ya está certificado por Lean. Y ahora está habiendo una corriente en matemáticas de decir: todo matemático en su carrera tiene que aprender a utilizar este tipo de herramientas porque dentro de una serie de años, puede que sean 10 años, a todos los matemáticos se les va a exigir que todas las demostraciones estén en Lean y estén validadas por un ordenador. Un demostrador automático va a tener que garantizar que tu artículo es correcto, matemáticamente correcto, no porque tú lo digas o porque lo digan los dos o tres revisores que han visto tu artículo, que puede que sean las únicas personas en el mundo que acaben leyéndose en detalle, no, no, porque una máquina diga que tu resultado es correcto. Y esa es una tendencia que ahora está. Liderando Terence Tao, que está colaborando con Google DeepMind, que tiene unos programas de generación automática de pruebas y a él le están pagando, le están financiando muy bien porque, por cierto, el señor Trump le quitó su proyecto de investigación y al…
Significado #2 · Palabras #1
Francis Villatoro explica cómo matemáticos aficionados comenzaron a investigar si el fenómeno observado con el cubo RGB también ocurría con otros sólidos regulares y poliedros, tras el desarrollo de ordenadores y la popularización de la matemática recreativa en revistas como Scientific American.
Habla: Francis VillatoroPalabras #19matemáticos aficionados cubo rgbtetraedro icosaedro dodecaedroscientific american matemática recreativamartin garner sólidos regulares poliedros…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…
Francis Villatoro comenta sobre la reciente publicación de una demostración matemática relacionada con un nuevo poliedro que desafía la conjetura de Rupert.
Habla: Francis VillatoroSignificado #4 · Palabras #2software validación matemáticarevisores publicación revista…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 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…
Francis Villatoro y Juan Carlos Gil comentan sobre la publicación en Cuanta Magazine de un artículo sobre un nuevo poliedro que desafía la conjetura de Rupert. Se destaca que el artículo narra la historia de los investigadores y es entretenido.
Habla: Francis VillatoroSignificado #18artículo cuanta magazine poliedro rupertdivulgación ciencia fondos privados cuantamagazineinvestigadores historia artículo cuanta magazine…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…
Gastón Giribet continúa relatando una anécdota personal sobre su época como postdoc en Princeton, y menciona un cambio abrupto en la decisión editorial de Annals of Mathematics respecto a la publicación de demostraciones asistidas por computadora.
Habla: Gastón GiribetSignificado #13annals of mathematics demostraciones computacionalescambio editorial annals of mathematicsmacpherson desacuerdo demostraciones computacionales…Manperson sigue vivo, pero es emérito ahora, pero en ese momento estaba en la escuela de matemática. Sí, todos los que mencioné siguen vivos, sacando Nash, son todos eméritos ahí. Entonces la cuestión es, en ese momento había un cambio abrupto en la decisión. Editorial de Annals of Mathematics, acaso la más importante de la revista de Matemática, también editada por Princeton. ¿Qué era empezar a aceptar demostraciones asistidas por computadora para ser publicadas? No porque no se aceptaran como demostraciones, sino como la revista dice: no, con 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.…
Francis Villatoro expresa su duda sobre la confianza que se puede depositar en demostraciones matemáticas realizadas por máquinas, a pesar de su aparente corrección.
Habla: Francis VillatoroSignificado #3 · Palabras #10belleza matemática comprensión personalcódigo máquinas matemáticas feademostraciones complejas esfuerzo limitadodemostraciones matemáticas máquinasconfianza demostración máquina correcciónrevolución matemáticas inteligencia artificial…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 o sea, tú dices, claro, hay muchas demostraciones que no las he estudiado, que no las entiendo pero tengo la convicción de que si yo dedicara tiempo suficiente, acabaría entendiéndolas pero cuando una demostración me requiere estudiar 100 millones de páginas pues yo sé que por mucho que yo me esfuerce yo no lo voy a ser capaz de entender. Entonces yo puedo confiar en una demostración 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…
Francis Villatoro describe una nueva tendencia en matemáticas donde se espera que todos los matemáticos aprendan a usar herramientas como Lean para validar sus demostraciones.
Habla: Francis VillatoroSignificado #2 · Palabras #1lean validación demostraciones matemáticasdemostrador automático artículo matemáticorevisores artículo mundo detalle…no entramos en los detalles, pero se detectó, gracias a pasar esa demostración a Lean, se detectó un error que rápidamente dijo: esto lo resuelvo yo con la punta al nabo, y lo arregló en un momentillo y lo arregló, ¿vale? Y ya está certificado por Lean. Y ahora está habiendo una corriente en matemáticas de decir: todo matemático en su carrera tiene que aprender a utilizar este tipo de herramientas porque dentro de una serie de años, puede que sean 10 años, a todos los matemáticos se les va a exigir que todas las demostraciones estén en Lean y estén validadas por un ordenador. Un demostrador automático va a tener que garantizar que tu artículo es correcto, matemáticamente correcto, no porque tú lo digas o porque lo digan los dos o tres revisores que han visto tu artículo, que puede que sean las únicas personas en el mundo que acaben leyéndose en detalle, no, no, porque una máquina diga que tu resultado es correcto. Y esa es una tendencia que ahora está. Liderando Terence Tao, que está colaborando con Google DeepMind, que tiene unos programas de generación automática de pruebas y a él le están pagando, le están financiando muy bien porque, por cierto, el señor Trump le quitó su proyecto de investigación y al…
Francis Villatoro reflexiona sobre el futuro de las matemáticas y cómo los verificadores automáticos están transformando la disciplina.
Habla: Francis VillatoroSignificado #1 · Palabras #3verificadores automáticos matemáticasasignatura herramientas matemáticas carrerarevistas validación máquina matemática…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 manera. O sea, y que las revistas digan: esto es verdad solo si la máquina lo dice. Y para que la máquina lo diga, tú tienes que haber pasado todo lo que tú has dicho, todo lo que tú has escrito en papel, a la máquina. Pero déjame que lo vuelva a decir, que no sé si yo mismo lo he entendido bien, o sea, no. Es que Tao esté haciendo inteligencia artificial generativa, inventándose cosas, no; la herramienta le ayuda a explorar el código, ¿cómo se llama? Lint Lint, L-A-N, es el demostrador más famoso ahora mismo, y es un metademostrador. Te permite trabajar con un…
Francis Villatoro explica cómo las pruebas matemáticas generadas con Lean son equivalentes a las tradicionales, aunque actualmente ocupan más espacio en formato digital.
Habla: Francis VillatoroSignificado #15pruebas matemáticas lean equivalentes tradicionalesfactor de 10 pruebas lean vs papeldemostraciones lean mejorando tamaño…ayuda a explorar el código, ¿cómo se llama? Lint Lint, L-A-N, es el demostrador más famoso ahora mismo, y es un metademostrador. Te permite trabajar con un lenguaje bastante próximo al humano, pero es un lenguaje formal, ¿verdad? Si no me equivoco, Francis. Con lo cual, una vez que tienes la prueba, es equivalente a una prueba matemática tradicional con todos los símbolos matemáticos. Ahora mismo el factor es del orden de un factor de 10. Es decir, si en hojas de papel, a mano, a ti 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…
Francis Villatoro describe una actitud anterior entre los matemáticos hacia el uso de Lean, un lenguaje de verificación matemática, comparándola con la actual valoración que se le está dando.
Habla: Francis VillatoroSignificado #8 · Palabras #20matemáticos rechazan leanramanujan frente a leanrevisión artículo dos años…que abarco en mis matemáticas y me parece fascinante lo que está haciendo. O sea, y ya te digo, está generando una tendencia en la que muchos matemáticos están empezando a valorar esto porque hace un año y medio el 99,9% de los matemáticos puede asegurar que Se negaba rotundamente a usar Lean. Eso es de inútiles, solo los inútiles requieren formalizar y que la máquina les diga que lo han hecho bien. No, no, no: aquí el matemático de pro tiene que mirárselo página a página y si para revisar un artículo hay que dedicarse dos años de revisión, pues le dedicamos dos años de revisión. Y ahora me imaginaba a Ramanujan con el link este delante; os imagináis. Ramanujan era otra cosa; es que Ramanujan no sabía demostrar, no era capaz de demostrar, no valoraba demostrar. Era un matemático que se dedicaba a jugar con desarrollos convergentes y divergentes y a operar con ellos, y era muy bueno, muy rápido haciendo…