Nuestro agente de demostración de Aleph acaba de alcanzar el puesto #1 en PutnamBench, un referente basado en problemas de Putnam —una de las olimpiadas de matemáticas universitarias más difíciles— totalmente formalizado con demostraciones verificadas por máquina y sin intervención humana. Los problemas de Putnam suelen considerarse más difíciles que los problemas de la IMO y abarcan una amplia gama de temas, incluyendo cálculo, teoría de números, teoría de grupos y otras áreas fundamentales de las matemáticas. Esta es una prueba sólida de que la IA puede manejar razonamientos profundos y de varios pasos con garantías de corrección — el mismo tipo de tecnología que usamos para verificar descubrimientos reales de software, hardware y científicos que requieren lógica formal.