Búsqueda · 24 momentos en 8 episodios
Ignacio CrespoBorja TosarJosé EdelsteinIsabel CorderoFrancis VillatoroHéctor Socasdemostración conjetura cornes leanmatemático nielsen revisa astra openailean programa ordenador rigor matemático30000 líneas de código leanerrores en antecedentes astra openaidemostraciones matemáticas nielsenconocimiento matemático previo de máquinasNielsenLeanconjetura de CornesFrancis VillatoroAstraOpenAIMucho FricuoICM 2026Terence TaoDINFiladelfia
Demostraciones Matemáticas Nielsen
Ep565: Introgresión; Eclipse; Inestabilidad Kelvin-Helmholtz; Piezoquiralidad
6 de agosto de 20265 momentos
Con
0:000:301:001:302:002:303:003:34
Francis Villatoro explica que un matemático llamado Nielsen revisó una demostración generada por la inteligencia artificial Astra de OpenAI, específicamente la demostración de la conjetura de Cornes, que consta de aproximadamente 30.000 líneas de código en Lean.
…estas demostraciones es que piden a gritos que humanos formen un grupito de humanos para estudiar en detalle cada una de esas demostraciones en Lean y ver si son correctas o no. ¿Y por qué digo esto? Y digo esto porque es importante porque ayer se publicó. Ya llevaba varios días hablándose del tema. Ya se publicó el documento: un matemático, Nielsen, ha cogido una de esas demostraciones, la demostración de la conjetura de Cornes, y se ha leído las, son, no recuerdo, una barbaridad, 30.000 líneas en Lean, o algo así, una barbaridad de líneas en Lean. Lean es, imagínate un programa de ordenador de 30.000 líneas y te lo tienes que leer con extremo cuidado porque cualquier pequeña desviación de lo que es el rigor matemático invalida automáticamente la prueba. No, pero es que Lean lo ha verificado, no, perdona, Lean lo ha verificado si en un código en Lean. Es muy importante, digamos, darle los antecedentes de la demostración. En una demostración matemática entre humanos, yo asumo que el que lee la demostración ya conoce los antecedentes. Yo me ahorro todo eso, porque ya los conoce. Pero en una demostración hecha por la máquina desde cero, se incluyen esos antecedentes y en esos antecedentes, ese conocimiento matemático conocido, puede haber errores. Y este matemático, Nielsen, ha descubierto. en una de las demostraciones, la de la conjuntura de Cornes que hay dos errores. Corners requiere dos condiciones, la propiedad T, que el grupo sea ICC, y resulta que en el código Lean, donde se definen esas propiedades, se cometen errores. Llámale…
Significado #2 · Palabras #1
Francis Villatoro describe cómo OpenAI ha contratado a matemáticos para buscar y demostrar conjeturas famosas utilizando una inteligencia artificial llamada Astra.
Habla: Francis VillatoroPalabras #12openai contrata matemáticos astrademostración formalizada lenguaje leandocumento sin intervención humana…con José. Bueno, la gran noticia en matemáticas de las últimas semanas es el último hito de OpenAI, de la compañía responsable de CharGPT, con una inteligencia artificial de laboratorio que se llama Astra y que todo el mundo cree que va a ser CharGPT 6.0. OpenAI ha hecho algo realmente sorprendente: ha contratado muchos matemáticos y ha puesto un grupo de matemáticos a buscar conjeturas famosas y a demostrarlas con esta inteligencia artificial. Esta tecnología artificial no ha ofrecido una demostración legible para un matemático, sino que ha ofrecido una demostración formalizada en un lenguaje de demostración automática que se llama LEAN. LEAN esas demostraciones en LEAN han sido validadas y verificadas en LEAN, con lo que son demostraciones en principio correctas, entre comillas; y OpenAI anunció que lo había logrado y unos días más tarde presentó un documento escrito por este chat GPT 6.0, por Astra, de 249 páginas con una descripción para humanos de las 10 demostraciones. Son dos resultados bastante importantes. El problema es que ese documento no ha sido tocado por manos humanas. Es un documento difícil de leer. Yo lo he intentado. Yo he intentado leer esas 241 páginas y algunas demostraciones son muy técnicas. Son las mejores demostraciones que han hecho una inteligencia artificial hasta el momento. Estamos hablando de demostraciones…
Francis Villatoro explica que un matemático llamado Nielsen revisó una demostración generada por la inteligencia artificial Astra de OpenAI, específicamente la demostración de la conjetura de Cornes, que consta de aproximadamente 30.000 líneas de código en Lean.
Habla: Francis VillatoroSignificado #2 · Palabras #1demostración conjetura cornes leanmatemático nielsen revisa astra openailean programa ordenador rigor matemático30000 líneas de código leanerrores en antecedentes astra openaidemostraciones matemáticas nielsenconocimiento matemático previo de máquinas…estas demostraciones es que piden a gritos que humanos formen un grupito de humanos para estudiar en detalle cada una de esas demostraciones en Lean y ver si son correctas o no. ¿Y por qué digo esto? Y digo esto porque es importante porque ayer se publicó. Ya llevaba varios días hablándose del tema. Ya se publicó el documento: un matemático, Nielsen, ha cogido una de esas demostraciones, la demostración de la conjetura de Cornes, y se ha leído las, son, no recuerdo, una barbaridad, 30.000 líneas en Lean, o algo así, una barbaridad de líneas en Lean. Lean es, imagínate un programa de ordenador de 30.000 líneas y te lo tienes que leer con extremo cuidado porque cualquier pequeña desviación de lo que es el rigor matemático invalida automáticamente la prueba. No, pero es que Lean lo ha verificado, no, perdona, Lean lo ha verificado si en un código en Lean. Es muy importante, digamos, darle los antecedentes de la demostración. En una demostración matemática entre humanos, yo asumo que el que lee la demostración ya conoce los antecedentes. Yo me ahorro todo eso, porque ya los conoce. Pero en una demostración hecha por la máquina desde cero, se incluyen esos antecedentes y en esos antecedentes, ese conocimiento matemático conocido, puede haber errores. Y este matemático, Nielsen, ha descubierto. en una de las demostraciones, la de la conjuntura de Cornes que hay dos errores. Corners requiere dos condiciones, la propiedad T, que el grupo sea ICC, y resulta que en el código Lean, donde se definen esas propiedades, se cometen errores. Llámale…
Francis Villatoro continúa una analogía sobre las demostraciones matemáticas, explicando la importancia de difundir y asimilar una demostración dentro de la comunidad matemática.
Habla: Francis VillatoroSignificado #17 · Palabras #3demostraciones matemáticas como hijascuidado de demostraciones por matemáticosterence tao en el icm 2026mucho fricuo y las demostracionesdifusión de demostraciones matemáticasasimilación de demostración comunidad matemáticaincorporación demostración conocimiento matemáticoimportancia asimilar demostración francis villatorodemostraciones complejas expertos matemáticoslógica clara en demostraciones sinuosasatajos imposibles en demostracionesguías matemáticas carecen de conciencia…y el futuro de las matemáticas en el ICM 2026, también en Filadelfia. Y Terence Tao ha dicho: lo voy a tratar con mis palabras porque no tengo las palabras exactas de Terence en la cabeza, pero básicamente ha dicho que una demostración es como una hija. A una hija no tienes que parirla, no basta con parirla y abandonarla. A una hija la tienes que cuidar, la tienes que cuidar, la tienes que educar, la tienes que transformar en un adulto, un adulto productivo, feliz y que tenga una buena vida. Y los matemáticos tratamos a nuestras demostraciones como si fueran nuestros hijos y las cuidamos. Entonces, una demostración, cuando tú haces una gran demostración, un matemático hace una gran demostración, no hace la demostración y dice: señores, como dice Mucho Fricuo, ya he cumplido, aquí no hay que hacer nada más, ya está, ahí tenéis la demostración, buscaros la vida. No, hombre, sino tienes que ir a conferencias científicas y contar la demostración, a dar seminarios, a dar cursos, a vender tu demostración para que la comunidad matemática pueda asimilar esa demostración, pueda incorporar esa demostración. Esa parte de asimilación y de incorporación de la demostración al común conocimiento matemático de esa área es mucho más importante que la propia demostración. Y eso es lo que los matemáticos han estado haciendo. De las grandes demostraciones, los grandes matemáticos se tiran años contando cómo funciona la demostración, los detalles, porque la demostración es un camino muchas veces sin trabas. es un camino perfectamente, muy sinuoso, dando mucha vuelta, pero perfectamente llega al final y todo el mundo se puede decir, ¿y por qué aquí no tomaste un atajo? Ah, no, porque no funciona, porque pasa tal y cual y cual, eso se lo puede contar el que lo ha hecho pero las guías no pueden, porque las guías no saben lo que han hecho, no son conscientes de lo que han hecho han producido un código link, dice, no, bueno, no puedo hacerlo porque no se puede hacer, punto pelota ¿Por qué no? Pues yo creo que cuando jugaba al Go, AlphaGo o AlphaCero, que aprendió sola. Bueno, es que yo he evaluado la partida y el lugar donde hay que poner una pieza es aquí. Aquí tengo que poner una piedra. ¿Y por qué? No, no, porque lo he evaluado y hay que…
Francis Villatoro advierte sobre la proliferación de demostraciones matemáticas generadas artificialmente, describiéndolas como 'indigeribles' y criticando su publicación en formato DIN.
Habla: Francis VillatoroSignificado #11 · Palabras #19demostraciones matemáticas generadas artificialmentepublicación de demostraciones en dindeshumanización de las matemáticas bellezadestrucción al estudiar código informático…Go, AlphaGo o AlphaCero, que aprendió sola. Bueno, es que yo he evaluado la partida y el lugar donde hay que poner una pieza es aquí. Aquí tengo que poner una piedra. ¿Y por qué? No, no, porque lo he evaluado y hay que ponerlo ahí. No tienes un razonamiento. Y eso va a ocurrir ahora con muchas demostraciones. Está habiendo una explosión terrible de demostraciones, porque es artificial, terrible; es una cosa absolutamente indigerible y mucha gente está empezando a publicar demostraciones en DIN. Y eso es deshumanizar completamente las matemáticas, la belleza de las matemáticas, la belleza de la comprensión, del razonamiento, el disfrute de aprender cosas. Cuando estás leyendo una demostración se destruye cuando lo que estás estudiando es un código informático, sea verificable o no; y permíteme, estoy hablando de una barbaridad, pero permíteme un punto final y ya acabo. Se encontró hay bugs, hay errores en el núcleo de Lean, como en cualquier programa informático. El núcleo de Lean no es muy grande, no son muchas líneas de código, son unas miles de líneas de código. Se ha encontrado un error y resulta que una IA aprovechó…
Francis Villatoro continúa hablando sobre la dificultad de comprender demostraciones matemáticas complejas, comparándolas con poesía y explicando que se puede apreciar su belleza incluso sin entenderlas completamente.
Habla: Francis VillatoroSignificado #4belleza de la poesía matemáticademostraciones matemáticas complejasdocumento de 241 páginas sin demostraciones…lo puedo creer, no me lo creo”. Y no me lo creo yo, que soy un ignorante, porque yo no soy un experto; son súper técnicas, son conceptos técnicos terribles, o sea, estas cosas que trabajan 20 personas en el mundo y que fuera ese circulito nadie más entiende. Pero bueno, hay un cuerpo genérico que te permite, tú vas leyendo con el lenguaje matemático y es como la poesía; te va gustando, te va agradando y vas diciendo que maravilla, que bien fluye esto, que bien razonado está esto, aunque no te enteres. Hay un disfrute de esa poesía matemática y en este documento de 241 páginas esas 10 demostraciones no las hay, entonces es muy aburrido, cuesta muchísimo. Vamos a ir con más preguntas, entonces, y quedaba José que tenías que hablar de la cena y escuchar la legislativa. ¿Que no sé si quieres contestarla o prefieres pasar? José, puedo decir algo brevemente respecto a lo anterior; lo ideal sería cuando te tira la…