Post

P := ∀ x y z n : ℕ, (x + 1)^(n + 3) + (y + 1)^(n + 3) ≠ (z + 1)^(n + 3) Le type P : Prop encode (en Lean) l'énoncé du grand théorème de Fermat, et le code qui vise à le démontrer (github.com/ImperialColl...) est déjà énorme (et c'est loin d'être fini).

Dans ce cas, si on veut s'assurer que je n'ai pas fait d'erreur d'énoncé, il suffit de relire P, ce qui est relativement simple. Mais prenez par exemple les résultats de calculabilité dans Mathlib, dont j'ai déjà parlé ici, ils supposent une formalisation des fonctions récursive, etc.

ce qui est relativement lourd. (D'ailleurs, je pose ici la question pour les mathématiques, mais c'est une question qui se pose aussi en informatique, si on veut démontrer des propriétés des programmes.)