Palomar: el registro de pruebas Lean verificadas por IA

Un registro para las pruebas matemáticas verificadas por IA

Terry Tao, uno de los matemáticos más influyentes del mundo, anunció el pasado 18 de agosto la apertura del Palomar registry, un nuevo registro público para pruebas formales escritas en Lean — el lenguaje de verificación matemática que se ha convertido en el estándar de facto para demostrar resultados con precisión computacional. Lo interesante no es solo que exista, sino que llega en un momento donde la frontera entre demostraciones humanas y generadas por inteligencia artificial se ha vuelto casi indistinguible.

El registro, incubado por el Lean FRO (Fundación Lean) y ICARM, permite someter repositorios de GitHub completos a dos verificaciones automáticas: una mecánica con la herramienta Comparator y otra semántica asistida por un modelo de lenguaje grande. Si pasan ambas, la prueba queda registrada. No es una revista revisada por pares, pero establece un estándar mínimo de trazabilidad que antes no existía.

¿Qué problema resuelve Palomar?

La proliferación de demostraciones generadas por IA ha creado un problema práctico: verificar que un repositorio de Lean realmente demuestra lo que dice es más complejo de lo que parece. Necesitas confirmar que el código compila, que no contiene atajos como axiomas adicionales, y que la descripción informal coincide semánticamente con el resultado formalizado.

Palomar aborda esto con tres componentes obligatorios en cada submission:

• Un "challenge file" con una descripción legible en Lean del resultado reclamado
• Un "solution module" con la demostración completa
• Un archivo formalization.yaml con metadata, descripciones informales y disclosures relevantes

Si un snapshot pasa ambos checks, queda registrado con un identificador único (ejemplo: PALOMAR-2026-08-13-000001). El proceso fue testeado exitosamente por Tao mismo con su formalización de la conjetura de Sendov, y ya hay discusiones activas en el canal de Zulip dedicado al proyecto.

El contexto: cuando la IA empieza a hacer matemáticas de investigación

Lo que hace relevante a Palomar va más allá del nicho académico. En los últimos meses, el ecosistema ha visto un aumento significativo de sistemas de IA produciendo demostraciones formales en Lean que alcanzan niveles de investigación real:

En agosto de 2026, Axiom Math anunció que su sistema AxiomProver había generado una demostración verificable en Lean 4 del teorema de las brechas de primos 246 — el resultado más avanzado conocido sobre la conjetura de los primos gemelos. El trabajo involucró a 41 contribuyentes nominales y creó PrimeGapsLib, una biblioteca pública de Lean que formaliza tanto el límite de 246 como el anterior de 600 de James Maynard. Según Ken Ono, matemático fundador de Axiom Math, "este teorema representa actualmente el umbral del conocimiento humano sobre números primos".

Más relevante aún para founders de startups: en junio de 2026, Pramaana Labs cerró una ronda seed de USD 27 millones liderada por Khosla Ventures (con participación de Accel, BoldCap, Nexus Venture Partners, Premji Invest y Unbound) precisamente para aplicar herramientas de verificación formal basadas en Lean a sistemas de IA en sectores críticos como derecho, descubrimiento de fármacos y preparación fiscal. Su CEO, Ranjan Rajagopalan, describe el enfoque como combinar un LLM convencional con una capa determinista sobre él: "Cada dominio donde equivocarse puede costarle a alguien su salud, dinero o libertad tiene reglas. Esas reglas necesitan ser codificadas".

¿Qué significa esto para tu startup?

Si tu empresa construye productos donde la corrección importa — desde algoritmos financieros hasta sistemas de diagnóstico médico o infraestructura crítica — Palomar y el movimiento de verificación formal representan dos señales importantes:

1. La verificación automática de código generado por IA deja de ser experimental.

El pipeline de Axiom Math (blueprint → AxiomProver genera código Lean → revisión humana → biblioteca reutilizable) muestra que la formalización ya no es solo para académicos. Las empresas pueden empezar a usar estas herramientas para verificar propiedades de software crítico. Como señala Ono: "El mundo está a punto de ejecutarse sobre código que nadie leyó. La formalización de pruebas es un banco de pruebas para resolver el desafío más importante que enfrentaremos con la IA".

2. Hay capital institucional apostando fuerte a este espacio.

Los USD 27 millones de Pramaana Labs no son una apuesta pequeña ni marginal. Indica que los inversores ven la verificación formal como un diferenciador competitivo real, especialmente en verticales reguladas donde los errores tienen consecuencias legales y financieras directas.

Acciones concretas que puedes implementar ahora:

• Evalúa si tu producto tiene componentes verificables formalmente. Si tienes lógica de negocio compleja con reglas codificadas (como el código tributario que menciona Rajagopalan), considera si vale la pena formalizarlas en Lean u otro sistema de verificación antes de escalar.
• Monitorea el ecosistema de verificación formal. Proyectos como PrimeGapsLib de Axiom Math demuestran que las bibliotecas de verificación se están volviendo reutilizables — no son ejercicios aislados. Esto significa que podrías aprovechar work previo en lugar de empezar desde cero.
• Considera la trazabilidad como ventaja competitiva. En un mercado saturado de claims sobre IA, tener demostraciones verificables de corrección (como las que Palomar estandariza) puede ser un diferenciador tangible para clientes enterprise que exigen garantías de precisión.

La línea entre novedad y calidad

Es importante entender qué NO es Palomar. Tao enfatiza que los checks automatizados "no llegan a lo que daría una revisión por pares adecuada de novedad, interés y precisión". El registro valida que la demostración existe y que coincide con la descripción, pero no juzga si el resultado es importante o correcto en profundidad. Es un primer filtro, no un sello de aprobación definitiva.

Esto tiene implicaciones prácticas: cualquier startup que considere usar verificación formal debe entender que la automatización reduce el costo de verificación, pero no elimina la necesidad de expertise humano en el diseño de las especificaciones y la interpretación de los resultados.

Fuentes

• Palomar: A registry of Lean verified mathematics
• Axiom Math's AI Verifies the 246 Prime-Gaps Theorem in Lean
• Pramaana Labs raises $27M seed round from Khosla Ventures to bring formal verification to AI