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

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

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