Là, j'étais dans un dossier vide, vibe a créé un nouveau projet Lean avec une dépendance sur Mathlib, puis a mouliné pendant une bonne dizaine de minutes et fini par me produire une formalisation (énoncé et preuve) du résultat. (La preuve est proche de celle du problème de l'arrêt.)

2 likes 1 replies