Búsqueda · 29 momentos en 13 episodios
Daniel MarínLuisa AchaerandioJuan Carlos GilFrancis VillatoroHéctor SocasGastón Giribetverificación código python herramientademostración formalizada precisiónejecución código no deseadachatgpt o gemini para demostracionesdemostraciones en lenguaje naturalformalización de demostraciones leanLeanChatGPTFrancis VillatoroGeminiInteligencia ArtificialMatemáticoAristótelesGrothendieckHéctor SocasINSSNat ZosanathanChatGPT 5.2 ProArchiveResolución del programa 728
Demostración formalizada precisión
Ep542: Emergencia en la ISS; Artemisa; IA en Matemáticas; Burbujas; Distracción
22 de enero de 20268 momentos
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro explica que al igual que se verifica el funcionamiento de un código Python generado por una herramienta, es crucial asegurar que una demostración formalizada sea precisa.
…te requiere un cierto entrenamiento incluso con chat GPT, porque chat GPT comete errores y tú tienes que tener una garantía absoluta de que lo que te ha dado es como un código Python: le pides que te generen un código Python o Python y te genera un código. Pero tú tienes que saber si el código corre, claro; es muy fácil: lo compilas, lo ejecutas y si corre, corre. Pero, ¿y si ejecuta pero no hace lo que tú quieres? Es que con la demostración es muy importante que lo que tú hayas formalizado sea exactamente lo que tiene que ser. entonces eso, lo que se está haciendo ahora mismo es: trabajas con el ChatGPT o el Gemini o lo que sea en lenguaje, digamos, humano, normal, sin ningún tipo de formalización y una vez que tienes una demostración… Sí, eso lo entiendo, pero a lo que voy es que, o sea, yo a ChatGPT le pido una demostración de un determinado… Tú haces copy-paste, o sea tú coges, te vas a la página web del Erdisk Problem, problema 333. Lo miras y pones el enunciado, copy paste del enunciado, ChatGPT, demuéstrame este resultado. Vale, y ahora si quiero, si ahora quiero meter eso en Lean, para que me…
Significado #1 · Palabras #5
Francis Villatoro explica el siguiente paso tras obtener una posible solución de ChatGPT: trasladarla a Lean para su validación.
Habla: Francis VillatoroPalabras #8validación demostraciones leansistema formalización demostraciones leanverificación demostración con leanenunciado demostración en lean…cosa. Pero claro, el que lo había hecho, imaginaos que eres un informático, no tenía ni zorra idea, no entendía la demostración, no entendía el problema y no sabía si XAGPT había dado una solución buena. Entonces lo que se decide con finales de noviembre. ¿Es esto? Hay que pasarlo a Lean. Lean es un sistema de formalización de demostraciones que te permite hacer una validación, una verificación de la demostración: si la demostración es correcta o no es correcta. Si tú pides un enunciado de lo que hay que demostrar, Lean, si tienes esta demostración escrita en ese lenguaje, te dice si la demostración demuestra eso o no lo demuestra, si todos los pasos son correctos, si hay algún error, etc. Pero claro, pasar las demostraciones escritas en lenguaje humano, digamos, a la manera usual de los humanos de ChagPT, pasarlas a Lean es algo que ChagPT es capaz de hacer pero con muchos errores. Entonces se desarrolló una herramienta que se llama Aristotle,…
Francis Villatoro describe cómo muchas personas están utilizando ChatGPT para generar demostraciones matemáticas y luego validándolas con Lean.
Habla: Francis VillatoroSignificado #13chatgpt genera demostraciones matemáticasvalidación lean de demostraciones chatgptdemostraciones incorrectas inssinteligencia artificial y demostraciones correctas…se la paso a Aristóteles, Aristóteles me da un programa en Lean, el programa en Lean, se lo paso a Lean y si Lean me dice, sí, es correcta, maravilla, lo he logrado. Y si me dice, no, es incorrecta, digo, bueno, mala suerte. Paso al siguiente problema. Eso lo han empezado a hacer mucha gente, como lo han empezado a hacer mucha gente. La mayoría de la gente está obteniendo entre comillas basura, o sea, demostraciones que no son demostración de nada y que el INSS rápidamente te dice que la demostración es incorrecta, pero algunas de ellas pues son demostraciones correctas. Entonces se están empezando a publicar demostraciones que están, digamos, o totalmente hechas por la inteligencia artificial o parcialmente hechas a través de un diálogo. Cuando la persona no es informático, sino que es matemático, a veces dialoga. Dice: “Chat GPT, pero vos me pones esta mierda de demostración. Yo que soy un matemático inútil me doy cuenta de que está mal. ¿Por qué no corriges esto, no sé qué? Esto está mal…
Francis Villatoro aclara que Lean requiere una demostración formalizada y no solo el enunciado de un problema. Para ello, se introduce el enunciado en ChatGPT o herramientas similares.
Habla: Héctor SocasSignificado #10 · Palabras #2demostración formalizada en leanenunciado problema chatgpt…el código Lean, después tienes que pasarlo; entonces, pues, en una mañana te da las demostraciones, las tienes en Lean corriendo por la tarde y por la noche ya sabes si son correctas o no son correctas, Francis. Una pregunta, si yo he entendido un poco el Flujo de trabajo de esto: alguien tiene que poner en Lean el enunciado del problema, ¿no? En Lean no, Lean necesita que le des la demostración formalizada; el enunciado del problema lo pones en GPT, en Chat GPT o el equivalente. Vale, pero no tienes que poner un enunciado del problema formalizado en Lean, o sea, ¿cómo sabe Lean que lo que está demostrando es lo que... Bueno, o sea, la idea que se está ahora usando, porque el Lean lo conoce muy poquita gente y traducir un enunciado o una demostración al Lean es algo que te requiere un cierto entrenamiento incluso con chat GPT, porque chat GPT comete errores y tú tienes que…
Francis Villatoro explica que al igual que se verifica el funcionamiento de un código Python generado por una herramienta, es crucial asegurar que una demostración formalizada sea precisa.
Habla: Francis VillatoroSignificado #1 · Palabras #5verificación código python herramientademostración formalizada precisiónejecución código no deseadachatgpt o gemini para demostracionesdemostraciones en lenguaje naturalformalización de demostraciones lean…te requiere un cierto entrenamiento incluso con chat GPT, porque chat GPT comete errores y tú tienes que tener una garantía absoluta de que lo que te ha dado es como un código Python: le pides que te generen un código Python o Python y te genera un código. Pero tú tienes que saber si el código corre, claro; es muy fácil: lo compilas, lo ejecutas y si corre, corre. Pero, ¿y si ejecuta pero no hace lo que tú quieres? Es que con la demostración es muy importante que lo que tú hayas formalizado sea exactamente lo que tiene que ser. entonces eso, lo que se está haciendo ahora mismo es: trabajas con el ChatGPT o el Gemini o lo que sea en lenguaje, digamos, humano, normal, sin ningún tipo de formalización y una vez que tienes una demostración… Sí, eso lo entiendo, pero a lo que voy es que, o sea, yo a ChatGPT le pido una demostración de un determinado… Tú haces copy-paste, o sea tú coges, te vas a la página web del Erdisk Problem, problema 333. Lo miras y pones el enunciado, copy paste del enunciado, ChatGPT, demuéstrame este resultado. Vale, y ahora si quiero, si ahora quiero meter eso en Lean, para que me…
Francis Villatoro explica cómo ChatGPT transforma demostraciones en lenguaje natural a formato Lean, incluyendo el enunciado y el resultado deseado. Menciona que Aristóteles, otra herramienta, no siempre funciona correctamente y puede cometer errores.
Habla: Francis VillatoroSignificado #8chatgpt transforma demostraciones leanaristóteles comete errores en demostracionesdemostración incluye enunciado y resultadoverificación demostraciones leandemostraciones matemáticas leansoftware verifica demostracioneslemas en demostraciones lean…copy paste del enunciado, ChatGPT, demuéstrame este resultado. Vale, y ahora si quiero, si ahora quiero meter eso en Lean, para que me compruebe esa demostración. Si quieres meter en Lean, necesitas utilizar Aristotel, otro software, que es un software. Que te convierte en una demostración. En lenguaje, el resultado que te da ChatGPT, te lo convierte en Lean Vale, o sea, y en la propia demostración está el enunciado, claro, sí, en la propia demostración está lo que quieres demostrar el denunciado y la resulta; entonces Aristóteles no siempre funciona, muchas veces falla, muchas veces falla CharGPT, otras veces falla Aristóteles que comete errores, pero en general tu. Manera de verificar que lo has hecho bien no es preguntarle a un matemático, porque los matemáticos van a decir: vamos hasta que pierdes el tiempo de demostraciones; es como la tienes en Lean, tienes un software que automáticamente te lo verifica. Hay demostraciones de 1500 líneas, hay demostraciones de 15.000 líneas en Lean; eso un humano es imposible. Que lo pille con cientos de lemas que eso después traducido al lenguaje humano reduce los ejemplos. Entonces, esto es un poco la circunstancia en la que tenemos y ahora mismo está habiendo muchas demostraciones. De hecho, por decir, hoy mismo se ha publicado una nueva demostración. Hoy es 22 de enero de 2026. Problema 347, 347 ¿vale? Entonces, y ayer otra,…
Francis Villatoro describe un artículo publicado por Nat Zosanathan que afirma no haber tenido intervención humana en su creación, utilizando ChatGPT y Aristóteles.
Habla: Francis VillatoroPalabras #13reescritura demostración formalizada aristótelesprograma 728 en archivearistóteles software resolución programa…de interés artificial y estas cosas y no tengo tiempo de perder el tiempo mirando demostraciones, lo que me dé lo meto, yo soy la persona que va muriendo de un lado a otro, lo mismo hizo un script que le pasa automáticamente las cosas, porque hay informática. Y este señor que se llama Nat Zosanathan ha publicado el primer artículo que, según él, no ha tenido ningún tipo de intervención humana. La demostración la hizo ChatGPT 5.2 Pro, la transcripción a Lean la hizo Aristóteles, la verificación se hizo en Lean y el artículo, que es el que ha publicado en Archive, un artículo que se llama Resolución del programa 728, una reescritura de la demostración formalizada con Aristóteles, Aristóteles del software, lo publicó el 12 de junio, ya va. por la tercera o cuarta versión, lo que hizo fue utilizar ChagPT, es decir, con la demostración de Lean, ahora le dijo a ChagPT, conviérteme esta demostración en versión humana, ahí él, que es matemático, es doctor en matemáticas, le estuvo diciendo qué tenía…
Francis Villatoro describe cómo la inteligencia artificial está logrando demostrar resultados matemáticos utilizando técnicas y estrategias de demostración ya conocidas.
Habla: Francis VillatoroSignificado #3inteligencia artificial demuestra resultados matemáticosdemostraciones lean aristótelesmatemático experto no replica demostración ia…o lo que sea la intensidad artificial te lo hace en un rato, en un par de horas. Y si lo ha hecho bien, maravilloso. Y si lo ha hecho mal, pues nada, se olvida como si nunca hubiera ocurriendo. Entonces, lo que está ocurriendo ahora mismo es que estamos Logrando con intensidad artificial demostrar, con demostraciones un poquito más cortas, un poquito más largas, resultados que en principio son una aplicación natural de las técnicas de demostración, las estrategias de demostración conocidas; y que un matemático experto en ese área podría haberlo hecho. Le ocurre que está ocurriendo que no lo está haciendo. Un matemático experto en ese área, lo están haciendo matemáticos expertos en otras cosas o informáticos y gente así que le gusta trabajar en estas cosas de matemática recreativa, entre comillas, de demostrar problemas de RIS. Hasta ahora no se ha demostrado…
Francis Villatoro y Héctor Socas comentan sobre la dificultad de demostrar problemas matemáticos a pesar de su fácil formulación, contrastando con el estilo de demostración de Grothendieck donde la prueba está implícita en el enunciado.
Habla: Francis VillatoroSignificado #11demostraciones grothendieck implícitasenunciado como demostración grothendieckproblemas matemáticos difíciles de demostrar…tanto la demostración que ya es prácticamente imposible sacar. Sí, es eso, es ir al detalle. ¿Sabéis quién hizo el primer resultado no trivial? El BIS. El 1940 dio la primera cota. Claro, pero la cota es enorme. Pero ya os digo, ese tipo de problemas son muy fáciles de formular y muy difíciles de demostrar. Pero eso no lo sabes hasta que te pones a demostrarlo. El enunciado no tiene nada que ver con las demostraciones de Grotendi. la demostración de Grothendieck en la que el enunciado de lo que quieres demostrar es bastante largo, es como un párrafo y contiene la demostración. Entonces la demostración es obvio por el enunciado, punto. Te lo lees y dices pues sí, pues es verdad. Fíjate que es una demostración en la que no hay que demostrar nada porque está todo escrito en el propio enunciado. O sea, están todos los extremos. Bueno, venga, siguiente tema, Juan Carlos, esto de las burbujas que se mueven así como les da la gana Burbujitas galopantes, y veréis luego por qué se llama así, pues sí, las burbujitas estas que parecen unos chismes absolutamente triviales y sin embargo llevan troleando a la física bastante tiempo. El mismo Leonardo da Vinci ya se fijó en que las burbujas en…