14 noticias
Jane Street, firma de trading cuantitativo, ha anunciado la creación de un equipo interno dedicado a los métodos formales, una disciplina que la compañía había descartado durante 25 años por sus costes prohibitivos. El cambio de postura se debe al auge de la programación agéntica, que modifica tanto
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