Búsqueda · 28 momentos en 15 episodios
Ignacio CrespoBorja TosarJosé EdelsteinIsabel CorderoFrancis VillatoroHéctor Socasia explota fallo en núcleo leanhipótesis de riemann demostrada por iademostración falsa con 3000 líneas linnexperto descubre error en leanLeanHipótesis de RiemannFrancis VillatoroCollardVATNúcleoOpenAICharGPTAstraJoséCharles GPTGPTGeminiClodasNielsenconjetura de Cornes
Ia explota fallo en núcleo Lean
Ep565: Introgresión; Eclipse; Inestabilidad Kelvin-Helmholtz; Piezoquiralidad
6 de agosto de 20266 momentos
Con
0:000:301:001:302:002:303:003:34
Francis Villatoro describe cómo una inteligencia artificial (IA) explotó un fallo en el núcleo del sistema Lean para demostrar falsamente que falso es verdadero, incluso llegando a simular una prueba de la hipótesis de Riemann.
…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ó ese error para demostrar que falso es verdadero. La IA es capaz de demostrar cualquier cosa; tú le dices: la hipótesis de Riemann, te la he demostrado, aquí está demostrado, 3000 líneas de Linn, ahí está la demostración pasa las líneas. La primera línea pone la definición de la hipótesis de Riemann, y la última línea, correcto, pero estás aprovechando un error que te permite eso lo descubrió el experto; se descubrió el experto y el experto pidió a una IA que construyera una demostración de la Conjetura de Collage, una lectura muy famosa, muy conocida; vas haciendo unas operaciones: dividir por dos, multiplicar por tres y hace que los números crezcan y después de crezcan y llegan, acaban en uno. Entonces, por existencia, una demostración por…
Significado #1 · Palabras #1
Francis Villatoro comenta sobre una segunda parte de una pregunta relacionada con las demostraciones de Lean sobre los 10 problemas de OpenAI, expresando desconocimiento sobre su significado. A continuación, introduce la noticia más relevante en matemáticas: el último hito de OpenAI y su inteligencia artificial Astra.
Habla: Francis VillatoroSignificado #6demostraciones lean problemas openaiinteligencia artificial astra openaihito openai compañía chargpt…a la Francis, luego puso a Isa, y no sé por qué, a ellos en particular, pero les pregunta por su opinión honesta sobre las charlas de divulgación de Maldacena Hombre, ya he puesto historia, pero le pregunto a José, que es aquí quien tiene más relación Y luego hay una segunda parte de la pregunta que es diferente, que es si logra encontrar traducción de las demostraciones de Lean sobre los 10 problemas OpenAI; no sé muy bien a qué se refiere, no sé si alguno se sabe. Comento yo eso segundo y después pasamos a Maldasena 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…
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 #16 · Palabras #20demostración conjetura cornes leanmatemático nielsen revisa astra openailean programa ordenador rigor matemático30000 líneas de código 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…
Francis Villatoro comenta sobre la creciente popularidad de herramientas como Charles GPT para generar código Lean y explica que algunas personas prefieren esto en lugar de recibir explicaciones detalladas de demostraciones matemáticas.
Habla: Francis VillatoroSignificado #11charles gpt genera código leanpreferencia por código lean automáticofrancis villatoro y charles gpt…y se da vuelta; está volviendo famoso. Y entonces probablemente eso incentive a gente joven que lo haga también. Pero se requiere un enorme conocimiento porque son demostraciones muy técnicas. Este es el gran problema que tenemos ahora mismo, como Esto se popularice y se está empezando a popularizar, ya está empezando a haber gente que está diciendo: No, no, no, no, yo no quiero que Charles G.P.T. me explique la demostración, porque yo no tengo ni zorrea, no lo voy a entender, quiero que me genere el código Lean automáticamente, porque las Demostraciones a principios de este año se generaban en lenguaje humano, hecho por la máquina, y entonces tú usabas Aristóteles, un conversor que te convertía esa demostración al lenguaje Lean, y después la verificabas en Lean. Se ha verificado en Lean y…
Francis Villatoro reflexiona sobre la necesidad de estudiar el lenguaje de programación Lean para revisar las demostraciones generadas por inteligencia artificial, expresando su propia dificultad para comprenderlo.
Habla: Francis VillatoroSignificado #4lenguaje programación lean francis villatorodemostraciones inteligencia artificial leandificultad para comprender leangpt analiza código leangemini y clodas evalúan demostracionesriesgos en evaluaciones gpthipótesis de la unidad disco unitario…miles de demostraciones en Lean. Y la única manera de gestionar eso para la comunidad matemática mundial va a ser que esos matemáticos entiendan Lean, también como entienden sumar, restar o multiplicar. Y eso estamos en un momento en la transición terrible. Entonces, esas 10 demostraciones, ¿sabes que una de ellas es incorrecta? ¿Las otras 9 son correctas? No lo sabemos. No lo sabemos. Tenemos que ponernos a estudiar Lean. Yo no sé Lean. Yo no puedo ponerme a leer un código de 20.000 líneas en Lean si me aburro leyendo un código en Lean de 100 líneas. O sea, alguien va a tener que hacerlo. Se lo ponemos a echar GPT y que lo lea y no se va Claro, eso tiene un enorme tipo de vicio porque este tipo de demostraciones se pasaron a otros, a Gemini, a Clodas, no sé qué, y dijeron que eran correctas O sea, las intereses de vida dijeron, estas demostraciones son correctas Ahora sabemos que una de ellas no lo es y hay dudas de alguna de las otras O sea, estas demostraciones hay que cogerlas con mucho cuidado Pero es que la ocasión anterior, con la famosa demostración de la hipótesis de la unidad, del disco unitario o algo así, OpenAI, antes de sacar la publicación del documento, contrató a una serie de matemáticos que eran todos muy famosos, medallas Phil, gente muy famosa, para que escribieran documentos. Los matemáticos entendieron ahí trabajando con la máquina y con la gente que…
Francis Villatoro describe cómo una inteligencia artificial (IA) explotó un fallo en el núcleo del sistema Lean para demostrar falsamente que falso es verdadero, incluso llegando a simular una prueba de la hipótesis de Riemann.
Habla: Francis VillatoroSignificado #1 · Palabras #1ia explota fallo en núcleo leanhipótesis de riemann demostrada por iademostración falsa con 3000 líneas linnexperto descubre error en lean…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ó ese error para demostrar que falso es verdadero. La IA es capaz de demostrar cualquier cosa; tú le dices: la hipótesis de Riemann, te la he demostrado, aquí está demostrado, 3000 líneas de Linn, ahí está la demostración pasa las líneas. La primera línea pone la definición de la hipótesis de Riemann, y la última línea, correcto, pero estás aprovechando un error que te permite eso lo descubrió el experto; se descubrió el experto y el experto pidió a una IA que construyera una demostración de la Conjetura de Collage, una lectura muy famosa, muy conocida; vas haciendo unas operaciones: dividir por dos, multiplicar por tres y hace que los números crezcan y después de crezcan y llegan, acaban en uno. Entonces, por existencia, una demostración por…
Tras describir un error intencionado en una demostración matemática, Francis Villatoro sugiere la posibilidad de utilizar inteligencias artificiales para identificar fallos en sistemas como Lean.
Habla: Héctor SocasSignificado #2 · Palabras #3ia detectando fallos en leandemostración falsa con iafrancis villatoro y sistemas leanerrores en código núcleo leanvat número 7000 en leanguías usan inteligencia artificial…acaban en uno. Entonces, por existencia, una demostración por existencia, pues es una demostración que en un cierto momento decía falso, verdadero, y a partir de aquí cualquier cosa es verdadera, por ejemplo, la fuente de Collard. Claro, eso fue intencionado. Eso se arregló en dos o tres días, dos días y medio, y ya ese error no está, pero puede haber errores en los demostradores automáticos. Eso me hace pensar que quizás se puede aprovechar; le puedes pedir a una IA que te demuestre algo que sabes que es falso y si te lo demuestra, te puede servir para encontrar errores en Lean, por ejemplo, en el código que sea que estás usando. Sí, de hecho las guías están usando para detectar bugs en código y se está aplicando también ese tipo de cosas, ¿no? El núcleo de Lean se suponía que estaba certificado matemáticamente de que era correcto y ha tenido un error absolutamente terrible; de hecho los detalles del error se publicaron y no te lo crees que haya podido ocurrir, pero puede ocurrir, ¿vale? Y era el error, el VAT número 7000 y pico, o sea, hay errores en este tipo de código. Por lo tanto, el matemático no puede confiar sobre eso. El matemático tiene que comprender, aprender, asimilar, meter dentro de sí. Pero es la base de toda la ciencia; al final tiene que ser verificable, reproducible, no basta con un resultado, tiene que ser revisado, verificado, comprobado por la comunidad para…