JUSTO AHORA: Un análisis revela que Putnam es 4 veces más fácil / requiere mucho menos razonamiento que el IMO. La longitud promedio de la prueba de Aristotle Lean4 para los 10 problemas resueltos de Putnam fue de ~250 líneas, en comparación con ~1000 para el IMO, una reducción del 75%. Estamos explorando la aplicación de computación extendida a los otros dos (A5 y B4), para cuantificar más precisamente la dificultad relativa. Algunas advertencias: ha habido mejoras en el modelo / algorítmicas desde el resultado de nivel de medalla de oro de Aristotle en el IMO, pero también la versión para consumidores disponible al público es mucho más débil que la que se utilizó internamente para resolver los problemas del IMO. Como aficionados a Putnam, incluso nosotros debemos admitir — el IMO sigue siendo el rey. 👑