El artículo «Claude can (sometimes) prove it» comenta que Claude Code, el agente de IA de Anthropic, posee una capacidad sorprendente para la demostración interactiva de teoremas (ITP) en Lean, un campo reservado hasta ahora a expertos. Aunque no es totalmente autónomo y requiere supervisión humana para actuar como "gestor del proyecto", el agente puede descomponer tareas complejas, escribir definiciones, generar pruebas y refactorizar código. Su eficacia reside en la retroalimentación estricta de Lean, que le permite iterar y corregir errores. Pese a su lentitud y a algunos fallos conceptuales, supone un avance radical: acerca la verificación formal, antes prohibitiva por su complejidad, a un futuro donde podría ser accesible y automatizada.