Les modèles internes d'OpenAI et d'Anthropic ont réfuté presque simultanément l'hypothèse du temps exponentiel (ETH). Depuis la fin des années 1990, on pense que tester si une formule logique avec n variables peut être vraie dans le pire des cas ne peut pas être effectué plus rapidement que le temps exponentiel jusqu'à n. OpenAI a publié une première version avec un algorithme plus rapide que celui trouvé par son modèle. Un jour plus tard, Anthropite a publié un résultat similaire du modèle Claude, et la preuve formelle dans Lean 4 a également été écrite par le modèle, et le programme la vérifie. Il s'avère que les modèles trouvent déjà de nouveaux algorithmes dont l'hypothèse est retenue depuis plus de 25 ans et apportent la preuve à la vérification automatique, il n'est donc pas nécessaire de les croire sur parole. Comme l'écrit Anthropit, le résultat ne dit rien sur la résolution réelle des formules. OpenAI a écrit début octobre qu'il se préparait à publier le modèle derrière ce référentiel, je m'attends donc également à de telles fonctionnalités dans l'API publique.