Búsqueda · 27 momentos en 10 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetramanujan mito demostración matemáticademostración pasos firme investigación matemáticafórmulas complejas verificación rigurosaSrinivasa RamanujanFrancis VillatoroTerence TaoLeanWilesÚltimo Teorema de Fermat
Demostración pasos firme investigación matemática
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro explica cómo la exigencia actual de demostrar cada paso en matemáticas obliga a los investigadores a evitar atajos y riesgos, contrastando esto con el enfoque anterior que permitía generar fórmulas complejas sin una verificación rigurosa.
…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…
Significado #1 · Palabras #1
Francis Villatoro comparte su opinión personal sobre las demostraciones asistidas por computadora, expresando la perspectiva de un matemático tradicional.
Habla: Francis VillatoroSignificado #8matemático tradicional comprensión demostraciónavances matemáticos comprensión objetosrelaciones entre objetos matemáticas…esos 1020 y tantos casos había que hacerlo por computadora. Entonces, vos siendo matemático, pero siendo más afín a otras ciencias en las cuales el cálculo, el cómputo es importante, ¿vos cómo te sentís acerca de las demostraciones asistidas por computadora? Acá viene lo personal. Bueno, a nivel personal, al matemático de toda la vida lo que nos gusta es disfrutar de la comprensión de la demostración; o sea, el avance en matemáticas es un avance a base de comprender objetos, de comprender cosas. Hay una serie de objetos que tienen relaciones entre ellos y lo que tú quieres es entender. Esas relaciones y disfrutar de la comprensión. O sea, vos decís que hay algo del goce y no solamente del estar seguro. Claro, claro. Porque la demostración cumple las dos cosas: saber que existe una demostración y que la ha hecho alguien, pues para mí es…
Francis Villatoro explica cómo la inteligencia artificial generativa está cambiando la forma en que los matemáticos abordan las demostraciones, contrastando con el uso limitado de demostradores automáticos en el pasado.
Habla: Francis VillatoroPalabras #3demostraciones 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 menciona un caso específico relacionado con las demostraciones del matemático Terence Tao, destacando la detección de una pequeña sutileza y error en una de sus pruebas.
Habla: Francis VillatoroPalabras #7terence tao demostración matemáticasutileza error prueba taodemostración tao vista por cuatrolean detección errores demostraciones taoterence tao demostración matemática leanlean certificación demostración matemáticalean validación demostraciones matemáticasdemostrador automático artículo matemáticorevisores artículo mundo detalle…que lo haya hecho todo bien, que no haya ningún resquicio, pero en pocos días puedes transferir tu demostración en papel a una demostración por ordenador, pasársela al demostrador automático y el demostrador automático te dice sí, no te has equivocado. ¿O ha pasado con demostraciones 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 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 explica que Terence Tao está liderando una nueva forma de ver la labor del matemático y que se están considerando sistemáticamente pasar todas las demostraciones a Lean.
Habla: Francis VillatoroPalabras #15terence tao lidera nueva visión matemáticodemostraciones wiles lean última versiónúltimo teorema fermat escrito en lean…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 demostraciones. Ahora mismo uno de los temas, por ejemplo, la demostración de Wiles, el último teorema de Fermat, está ahora mismo escribiéndose en Lean. Ahora mismo eso puede costar del orden de un año, ¿por qué? Porque hay que pasar toda la demostración de Wiles, pero además todo lo publicado previo en lo que se basa en Wiles. Porque Wiles se basa en 30 años de matemática, entonces tienes que codificar una barbaridad de conocimiento de matemática. La conjetura de…
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 VillatoroPalabras #14ramanujan desarrollos convergentes divergentesmatemáticas ramanujan sin demostraciones formalesramanujan operación rápida desarrollos…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…
Francis Villatoro explica cómo la exigencia actual de demostrar cada paso en matemáticas obliga a los investigadores a evitar atajos y riesgos, contrastando esto con el enfoque anterior que permitía generar fórmulas complejas sin una verificación rigurosa.
Habla: Francis VillatoroSignificado #1 · Palabras #1ramanujan mito demostración matemáticademostración pasos firme investigación matemáticafórmulas complejas verificación rigurosa…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…