software · 33 menciones
Alcides Fonseca sostiene que los sistemas de permisos actuales de los agentes de inteligencia artificial —ya sean permisos granulares por solicitud o un modo “yolo” sin restricciones— son insuficientes para proteger datos críticos. El problema se agrava con el llamado “trío letal”: cuando un agente
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 matemático Terence Tao publica una versión depurada y legible de la demostración de la conjetura de Sendov obtenida en 2025 por Lech Mazur mediante una herramienta de inteligencia artificial, y cuya verificación formal en Lean ya estaba disponible. Tras varios días de trabajo asistido por IA, con
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
El problema de álgebra de bachillerato planteado por Alfred Tarski pregunta si toda identidad verdadera sobre la suma, la multiplicación y la exponenciación de enteros positivos se deduce a partir de una lista de once identidades elementales. El lógico Alex Wilkie demostró en los años setenta que ex
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
OpenAI presentó las soluciones a 10 problemas matemáticos abiertos, algunas enquistadas durante décadas, mediante un modelo interno avanzado conocido como Astra. Los hallazgos abarcan áreas como el empaquetamiento de esferas en dimensiones superiores, los códigos de corrección de errores, la complej
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 Astra, una versión interna de su nuevo modelo de inteligencia artificial generativa, con la que asegura haber resuelto o avanzado en diez problemas matemáticos abiertos durante al menos una década, y en la mayoría de los casos durante mucho más tiempo. El coste total de los cálc
OpenAI anunció la resolución de diez problemas matemáticos abiertos mediante un modelo aún por publicar, un hito que, según matemáticos consultados, marca un punto de inflexión en la disciplina. El anuncio ha reabierto el debate sobre el papel futuro de los humanos en un campo que durante siglos ha
El kernel de Lean presentó un fallo de solidez (bug #14576) que fue detectado y corregido durante la semana del 27 de julio. El origen fue la publicación, el 25 de julio, de un repositorio con una aparente refutación de la conjetura de Collatz generada con ayuda de IA y sin "sorry", obra de Ramana K
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
El ingeniero Joshua Barretto propone en un ensayo que el lenguaje humano funciona como un espacio latente de alta entropía: una herramienta tecnológicamente moldeada durante milenios que facilita el razonamiento conceptual, del mismo modo que un sistema de tipos fuerte en lenguajes como Rust o Haske
Un investigador de UC Berkeley, Phillip Kerger, logró que el modelo GPT-5.6 Sol Pro de OpenAI generara en una sola sesión ininterrumpida de 148 minutos una demostración que cierra una brecha de complejidad en optimización convexa sin derivadas que llevaba abierta desde 1996. El resultado fue verific
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
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
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
Sostactic es una herramienta innovadora que extiende las capacidades de los sistemas de demostración de teoremas como Lean 4 para probar desigualdades polinómicas. Tradicionalmente, probar estas desigualdades en Lean ha sido limitado por tácticas como `nlinarith` y `positivity`. Sostactic supera est
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
Mistral AI ha lanzado Leanstral, la primera base de código open-source diseñada para agentes de codificación en Lean 4. Leanstral busca abordar una limitación clave en el desarrollo de IA: la necesidad de revisión humana exhaustiva en tareas de codificación de alto riesgo. El modelo, con 6 mil millo
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 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