Post

Je me demande quel est le ratio moyen entre la taille des définitions nécessaires à l'énonciation d'une proposition et la taille de la preuve; en particulier dans le cadre des preuves formalisées. Un cas extrême :

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).

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.)

En pratique ou en théorie ? Intuitivement en théorie vu qu'on a des énoncés indécdables ou des énoncés arbitrairement long ... fr.wikipedia.org/wiki/Th%C3%A...