45 noticias
Este artículo técnico explica cómo formalizar una prueba de teoría de la computación utilizando el lenguaje de programación Lean, dirigido a ingenieros de software con conocimientos básicos de lógica y programación. El autor aborda un problema específico del libro 'Introduction to the Theory of Comp
El reciente viralizado de un tweet de Boris Cherny que utilizó TLA+ para modelar el Claude Agent SDK ha generado un interés masivo en el uso de modelos formales en la programación asistida por IA. TLA+ (Temporal Logic of Actions) es un lenguaje de especificación que describe el comportamiento tempor
Trail of Bits ha documentado cómo utilizó agentes de inteligencia artificial para desarrollar herramientas de auditoría personalizadas antes de revisar el código de la Miden VM, una máquina virtual de conocimiento cero. Durante seis meses, el equipo construyó desde cero un servidor LSP, un descompil
Un equipo de diez agentes de IA, coordinados mediante un tablero de mensajes, ha desarrollado un nuevo algoritmo determinista llamado C-HD para calcular distancias de caminos más cortos en grafos dirigidos con pesos reales no negativos. Este avance, respaldado por una verificación formal completa en
Un análisis técnico utilizando inteligencia artificial ha identificado vulnerabilidades adversariales significativas en varias funciones hash populares, como xxHash, komihash y HighwayHash. El estudio, realizado por un investigador que empleó la herramienta Claude Fable para examinar el proyecto SMh
El artículo 'Semantics for 2D Rasterization', presentado en arXiv el 24 de marzo de 2026, introduce μSkia, una semántica formal para la biblioteca de gráficos 2D Skia. Este trabajo aborda la ineficiencia en las secuencias de operaciones de aplicaciones que utilizan librerías de rasterización como Sk
Un desarrollador de software ha documentado su proceso para generar una prueba formal en Lean de la conjetura de refinamiento de John Conway, un problema abierto en la teoría de los números surrealistas. El autor, que se describe como un novato en matemáticas, utilizó un modelo de lenguaje de fronte
Bend es un lenguaje de programación diseñado para eliminar la ambigüedad en la interacción con agentes de inteligencia artificial, garantizando que el código generado cumpla estrictamente con las especificaciones definidas por el usuario. A diferencia de los lenguajes tradicionales, Bend utiliza un
La investigación matemática enfrenta una crisis de divulgación debido a la capacidad de las grandes empresas de inteligencia artificial para resolver problemas complejos mediante computación intensiva. Este fenómeno, descrito como la 'caída de la economía de la demostración', permite a corporaciones
El texto analiza el impacto de la inteligencia artificial en la matemática, argumentando que la era del matemático humano está terminando. El autor, citando el reciente avance de OpenAI en la resolución de problemas del Premio Millennium, sugiere que la IA no acelerará la investigación, sino que la
El autor argumenta que los laboratorios de frontera de IA no han logrado la autonomía total que prometen, citando el incidente de Navier-Stokes como ejemplo de la necesidad de supervisión humana. A diferencia de la narrativa de reemplazo automático, los modelos actuales requieren supervisión laborio
Investigadores Alpöge y Buckmaster han logrado un avance significativo en el problema de la regularidad global de las ecuaciones de Navier-Stokes tridimensionales incompresibles. Su trabajo, que se apoya en investigaciones previas de Córdoba y Martínez-Zoroa, demuestra la existencia de singularidade
MathKernel es una biblioteca de Python y servidor MCP (protocolo de contexto para modelos) que actúa como núcleo matemático multi-motor diseñado para que los modelos de lenguaje de gran tamaño (LLM, por sus siglas en inglés) puedan realizar cálculos avanzados sin sacrificar el rigor. La herramienta
Claude completa en 11 días la primera demostración formal del Último Teorema de Fermat La inteligencia artificial de Anthropic, Claude, ha logrado en apenas 11 días lo que la comunidad matemática llevaba años intentando: la primera demostración completa, verificada por ordenador, del Último Teorema
El matemático Terence Tao anunció la apertura de Palomar, un registro de demostraciones matemáticas verificadas en el lenguaje de pruebas Lean, una iniciativa impulsada por Lean FRO e ICARM. El proyecto surge ante la proliferación de pruebas generadas por inteligencia artificial, algunas formalizada
El artículo repasa los argumentos del clásico paper de 1979 'Social Processes and Proofs of Theorems and Programs', que sostenía que la verificación formal de programas estaba abocada al fracaso, y los contrasta con la situación actual. En 1979, los autores defendían que las demostraciones matemátic
Anthropic anunció el lunes que un modelo de inteligencia artificial aún sin distribuir logró un progreso significativo en la hipótesis de Riemann, uno de los problemas sin resolver más antiguos de las matemáticas, con una recompensa de un millón de dólares por una demostración general. El avance amp
Claude eleva al 67,2% la cota inferior de ceros de la zeta de Riemann Una versión no publicada del modelo de inteligencia artificial Claude, desarrollado por Anthropic, ha elevado del 41,6% al 67,2% la cota inferior conocida de ceros de la función zeta de Riemann que satisfacen la hipótesis de Riem
TheoremDB es un espacio de trabajo público y colaborativo pensado para la investigación matemática asistida por máquina. Su objetivo es resolver un problema habitual entre los agentes de investigación: la repetición de esfuerzos porque los intentos previos, los resultados parciales y los enfoques fa
El matemático Terence Tao advirtió en una conferencia en Filadelfia que la comunidad está "muy, muy cerca" de que un resultado matemático importante sea demostrado y verificado sin que ningún humano pueda comprenderlo y explicarlo. La afirmación, recogida por el periodista Kai Williams en entrevista
Un reciente intento de refutar la conjetura de Collatz, cuya presunta refutación fue verificada en el asistente de pruebas Lean y contrastada con el comprobador independiente Nanoda, resultó ser erróneo: la demostración aprovechaba un fallo en el núcleo de Lean y Nanoda tampoco detectó el problema.
OpenAI ha presentado diez nuevos resultados en matemáticas e informática teórica obtenidos con una versión interna de su próximo modelo principal, Astra, por un coste estimado de unos 2.000 dólares en tokens. Los avances abarcan geometría de altas dimensiones, teoría de códigos, complejidad de circu
La comunidad matemática debate si la adopción masiva de Lean como asistente de demostración interactiva (ITP) ha llegado a un punto de no retorno o si aún es viable apoyar una alternativa con base en teoría de conjuntos. El autor recuerda que hace tres años Lean ya acumulaba impulso gracias al Proye
Los verificadores de tipos no solo evitan errores de programación como sumar cadenas y enteros, sino que además sustentan los asistentes de demostración, lenguajes como Lean y Rocq que validan matemáticamente teoremas. La base de esa capacidad es la correspondencia de Curry-Howard, que establece una
En un artículo técnico extenso, un investigador especializado en verificación formal argumenta por qué Rocq sigue siendo, en su práctica diaria, una herramienta más adecuada que Lean para la verificación de programas, aunque concede que Lean ha ganado tracción en la formalización de matemáticas, sob
El ingeniero y criptógrafo conocido como imperialviolet —figura vinculada al proyecto de navegador Chromium de Google— ha presentado esta semana un experimento singular: un descompresor completo del algoritmo Zstandard (zstd) implementado y verificado formalmente en el lenguaje de programación depen
El proyecto lean-zip, una implementación del algoritmo de compresión DEFLATE escrita en el lenguaje de programación Lean, consigue resultados de compresión más rápidos y con mejor ratio que miniz_oxide, la implementación de referencia en Rust puro. Sobre el corpus estándar Silesia (212 MB), lean-zip
La verificación formal permite demostrar la corrección de enunciados matemáticos escribiendo la prueba en código para que un programa la valide mecánicamente. Entre las herramientas disponibles se encuentran Rocq (antes Coq), Isabelle y Lean, esta última creada en 2013 por Leonardo de Moura en Micro
Gwern Branwen ha publicado una propuesta de investigación titulada 'Lean Software Scaling Laws' que plantea medir empíricamente cómo escala la perplejidad de los modelos de lenguaje grandes (LLM) de programación en función del tamaño del código fuente, tomando Lean como caso de estudio. La hipótesis
La verificación formal permite demostrar matemáticamente que un programa cumple ciertas propiedades en todos los estados alcanzables, a diferencia del testing, que solo descarta un conjunto finito de casos. Para ello se usan lenguajes como Dafny, Lean, Rocq, Isabelle, F* o TLA+, en los que las espec
La irrupción de la inteligencia artificial en las matemáticas ha pasado en pocos años de la regurgitación de fórmulas básicas a la demostración autónoma de teoremas de nivel predoctoral. En el verano de 2025, sistemas de Google DeepMind y OpenAI alcanzaron la medalla de oro en la Olimpiada Internaci
Jane Street, una de las firmas de trading cuantitativo más influyentes de Wall Street, ha anunciado la creación de un equipo dedicado a métodos formales de verificación de software, en un giro estratégico motivado por el auge de la programación agéntica. La decisión marca un cambio radical en la pos
Un repositorio de GitHub ha sido publicado con una implementación formalmente verificada de un algoritmo para la intersección de polígonos, un logro significativo en el campo de la geometría computacional. El proyecto, liderado por schildep, utiliza el asistente de demostración de teoremas Lean 4 pa
ATLAS es una biblioteca masiva de matemáticas formalizadas, desarrollada por Facebook Research, que traduce libros de texto universitarios y de posgrado a código formal utilizando modelos de lenguaje grande (LLMs). Su importancia radica en acelerar el proceso de verificación matemática, permitiendo
Este artículo explora la historia y el panorama actual de la formalización matemática, cuestionando la prevalencia de Lean como la única opción viable. El autor, con décadas de experiencia en el campo, argumenta que la reciente popularidad de Lean, a pesar de sus ventajas (una gran biblioteca, comun
Un equipo de investigadores ha descubierto una vulnerabilidad crítica en el entorno de desarrollo Lean 4, a pesar de que una implementación de zlib (lean-zip) había sido formalmente verificada como correcta por Lean. El hallazgo, realizado por Kiran Gopinathan utilizando un agente Claude y herramien
Este artículo explora el concepto de un "lenguaje de programación perfectible", ejemplificado por Lean. La idea central es que un lenguaje perfectible no solo permite escribir código, sino también expresar propiedades sobre ese código dentro del propio lenguaje. Esto abre la puerta a la verificación
Investigadores de Facebook IA han desarrollado un sistema llamado RepoProver, capaz de formalizar automáticamente libros de texto matemáticos utilizando inteligencia artificial. El sistema, cuyo código está disponible en GitHub, emplea una arquitectura multi-agente que colabora en un repositorio Git
Este artículo presenta el "Mathematics Distillation Challenge – Teorías Ecuacionales", una iniciativa innovadora para avanzar en la investigación matemática a través de la colaboración y la asistencia de la inteligencia artificial. Tradicionalmente, la investigación matemática se ha centrado en un p
El artículo de theorem.dev presenta `lf-lean`, un proyecto innovador que explora el futuro de la ingeniería de software verificada. El problema central que aborda es cómo garantizar la corrección del código generado por la inteligencia artificial (IA), especialmente cuando la capacidad de generación
Un equipo de matemáticos, liderado por Maryna Viazovska (galardonada con la Medalla Fields en 2022), ha formalizado la solución al problema del empaquetamiento de esferas en dimensiones 8 y 24, un hito en la verificación matemática. El problema, que se remonta a la conjetura de Kepler en 1611, busca
El auge de los Modelos de Lenguaje Grandes (LLMs) está transformando la industria del software, generando debates sobre su uso ético y efectivo. Este artículo explora un enfoque menos discutido: el uso determinista de los LLMs, inspirándose en cómo los matemáticos están abordando el desafío de integ
Un matemático con experiencia en programación está explorando el uso del sistema de demostración de teoremas Lean para formalizar las matemáticas, con el objetivo de revolucionar la escritura matemática y el desarrollo de la inteligencia artificial. La formalización, que implica verificar mecánicame
Investigadores han presentado 'Lean Collab', un nuevo sistema colaborativo para la demostración de teoremas utilizando Lean 4 y la red neuronal Ensue. La herramienta busca acelerar la verificación formal, permitiendo que múltiples agentes trabajen en la resolución de problemas matemáticos complejos
El artículo explora la verificación formal de episodios de la serie infantil educativa Cyberchase utilizando el lenguaje de demostración de teoremas Lean. El autor, quien atribuye parte de su éxito en informática a la serie, compara la resolución de problemas en Cyberchase con los desafíos de la ing