software · 11 menciones
Ansatz es una librería de Clojure que permite escribir programas verificados formalmente sin salir del ecosistema de la JVM. Está construida sobre el Calculus of Inductive Constructions (CIC), la misma teoría de tipos que sustenta Lean 4, e implementa el núcleo de Lean 4 en Java. De este modo, las p
Talos es un intérprete de WebAssembly escrito en Lean 4 cuyo objetivo no es la velocidad de ejecución, sino servir como objeto formal sobre el que demostrar propiedades. La misma definición que ejecuta un programa Wasm es la que se emplea para razonar, lo que elimina la necesidad de mantener un inté
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
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
Un desarrollador ha creado una herramienta de línea de comandos (CLI) llamada 'korb' que permite automatizar los pedidos de comestibles de REWE a través de sus APIs. Escrita en Haskell, la herramienta está diseñada para ser utilizada por agentes o asistentes para organizar las compras de REWE, gener
Un investigador español, Francisco, ha desarrollado P2PCLAW, una red peer-to-peer innovadora que permite a agentes de inteligencia artificial y a investigadores compartir resultados científicos y validar afirmaciones a través de pruebas matemáticas formales. La plataforma, construida con GUN.js e IP
Este artículo técnico explora una peculiaridad en el sistema de tipos de Rust y cómo un intento de emular tipos de orden superior (HKTs) llevó a un error de desbordamiento en la evaluación de requisitos de traits, causando que el compilador fallara. El autor, en su intento de crear un lenguaje de sc
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
El auge de las redes neuronales en aplicaciones críticas, como sistemas de seguridad y control, ha revelado una brecha preocupante: la verificación y el análisis de estas redes a menudo se realizan *fuera* del entorno de programación donde se definen y ejecutan. Esta separación crea una desconexión