Búsqueda · 34 momentos en 19 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetrobert manperson charla annals of mathematicsnash emérito escuela de matemáticaprinceton postdoc robert manpersonannals of mathematics demostraciones computacionalescambio editorial annals of mathematicsmacpherson desacuerdo demostraciones computacionalesAnnals of MathematicsPrincetonRobert MacPhersonHalesKeplerFrancis VillatoroRobert ManpersonNashGastón GiribetLeanTerence Tao
Annals of Mathematics demostraciones computacionales
Con
0:000:301:001:302:002:303:003:15
Gastón Giribet continúa relatando una anécdota personal sobre su época como postdoc en Princeton, y menciona un cambio abrupto en la decisión editorial de Annals of Mathematics respecto a la publicación de demostraciones asistidas por computadora.
…en la escuela de ciencias naturales, pero ver a los matemáticos era como, si sos muy nerdes, como estar adelante, como ser cholulo con las estrellas de rock. Estaba MacPherson, De Ling, en ese momento Nash estaba vivo, esos tipos, Spencer y Wiles. Bueno, La idea es que Manperson dio una charla en la cual se discutía cuándo Annals of Mathematics, la conspicua... Robert Manperson sigue vivo, pero es emérito ahora, pero en ese momento estaba en la escuela de matemática. Sí, todos los que mencioné siguen vivos, sacando Nash, son todos eméritos ahí. Entonces la cuestión es, en ese momento había un cambio abrupto en la decisión. Editorial de Annals of Mathematics, acaso la más importante de la revista de Matemática, también editada por Princeton. ¿Qué era empezar a aceptar demostraciones asistidas por computadora para ser publicadas? No porque no se aceptaran como demostraciones, sino como la revista dice: no, con esas huevadas a mí no me vengan. Pero era la primera vez que la revista se abría, hace 20 años, a la posibilidad de empezar a publicar esas cosas. Se notaba en MacPherson que él no parecía estar muy de acuerdo; no parecía mostrar su aquiescencia con esa idea. Pero en ese momento se estaba discutiendo acerca de una de las demostraciones sobre la conjetura de Kepler, que en algún sentido tiene un espíritu parecido a esto: las formas óptimas de apilar esferas en generalizaciones dimensionales de los tetraedros.…
Significado #1 · Palabras #1
Gastón Giribet continúa relatando una anécdota personal sobre su época como postdoc en Princeton, y menciona un cambio abrupto en la decisión editorial de Annals of Mathematics respecto a la publicación de demostraciones asistidas por computadora.
Habla: Gastón GiribetSignificado #1 · Palabras #1robert manperson charla annals of mathematicsnash emérito escuela de matemáticaprinceton postdoc robert manpersonannals of mathematics demostraciones computacionalescambio editorial annals of mathematicsmacpherson desacuerdo demostraciones computacionales…en la escuela de ciencias naturales, pero ver a los matemáticos era como, si sos muy nerdes, como estar adelante, como ser cholulo con las estrellas de rock. Estaba MacPherson, De Ling, en ese momento Nash estaba vivo, esos tipos, Spencer y Wiles. Bueno, La idea es que Manperson dio una charla en la cual se discutía cuándo Annals of Mathematics, la conspicua... Robert Manperson sigue vivo, pero es emérito ahora, pero en ese momento estaba en la escuela de matemática. Sí, todos los que mencioné siguen vivos, sacando Nash, son todos eméritos ahí. Entonces la cuestión es, en ese momento había un cambio abrupto en la decisión. Editorial de Annals of Mathematics, acaso la más importante de la revista de Matemática, también editada por Princeton. ¿Qué era empezar a aceptar demostraciones asistidas por computadora para ser publicadas? No porque no se aceptaran como demostraciones, sino como la revista dice: no, con esas huevadas a mí no me vengan. Pero era la primera vez que la revista se abría, hace 20 años, a la posibilidad de empezar a publicar esas cosas. Se notaba en MacPherson que él no parecía estar muy de acuerdo; no parecía mostrar su aquiescencia con esa idea. Pero en ese momento se estaba discutiendo acerca de una de las demostraciones sobre la conjetura de Kepler, que en algún sentido tiene un espíritu parecido a esto: las formas óptimas de apilar esferas en generalizaciones dimensionales de los tetraedros.…
Francis Villatoro comparte su opinión personal sobre las demostraciones asistidas por computadora, expresando la perspectiva de un matemático tradicional.
Habla: Francis VillatoroSignificado #10matemá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 menciona el trabajo de Hales sobre la conjuntura de Kepler, destacando que fue publicado en Annals of Mathematics y consistió en gigabytes de código.
Habla: Francis VillatoroPalabras #3conjuntura de kepler trabajo halesannals of mathematics publicación halesgigabytes código conjuntura kepler…una posición, bueno, no importa, pero resolviste tu problema. O algunas personas pueden decir, sí, pero ¿cuánto de eso es entender? ¿Y qué es física si no entender la naturaleza? Tú has comentado el caso de la demostración de la conjuntura de Kepler, ¿no? El trabajo famoso de Hales desde el 98. Ese acabó, fue el tema que tú has comentado, ¿no? Acabó publicándose en Anas Mathematics. El problema que tenía es que eran gigabytes de código. O sea, que no eran, no estamos hablando de un código de cien líneas o de mil líneas. Era un código con un tamaño tremendo, súper matematizado y súper no sé qué, donde se podía colar un error en cualquier lugar. Eso generaba una cierta tensión, una cierta duda. Pero la belleza de la matemática es comprender. entonces, si tú tienes un código, si una máquina comprende por ti, has perdido el gran elemento de belleza que tienen las matemáticas es decir, ya es una matemática fea, porque está entendiendo a alguien por ti…
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 #4demostraciones 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 una nueva tendencia en matemáticas donde se espera que todos los matemáticos aprendan a usar herramientas como Lean para validar sus demostraciones.
Habla: Francis VillatoroSignificado #8lean validación demostraciones matemáticasdemostrador automático artículo matemáticorevisores artículo mundo detalle…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 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 #17terence 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…