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 #11demostraciones matemáticas máquinasconfianza demostración máquina correcciónrevolución matemáticas inteligencia artificialinteligencia artificial generativa matemáticosdemostradores automáticos uso limitadoformalizar demostraciones ordenador matemático…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 tiempo a pasar tu demostración escrita a mano a un demostrador automático requería años de trabajo para después que resulte que el demostrador automático diga: pues sí, no te has equivocado, es correcta. Pero ahora mismo con la Inteligencia Artificial Generativa, ChatGPT y compañía podemos automatizar ese proceso. Las demostraciones en Lean, L-A-N, es fácil, claro; el ChatGPT más o menos te la construye y tú tienes que estar como, es tu demostración, tú…
Francis Villatoro describe cómo el uso de herramientas como Lean permite detectar errores incluso en demostraciones matemáticas complejas realizadas por figuras destacadas como Terence Tao.
Habla: Francis VillatoroSignificado #16lean detección errores demostraciones taoterence tao demostración matemática leanlean certificación demostración matemática…de Tao, de Terence Tao, el matemático más famoso de la actualidad? Que se encontró una pequeña sutileza en una de sus demostraciones. Uy, aquí hay un pequeño error y nadie se había dado cuenta hasta el momento. Es verdad que esas demostraciones las ven 4 o 5. Matemáticos en el mundo. El resto de los matemáticos confiamos en que está bien demostrado; 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…
Francis Villatoro reflexiona sobre cómo Terence Tao está impulsando una revolución en la demostración matemática, anticipando que los matemáticos jóvenes adoptarán estas técnicas en las próximas décadas.
Habla: Francis VillatoroSignificado #19terence tao revoluciona demostración matemáticamatemáticas jóvenes adoptarán técnicas taodemostración en matemáticas próxima década…no había pensado, pero ahora que lo pienso pues es una buena idea y entonces está acelerando ese proceso de búsqueda de ideas a la hora de demostrar y ya tiene varios ejemplos y son absolutamente fascinantes, claro eso ahora mismo lo puede hacer pues Dios En matemáticas, Terence Tao, pero que ya no es un niño, que ya no tiene 30 años, que ya tiene sus 50 a largo, pero probablemente eso lo aprendan a hacer los matemáticos jóvenes en las próximas décadas y lo haga todo el mundo, por lo que promete una enorme revolución a lo que es la demostración en matemáticas. A mí me parece muy valiente por parte de Tao, yo soy muy equipo Tao, pero poquísimo 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…
Francis Villatoro compara al matemático Srinivasa Ramanujan con el uso actual de herramientas como 'Lint' para la revisión de demostraciones matemáticas, señalando que Ramanujan no se enfocaba en demostrar formalmente sus ideas.
Habla: Francis VillatoroSignificado #2 · Palabras #1ramanujan desarrollos convergentes divergentesmatemáticas ramanujan sin demostraciones formalesramanujan operación rápida desarrollosmatemática transfinita ramananujanconjeturas sin verificación ramananujandemostración matemática resultados ramananujanramanujan no era matemático modernoramanujan oileriano sin verificación formalpublicación de resultados correctos ramanojuaneuler matemática símbolos límitescochí relaciones númerosfrancis villatoro euler ramajuanresultados euler ramanujan verdad falsedaddemostración resultados nadie recuerdaintuiciones complejas ramanujanmatemática expresiones complicadas ramanujanramanujan generó matemáticaramanujan mito demostración matemáticademostración pasos firme investigación matemáticafórmulas complejas verificación rigurosapelícula el hombre que conocía infinitofrancis villatoro casting sorpresacoffee break futura película…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 eso. Entonces, gran parte de la matemática. De Ramanujan, que es lo que se llama matemática transfinita, es una matemática que si no viene alguien detrás y demuestra, pues son solamente conjeturas. Por fortuna, Ramanuján ha tenido mucha suerte porque ha habido toda una generación de matemáticos en los últimos 50 años que ha estado demostrando mucho de sus resultados y encontrando que muchos son falsos, que eso a veces no se Publicita, pero muchos son falsos, pero no pasa nada; si es falso pues se tira a la basura y se olvida. Lo importante es lo que es correcto, entonces lo que se está publicando es lo que es correcto, pero claro, Ramanuján no demostraba; es decir, Ramanuján no era un matemático, era un oileriano. Hacía lo Mismo que hacía Euler en su época, que era una cosa pre-cochí, pre-demostraciones y rigor, era jugar con la matemática y con los símbolos como si cualquier cosa se pudiera hacer sin ningún tipo de límite y condición. Eso es lo que hacía Euler. Lo que hacía cochí eran cochinadas. Pero si no recuerdo mal, Francis se sigue utilizando una de sus relaciones para calcular números. Dígitos de pi de forma muy rápida. Muchísimas, hay muchísimas resultados de Euler que son verdad y muchos que son mentiras y hay muchos resultados de Ramanujan que son verdad y muchos que son mentiras, pero los que son verdad, una vez que se demuestra que son verdad, ya se puede ¿Qué pasa? Que nadie se acuerda de quién demostró los resultados de. Ramanujan, es que Ramanujan lo intuyó, lo intuyó, pero no podemos decir lo demostró a Ramanujan; entonces claro, Ramanujan generó mucha matemática, expresiones matemáticas muy complicadas que tú dices. Es tan complicada que hoy en día la única manera que a alguien se le ocurriera una barbaridad de este tipo es que lo demostrara, pero porque hoy en día le obligamos a la gente a demostrar, a dar todos los pasos en firme, a no enfangarse, a no meterse en el barro, hundirse, ahogarse, casi morir y salir vivo de repente con una fórmula súper maravillosa y súper bella estéticamente, pero que nadie sabe si es verdad o no. pero tú dices, no, pero como sobreviví del fango debe de ser verdad, porque soy Ramanujan y pues hasta que alguien lo demuestre no lo es, entonces, bueno, Ramanujan tiene mucho mito a su alrededor Recomiendo la película El hombre que conocía el infinito, ¿no? donde relata su viaje a Hardy. Bueno, es muy amable, muy agradable; no sé cuánto es verdad. Con un actor súper delgado, Ramanujan era muy gordo. Ah, sí, Ramanujan era un gordo. El día que hagan una película sobre vos, Francis, yo voy a hacer el casting; no te vamos a consultarte. Para vos va a ser una sorpresa: vas a ir a la premiere y no vas a saber nada. Bueno, bueno, no sé; vamos a hacer la película de Coffee Break y vamos a buscar; yo me voy a encargar del casting de todos. Estamos viviendo un momento fascinante en la revolución de lo que está ocurriendo en matemáticas en la frontera y nos va a afectar a todos; los que ya tenemos una cierta edad nunca vamos a aprender. No voy a tener la capacidad de ganar intuiciones matemáticas…