Búsqueda · 33 momentos en 16 episodios
Silvana TapiaJuan Carlos GilFrancis VillatoroHéctor SocasBorja TosarGastón Giribetterence tao google deepmind demostracionespublicación nature herramientas inteligencia artificialresultados matemáticos mastodon taointeligencia artificial chateo códigoNatureMastodonGoogle DeepMindTerence TaoLintFrancis VillatoroJuan Carlos GilLeanInteligencia Artificial
Inteligencia Artificial chateo código
Con
0:000:301:001:302:002:303:003:15
Francis Villatoro describe cómo Terence Tao está utilizando herramientas avanzadas de inteligencia artificial proporcionadas por Google DeepMind para generar y publicar demostraciones matemáticas complejas, compartiendo públicamente sus resultados en Mastodon.
…¿vale? Con dos cojones. Ahora mismo, Google DeepMind está financiando a Tao, que Tao use las herramientas de interés artificial más avanzadas del mundo, que no están disponibles para nadie más que para él, porque está cogiendo el state of the art y los que Están publicando lo van a publicar en Nature, a lo grande, y está pasando demostraciones extremadamente complicadas a este tipo de herramientas de manera muy rápida. Habla en Mastodon, él está publicitando toda esta línea que está trabajando ahora, que son cosas de los últimos meses. Está vendiendo los resultados de manera absolutamente increíble, te pone todo el chateo con la inteligencia artificial. Te lo publica junto con el código. Lean y la demostración de que todo ha funcionado. Pero ojo, que eso es un código de un lenguaje que han desarrollado para hacer pruebas formales. Claro, es para demostrar que una demostración es correcta. El otro tipo de pruebas tradicionales matemáticas, de…
Significado #1 · Palabras #1
Francis Villatoro describe cómo Terence Tao está utilizando herramientas avanzadas de inteligencia artificial proporcionadas por Google DeepMind para generar y publicar demostraciones matemáticas complejas, compartiendo públicamente sus resultados en Mastodon.
Habla: Francis VillatoroSignificado #1 · Palabras #1terence tao google deepmind demostracionespublicación nature herramientas inteligencia artificialresultados matemáticos mastodon taointeligencia artificial chateo código…¿vale? Con dos cojones. Ahora mismo, Google DeepMind está financiando a Tao, que Tao use las herramientas de interés artificial más avanzadas del mundo, que no están disponibles para nadie más que para él, porque está cogiendo el state of the art y los que Están publicando lo van a publicar en Nature, a lo grande, y está pasando demostraciones extremadamente complicadas a este tipo de herramientas de manera muy rápida. Habla en Mastodon, él está publicitando toda esta línea que está trabajando ahora, que son cosas de los últimos meses. Está vendiendo los resultados de manera absolutamente increíble, te pone todo el chateo con la inteligencia artificial. Te lo publica junto con el código. Lean y la demostración de que todo ha funcionado. Pero ojo, que eso es un código de un lenguaje que han desarrollado para hacer pruebas formales. Claro, es para demostrar que una demostración es correcta. El otro tipo de pruebas tradicionales matemáticas, de…
Juan Carlos Gil, tras una explicación sobre la digitalización de demostraciones matemáticas, aclara que Terence Tao está utilizando inteligencia artificial generativa para explorar código y menciona el uso de 'Lint', un metademostrador.
Habla: Juan Carlos GilPalabras #2terence tao inteligencia artificial generativalint demostrador más famosolenguaje formal cercano al humano…verdad solo si la máquina lo dice. Y para que la máquina lo diga, tú tienes que haber pasado todo lo que tú has dicho, todo lo que tú has escrito en papel, a la máquina. Pero déjame que lo vuelva a decir, que no sé si yo mismo lo he entendido bien, o sea, no. Es que Tao esté haciendo inteligencia artificial generativa, inventándose cosas, no; la herramienta le ayuda a explorar el código, ¿cómo se llama? Lint Lint, L-A-N, es el demostrador más famoso ahora mismo, y es un metademostrador. Te permite trabajar con un lenguaje bastante próximo al humano, pero es un lenguaje formal, ¿verdad? Si no me equivoco, Francis. Con lo cual, una vez que tienes la prueba, es equivalente a una prueba matemática tradicional con todos los símbolos matemáticos. Ahora mismo el factor es del orden de un factor de 10. Es decir, si en hojas de papel, a mano, a ti te ha cubierto, yo que sé,…
Francis Villatoro describe cómo Terence Tao utiliza Lean y la inteligencia artificial para desarrollar nuevas demostraciones matemáticas, formalizando ideas sencillas en Lean y obteniendo sugerencias de conexiones que antes no había considerado.
Habla: Francis VillatoroPalabras #13terence tao usa lean inteligencia artificiallean formaliza demostraciones matemáticas sencillasinteligencia artificial sugiere conexiones matemáticas tao…Todo eso ahora mismo lo están formalizando y los rumores eran que era inminente que acabaran, o sea que puede ser para mediados del año que viene o para finales del año que viene que lo tengan listo y entonces podrás certificar que no hubo ningún error. y ahora mismo incluso Tao está haciendo otra cosa que es también maravillosa que es desarrollar nuevas demostraciones apoyado en los códigos de Lean. O sea, conforme tú estás buscando ideas para demostrar algo, las vas formalizando en ejemplos más o menos sencillos en Lean y la inteligencia artificial te va ayudando a ver nuevas ideas. entonces Tao ya tiene varios ejemplos en los que la inteligencia artificial le ha dado a la hora de formalizar en el Lean lo que le estaba escribiendo una idea que él no tenía, una conexión con esto 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…