Resolver cada problema en uno de los benchmarks más exigentes de las matemáticas suele costar decenas de miles de dólares. NEAR AI lo hizo por solo $111.
El 6 de septiembre de 2026, Alex Skidanov, cofundador de NEAR Protocol, anunció que el agente de código abierto Lean del proyecto había resuelto los 672 problemas del benchmark PutnamBench, un conjunto derivado de la Competencia Matemática William Lowell Putnam. La factura total: $111. La segunda propuesta más económica conocida costó 250 veces más.
Qué es realmente PutnamBench y por qué importa
La competencia Putnam es el concurso de matemáticas universitarias más prestigioso de América del Norte. Obtener una puntuación de cero no es inusual, ni siquiera entre estudiantes brillantes. El examen está diseñado para derrotarte.
PutnamBench, introducido en 2024, toma esa tradición de dificultad y la convierte en un conjunto formal de evaluación para demostradores automáticos de teoremas de IA. El benchmark contiene 672 problemas codificados en Lean 4, un lenguaje de asistente de pruebas que requiere que los argumentos matemáticos se escriban con precisión verificable por máquina. Una prueba lógicamente poco rigurosa se rechaza por completo, sin puntos parciales.
Antes del resultado de NEAR AI, los agentes que intentaban PutnamBench necesitaban frecuentemente miles de llamadas de inferencia por problema. Los costos de cómputo se acumulaban rápidamente, colocando las ejecuciones completas del benchmark en un rango de $10,000 a $25,000 en gastos totales para los sistemas líderes.
El agente Lean de NEAR AI completó todo el conjunto de 672 problemas por $111.
Por qué la brecha de costos es la historia real
Con un costo de $10,000 a $25,000 por ejecución completa, solo un pequeño número de organizaciones podían permitirse iterar, experimentar y mejorar sus pipelines de demostración de teoremas. Con $111, ese cálculo se invierte por completo.
El rápido avance en los resultados de PutnamBench entre 2025 y 2026 ya estaba impulsado por flujos de trabajo agentes que combinan modelos de lenguaje grandes con el motor de verificación de pruebas de Lean. El enfoque de NEAR AI extiende ese patrón, pero añade una capa de eficiencia que la comunidad de benchmark no había visto antes.
NEAR AI ha situado este logro dentro de una visión de infraestructura más amplia centrada en lo que llama IronClaw, un marco orientado hacia la inteligencia artificial confidencial y verificable. La capacidad de verificación formal encaja directamente en este enfoque: si puedes demostrar que un argumento matemático es correcto a nivel de máquina, tienes una base para sistemas de IA cuyas salidas pueden ser auditadas de forma independiente en lugar de confiarse en la fe.
La decisión de NEAR Protocol de hacer abierto el agente Lean aumenta aún más su importancia. Las herramientas propietarias que ofrecen una ventaja de costo de 250x tienden a mantenerse propietarias. Hacer abierto el agente significa que la metodología está disponible para su inspección, extensión y uso por cualquiera.