The readings shared in Bluesky on 20 June 2025 are
El demostrador de teoremas Lean ha sido galardonado con el «SIGPLAN Programming Languages Software Award 2025», otorgado por ACM SIGPLAN (Special Interest Group on Programming Languages de la ACM (Association for Computing Machinery).
La cita del premio destaca lo siguiente:
El demostrador de teoremas Lean constituye un sistema informático extraordinario. Fundamentado en sólidas bases teóricas y de ingeniería, Lean ha ejercido y continúa ejerciendo un amplio impacto tanto en la práctica industrial como en la investigación científica.
El proyecto Lean ha generado un impacto particularmente significativo en tres áreas clave: matemáticas, verificación de hardware y software, e inteligencia artificial. En el ámbito matemático, ha logrado una aceptación considerable dentro de la comunidad académica, evidenciada por el desarrollo de Mathlib, una biblioteca creada por usuarios que supera las 1.8 millones de líneas de código.
La credibilidad del sistema se ha consolidado mediante la verificación exitosa de resultados fundamentales, incluyendo Liquid Tensor Experiment (propuesto por el medallista Fields Peter Scholze) y la verificación de la conjetura polinomial de Freiman-Ruzsa dirigida por el medallista Fields Terence Tao. Estos logros han proporcionado al sistema un reconocimiento sin precedentes en la comunidad científica internacional.
Es indiscutible que los métodos formales basados en Lean ocuparán una posición central en el desarrollo de las matemáticas durante los próximos años. Paralelamente, el sistema ha demostrado su valor práctico en proyectos industriales de verificación críticos, tales como la verificación del lenguaje de control de acceso Cedar en Amazon Web Services, la validación del muestreador SampCert para privacidad diferencial (también en AWS), y diversos proyectos de verificación blockchain en empresas líderes como StarkWare y Nethermind.
Finalmente, el éxito de iniciativas como AlphaProof de DeepMind y la adopción estratégica de Lean por parte de empresas emergentes como Harmonic han consolidado su posición como la solución de referencia para sistemas de razonamiento matemático potenciados por inteligencia artificial.
The readings shared in Bluesky on 19 June 2025 are
El artículo «Can A.I. quicken the pace of math discovery?» presenta la iniciativa "Exponentiating Mathematics" de DARPA. Su objetivo es desarrollar una IA como coautor para acelerar la investigación en matemáticas.
El programa confronta limitaciones de los LLMs actuales. Estos fallan en razonamiento lógico-matemático y generan "alucinaciones". La solución propuesta integra IA con asistentes de prueba formales como Lean.
Lean desempeña el papel central como verificador. Los LLMs generan pruebas formales que Lean acepta o rechaza según su corrección. Esta iteración crea un ciclo de refinamiento continuo. Su lenguaje específico resulta arduo, pero su metodología es fundamental. La verificación formal garantiza corrección absoluta y elimina alucinaciones de LLMs generativos.
La meta es crear IA que sugiera ideas y construya pruebas verificadas. Los sistemas formales garantizan fiabilidad absoluta. Esto transforma herramientas actuales en colaboradores matemáticos confiables.
The readings shared in Bluesky on 17 June 2025 are
The readings shared in Bluesky on 16 June 2025 are
The readings shared in Bluesky on 15 June 2025 are
El vídeo «Hablemos de Lisp» presenta un diálogo que explora la historia, conceptos fundamentales y legado duradero del lenguaje de programación Lisp. El análisis comienza con una perspectiva histórica rigurosa, desmitificando la creencia común de que fue el primer lenguaje funcional. En su lugar, identifica al IPL (Information Processing Language) de Herbert Simon y Allen Newell como su precursor fundamental.
El vídeo establece una distinción crucial entre los diferentes pioneros de la inteligencia artificial: mientras que Simon y Newell sentaron las bases conceptuales del campo, John McCarthy acuñó el término "inteligencia artificial" y creó LISP, inspirado precisamente por las capacidades de procesamiento de listas que había demostrado IPL.
Respecto al paradigma funcional, el análisis revela que LISP, en sus primeras etapas, no cumplía estrictamente con los principios de la programación funcional moderna, como la inmutabilidad y la gestión explícita de efectos secundarios. La formalización teórica de este paradigma se atribuye posteriormente a la familia de lenguajes ISWIM, propuesta por Peter Landin.
La génesis de la implementación de LISP se sigue de FLPL (Fortran Lisp Processing Language), un lenguaje intermedio que resultó fundamental por introducir la expresión condicional, una construcción sintáctica que más tarde sería adoptada ampliamente por lenguajes imperativos.
Una de las discusiones más reveladoras del vídeo aborda la distinción entre el concepto original de LISP (1959) y su primera implementación (1960). McCarthy había concebido inicialmente una sintaxis de alto nivel (M-expresión) que se compilaría a una representación simbólica intermedia (S-expresión). Sin embargo, el éxito de la implementación de la función eval puso de manifiesto la profunda simetría entre código y datos —la homoiconicidad— inherente a la S-expresión.
Esta propiedad fundamental resultó tan poderosa que llevó al abandono de la M-expresión, convirtiendo la sintaxis intermedia en el lenguaje de programación definitivo.
El vídeo concluye evaluando el legado perdurable de LISP en la ciencia de la computación. Se le atribuye la introducción de conceptos fundamentales como la expresión condicional y la recolección automática de basura (garbage collection). Su relevancia actual se manifiesta a través de sus numerosos dialectos modernos, destacando Common Lisp, Scheme, Clojure y Racket, que continúan explorando y expandiendo los principios originales del lenguaje.
En la entrevista "Hardest problems in mathematics, physics & the future of AI", Terence Tao comparte sus reflexiones sobre diversos problemas fundamentales sin resolver en análisis y teoría de números, examina la metodología de la investigación matemática contemporánea y analiza el papel emergente que desempeñan la verificación formal y la inteligencia artificial en la disciplina.
Tao examina varios problemas que se encuentran en la frontera del conocimiento matemático actual. En análisis, dedica especial atención al problema de Kakeya, destacando sus profundas conexiones con el análisis armónico y las ecuaciones en derivadas parciales. Su análisis revela cómo este problema aparentemente geométrico se entrelaza con áreas fundamentales del análisis moderno.
Respecto al problema de la regularidad de Navier-Stokes, Tao identifica la "supercriticalidad" como el obstáculo central que impide su resolución. De manera particularmente innovadora, describe su construcción teórica de un análogo fluídico de una máquina de von Neumann, presentándola como una estrategia prometedora para demostrar la existencia de explosiones en tiempo finito (blowup) en las soluciones de estas ecuaciones.
En el ámbito de la teoría de números, Tao analiza la conjetura de los primos gemelos, atribuyendo su persistente dificultad a la extrema fragilidad del patrón subyacente. Explica cómo este patrón podría ser destruido por "conspiraciones" matemáticas imperceptibles para los métodos estadísticos tradicionales. Esta fragilidad contrasta marcadamente con la robustez inherente de las progresiones aritméticas, como las estudiadas en el teorema de Green-Tao.
Un concepto clave que emerge de su análisis es el problema de la paridad*, que identifica como un obstáculo metodológico fundamental en teoría de números. En cuanto a la hipótesis de Riemann, Tao la considera aún más inaccesible a los métodos actuales, situándola en una categoría propia de dificultad.
Un hilo conductor de la entrevista es la exploración de la dicotomía entre estructura y aleatoriedad, un tema que permea múltiples áreas de las matemáticas. Esta perspectiva filosófica informa tanto el análisis de problemas específicos como la comprensión general de los fenómenos matemáticos.
Metodológicamente, Tao defiende un enfoque de simplificación estratégica en la resolución de problemas. Su estrategia consiste en descomponer problemas complejos en dificultades individuales, abordar cada una por separado, y posteriormente integrar las soluciones. Este método refleja una filosofía pragmática que prioriza la claridad conceptual y el progreso incremental.
Una porción sustancial de la discusión se centra en el impacto transformador de la prueba asistida por ordenador, con particular énfasis en el asistente de pruebas Lean. Tao ilustra su potencial a través de su "Equational theories project" de clasificación de 22 millones de identidades algebraicas, demostrando cómo estas herramientas facilitan la colaboración a gran escala y la gestión de la complejidad en pruebas matemáticas modernas.
Sus predicciones sobre el futuro son especialmente significativas: anticipa que las herramientas de inteligencia artificial revolucionarán la formalización matemática. Más ambiciosamente, prevé que la IA podría generar conjeturas matemáticas genuinamente novedosas al identificar conexiones profundas entre campos aparentemente dispares.
La entrevista proporciona una ventana excepcional al proceso intelectual de uno de los matemáticos más influyentes de nuestra época. Tao logra equilibrar la precisión técnica con la accesibilidad conceptual, ofreciendo tanto análisis detallados de problemas específicos como reflexiones más amplias sobre la naturaleza de la investigación matemática.
Su visión integra consideraciones técnicas, marcos filosóficos y prospectivas tecnológicas, presentando una imagen completa de las matemáticas como disciplina en constante evolución. La entrevista destaca no solo los desafíos actuales, sino también las herramientas emergentes que podrían redefinir fundamentalmente cómo se desarrollarán las matemáticas en el futuro.
The readings shared in Bluesky on 14 June 2025 are