Ir al contenido principal

Readings shared October 26, 2025

The readings shared in Bluesky on 26 October 2025 are:

Readings shared October 25, 2025

The readings shared in Bluesky on 25 October 2025 are:

Readings shared October 22, 2025

The readings shared in Bluesky on 22 October 2025 are:

Una refutación inusual del problema de Erdős

Terence Tao ha comentado en Mastodon otro ejemplo interesante de la asistencia informática en matemáticas, que involucra nuevamente a los problemas de Erdös: el Problema #707, anteriormente marcado como "abierto", ahora está "refutado" - con la refutación formalizada en Lean. Pero el camino hacia esa refutación fue bastante inusual, y no encajaba perfectamente en ninguna de las narrativas estándar sobre la IA en las matemáticas.

La refutación inicial fue obra de humanos usando argumentos convencionales, sin ayuda inicial de LLMs. Sin embargo, descubrieron después que el problema ya había sido resuelto tres décadas antes por Hall, un hallazgo que las búsquedas bibliográficas humanas y asistidas por IA no detectaron. Para formalizar su prueba en Lean, los autores, sin experiencia previa, usaron ChatGPT en un proceso de "codificación por vibraciones", logrando generar unas 3000 líneas de código verificadas. Este proceso incluso permitió corregir un error en la formalización original del problema.

Este caso ilustra un uso muy específico y responsable de la IA: no para generar ideas matemáticas, sino para asistir en la creación de código formal verificable. La formalización complementa, pero no reemplaza, la prueba humana central. Debido a su contribución crucial en esta etapa, tanto ChatGPT como Lean aparecen como coautores del artículo, destacando un modelo inusual de colaboración humano-IA.

Readings shared October 21, 2025

The readings shared in Bluesky on 21 October 2025 are:

Readings shared October 20, 2025

The readings shared in Bluesky on 20 October 2025 are:

Readings shared October 18, 2025

The readings shared in Bluesky on 18 October 2025 are:

Readings shared October 17, 2025

The readings shared in Bluesky on 17 October 2025 are:

Readings shared October 16, 2025

The readings shared in Bluesky on 16 October 2025 are:

Readings shared October 15, 2025

The readings shared in Bluesky on 15 October 2025 are:

Readings shared October 14, 2025

The readings shared in Bluesky on 14 October 2025 are:

Readings shared October 13, 2025

The readings shared in Bluesky on 13 October 2025 are:

Readings shared October 10, 2025

The readings shared in Bluesky on 10 October 2025 are:

Readings shared October 7, 2025

The readings shared in Bluesky on 7 October 2025 are:

Readings shared October 6, 2025

The readings shared in Bluesky on 6 October 2025 are:

Readings shared October 4, 2025

The readings shared in Bluesky on 4 October 2025 are:

Readings shared October 03, 2025

The readings shared in Bluesky on 03 October 2025 are:

Readings shared October 01, 2025

The readings shared in Bluesky on 01 October 2025 are:

Readings shared September 29, 2025

The readings shared in Bluesky on 29 September 2025 are:

Readings shared September 28, 2025

The readings shared in Bluesky on 28 September 2025 are:

Readings shared September 23, 2025

The readings shared in Bluesky on 23 September 2025 are:

Readings shared September 22, 2025

The readings shared in Bluesky on 22 September 2025 are:

Readings shared September 20, 2025

The readings shared in Bluesky on 20 September 2025 are:

Readings shared September 19, 2025

The readings shared in Bluesky on 19 September 2025 are:

Readings shared September 18, 2025

The readings shared in Bluesky on 18 September 2025 are:

Readings shared September 17, 2025

The readings shared in Bluesky on 17 September 2025 are:

Readings shared September 12, 2025

The readings shared in Bluesky on 12 September 2025 are

Readings shared September 11, 2025

The readings shared in Bluesky on 11 September 2025 are

Readings shared September 10, 2025

The readings shared in Bluesky on 10 September 2025 are

Readings shared September 9, 2025

The readings shared in Bluesky on 9 September 2025 are

Readings shared September 5, 2025

The readings shared in Bluesky on 5 September 2025 are

Readings shared September 4, 2025

The readings shared in Bluesky on 4 September 2025 are

Readings shared September 3, 2025

The readings shared in Bluesky on 3 September 2025 are

Readings shared September 1, 2025

The readings shared in Bluesky on 1 September 2025 are

Readings shared August 30, 2025

The readings shared in Bluesky on 30 August 2025 are

Readings shared August 29, 2025

The readings shared in Bluesky on 29 August 2025 are

Readings shared August 28, 2025

The readings shared in Bluesky on 28 August 2025 are

Readings shared August 26, 2025

The readings shared in Bluesky on 26 August 2025 are

Readings shared August 25, 2025

The readings shared in Bluesky on 25 August 2025 are

Readings shared August 24, 2025

The readings shared in Bluesky on 24 August 2025 are

Readings shared August 22, 2025

The readings shared in Bluesky on 22 August 2025 are

Readings shared August 20, 2025

The readings shared in Bluesky on 20 August 2025 are

Readings shared August 18, 2025

The readings shared in Bluesky on 18 August 2025 are

Readings shared August 17, 2025

The readings shared in Bluesky on 17 August 2025 are

Readings shared August 15, 2025

The readings shared in Bluesky on 15 August 2025 are

HaLLMos (IA para aprender a escribir demostraciones matemáticas)

HaLLMos es un sistema de inteligencia artificial gratuito diseñado para ayudar en la redacción de pruebas matemáticas de nivel básico. El sistema revisa borradores, identifica lagunas en el razonamiento y facilita el proceso de iteración sin revelar directamente la respuesta.

Es completamente gratuito, funciona desde el navegador web y no requiere crear una cuenta. Los usuarios pueden elegir entre ejercicios introductorios para aprender técnicas de demostración o utilizar el espacio de pruebas libre para trabajar con sus propios problemas.

Readings shared August 14, 2025

The readings shared in Bluesky on 14 August 2025 are

Readings shared August 13, 2025

The readings shared in Bluesky on 13 August 2025 are

Reseña de «The Infinity Project (How to use AI and mathematics to prove and improve science and security)»

En el artículo «The Infinity Project (How to use AI and mathematics to prove and improve science and security)» se propone invertir 112,5 MUSD en un concurso entre institutos de matemáticas para formalizar el conocimiento matemático en programas verificables. Con IA y lenguajes como Lean, se busca traducir y validar pruebas, democratizando el acceso a las matemáticas.

El objetivo es aplicar esta infraestructura para aumentar el rigor científico y reforzar la ciberseguridad. Formalizar teorías y procesos permitiría optimizar la investigación, prevenir fallos en sistemas críticos y reducir vulnerabilidades, con beneficios económicos y sociales significativos.

El plan incluye crear una amplia biblioteca matemática, entrenar IA para generar nuevo conocimiento útil y mostrar aplicaciones prácticas. Se plantea una colaboración entre academia, industria y gobiernos, con el potencial de abrir nuevas industrias y transformar ciencia, tecnología y seguridad.

Readings shared August 9, 2025

The readings shared in Bluesky on 9 August 2025 are

Readings shared August 10, 2025

The readings shared in Bluesky on 10 August 2025 are

Readings shared August 8, 2025

The readings shared in Bluesky on 8 August 2025 are

Readings shared August 6, 2025

The readings shared in Bluesky on 6 August 2025 are

Readings shared August 5, 2025

The readings shared in Bluesky on 5 August 2025 are

Readings shared August 2, 2025

The readings shared in Bluesky on 2 August 2025 are

Readings shared August 1, 2025

The readings shared in Bluesky on 1 August 2025 are

Readings shared July 31, 2025

The readings shared in Bluesky on 31 July 2025 are

Readings shared July 29, 2025

The readings shared in Bluesky on 29 July 2025 are

Readings shared July 28, 2025

The readings shared in Bluesky on 28 July 2025 are

Readings shared July 27, 2025

The readings shared in Bluesky on 27 July 2025 are

Reseña de «Solving formal math problems by decomposition and iterative reflection»

El artículo «Solving formal math problems by decomposition and iterative reflection» presenta Delta Prover, un nuevo sistema que resuelve problemas matemáticos complejos. Este agente utiliza un LLM que interactúa con el asistente de pruebas Lean 4. Mediante una descomposición de problemas y una reparación iterativa de las pruebas, el sistema aprende de los errores para construir demostraciones verificables. Alcanza un rendimiento del 95.9% de éxito en los problemas de miniF2F, superando a otros métodos sin necesitar un costoso reentrenamiento del modelo.

Readings shared July 26, 2025

The readings shared in Bluesky on 26 July 2025 are

Readings shared July 25, 2025

The readings shared in Bluesky on 25 July 2025 are

Readings shared July 24, 2025

The readings shared in Bluesky on 24 July 2025 are

Readings shared July 22, 2025

The readings shared in Bluesky on 22 July 2025 are

Readings shared July 18, 2025

The readings shared in Bluesky on 18 July 2025 are

Readings shared July 18, 2025

The readings shared in Bluesky on 18 July 2025 are

Readings shared July 17, 2025

The readings shared in Bluesky on 17 July 2025 are

Readings shared July 16, 2025

The readings shared in Bluesky on 16 July 2025 are

Readings shared July 15, 2025

The readings shared in Bluesky on 15 July 2025 are

Readings shared July 14, 2025

The readings shared in Bluesky on 14 July 2025 are