En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.

Sommaire

• Vérifier des programmes
• Vérifier des démonstrations mathématiques
• Brouwer-Heyting-Kolmogorov
• Curry-Howard
• Quantificateurs et types dépendants
• Logique intuitionniste
• Quelques exemples
• Quelques succès de la formalisation
• La recherche en théorie des types
• Conclusion

Vérifier des programmes

Comme nous sommes sur LinuxFr.org, je devrais peut-être commencer par ceci : nous passons énormément de temps à découvrir des bugs, et pour les personnes du développement logiciel, à les comprendre, à les résoudre, et de préférence à les éviter en écrivant des tests.

Dans une formation universitaire de base en informatique, on rencontre des algorithmes, mais aussi des méthodes pour prouver que ces algorithmes terminent et répondent bien au problème posé. Les premières introduites sont typiquement les variants de boucle (montrer qu’une certaine valeur décroît à chaque itération, ce qui assure que le programme termine si elle ne peut pas décroître à l’infini), et les invariants de boucle (montrer qu’une certaine propriété vraie au début d’une boucle est préservée entre deux itérations, ce qui assure qu’elle reste encore vraie à la fin de la boucle).

On a donc, d’une part, un algorithme, implémentable sur machine, d’autre part une preuve, sur papier, que l’algorithme est correct. Mais si l’implémentation a une erreur par rapport à l’algorithme sur papier ? Et puisque nous n’arrêtons pas de nous tromper dans nos programmes, il est fort possible que nous nous trompions dans notre preuve (qui n’a jamais oublié qu’il fallait faire quelque chose de spécial dans le cas <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNzA1LjI3NzQ4OTAwMjU0MSAyMjU1LjU1NTU1NTU1%0ANTU1NTcgNzQ4LjU1NDk3ODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogNS4xODFl%0AeDsgaGVpZ2h0OiAxLjY4N2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMjQxZXg7%0AIG1hcmdpbjogMXB4IDBweDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJo%0AdHRwOi8vd3d3LnczLm9yZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhf%0AU1ZHX2dseXBocyI+PHBhdGggaWQ9IlNUSVhXRUJNQUlOSS02RSIgc3Ryb2tl%0ALXdpZHRoPSIxMCIgZD0iTTQ2MCAxMTdsMTQgLTEzYy02OCAtOTMgLTkzIC0x%0AMTMgLTE0MCAtMTEzYy0yNSAwIC00NyAxNiAtNDcgNTRjMCAxMCAyIDIzIDE2%0AIDc1bDQ0IDE2MmM4IDMxIDE0IDY3IDE0IDc5YzAgMTggLTkgMjkgLTI0IDI5%0AYy00MCAwIC04NSAtNDkgLTE0OCAtMTQyYy00NSAtNjcgLTUzIC05MCAtMTAw%0AIC0yNDhoLTc1bDk2IDM1MGMxIDUgMiAxMSAyIDE3YzAgMjAgLTE0IDI2IC02%0ANSAyN3YxNmM4MSAxNiAxMDkgMjAgMTYyIDMxbDQgLTJsLTY3IC0yMTggYzEw%0AMCAxNjAgMTY3IDIyMCAyMzEgMjIwYzQzIDAgNjUgLTI1IDY1IC02MWMwIC0x%0AOCAtNCAtMzkgLTEwIC02MGwtNTYgLTIwM2MtMTAgLTM2IC0xNCAtNTMgLTE0%0AIC02MWMwIC05IDQgLTE4IDE2IC0xOGMxNCAwIDMyIDE2IDYxIDUzYzcgOCAx%0ANCAxNyAyMSAyNloiPjwvcGF0aD48cGF0aCBpZD0iU1RJWFdFQk1BSU4tM0Qi%0AIHN0cm9rZS13aWR0aD0iMTAiIGQ9Ik02MzcgMzIwaC01ODl2NjZoNTg5di02%0ANnpNNjM3IDEyMGgtNTg5djY2aDU4OXYtNjZaIj48L3BhdGg+PHBhdGggaWQ9%0AIlNUSVhXRUJNQUlOLTMwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJNNDc2IDMz%0AMGMwIC0xNzIgLTYzIC0zNDQgLTIyNiAtMzQ0Yy0xNzEgMCAtMjI2IDE4NiAt%0AMjI2IDM1MGMwIDE3NyA2OSAzNDAgMjMwIDM0MGMxMzEgMCAyMjIgLTE0MSAy%0AMjIgLTM0NnpNMzgwIDMyNWMwIDIwOCAtNDQgMzI1IC0xMzIgMzI1Yy04MyAw%0AIC0xMjggLTExOCAtMTI4IC0zMjFzNDQgLTMxNyAxMzAgLTMxN2M4NSAwIDEz%0AMCAxMTUgMTMwIDMxM1oiPjwvcGF0aD48L2RlZnM+PGcgc3Ryb2tlPSJibGFj%0AayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0iMCIgdHJhbnNmb3JtPSJt%0AYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGluazpocmVmPSIjU1RJWFdF%0AQk1BSU5JLTZFIj48L3VzZT48dXNlIHhsaW5rOmhyZWY9IiNTVElYV0VCTUFJ%0ATi0zRCIgeD0iNzgyIiB5PSIwIj48L3VzZT48dXNlIHhsaW5rOmhyZWY9IiNT%0AVElYV0VCTUFJTi0zMCIgeD0iMTc1MCIgeT0iMCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="n = 0"> ?).

En tant que programmeurs, on peut imaginer une approche où non seulement l’algorithme est implémenté, mais sa preuve de terminaison et de correction est aussi « implémentée », c’est-à-dire encodée dans un langage qui ressemble à un langage de programmation, pour être ensuite non pas interprétée ou compilée mais vérifiée.

La vérification est un très vaste domaine de l’informatique, dont je ne suis pas spécialiste du tout, et dans lequel il existe énormément d’approches : la logique de Hoare (voir par exemple l’outil why3), qui est essentiellement un raffinement des variants et invariants de boucle, la logique de séparation spécialement conçue pour raisonner sur la mémoire mutable (voir Iris), le model checking qui se concentre sur des programmes d’une forme particulièrement simple (typiquement des systèmes de transition finis) pour en vérifier des propriétés de façon complètement automatisée, etc.

Dans cette dépêche, je vais parler d’une approche avec quelques caractéristiques particulières :

• On vérifie des programmes purement fonctionnels (pas d’effets de bord, même si on peut les simuler).

• Le même langage mélange à la fois les programmes et leurs preuves.

• Plus précisément, le langage ne fait pas (ou peu) de distinction entre les programmes et les preuves.

Vérifier des démonstrations mathématiques

Pour se convaincre de l’ampleur que les démonstrations ont prise dans les mathématiques contemporaines, il suffit d’aller jeter un œil, par exemple, au projet Stacks : un livre de référence sur la géométrie algébrique, écrit collaborativement sur les 20 dernières années, dont l’intégrale totalise plus de 7500 pages très techniques. Ou bien la démonstration du théorème de classification des groupes finis simples : la combinaison de résultats répartis dans les dizaines de milliers de pages de centaines d’articles, et une preuve « simplifiée » toujours en train d’être écrite et qui devrait faire plus de 5000 pages. Ou bien le théorème de Robertson-Seymour, monument de la théorie des graphes aux nombreuses applications algorithmiques : 20 articles publiés sur 20 ans, 400 pages en tout. Ou bien, tout simplement, le nombre de références dans la bibliographie de la moindre thèse ou d’articles publiés récemment sur arXiv.

Inévitablement, beaucoup de ces démonstrations contiennent des erreurs. Parfois découvertes, parfois beaucoup plus tard. Un exemple assez célèbre est celui d’un théorème, qui aurait été très important s’il avait été vrai, publié en 1989 par Vladimir Voedvodsky, un célèbre mathématicien dont je vais être amené à reparler plus bas, avec Mikhail Kapranov. Comme raconté par Voedvodsky lui-même, un contre-exemple a été proposé par Carlos Simpson en 1998, mais jusqu’en 2013, Voedvodsky lui-même n’était pas sûr duquel était faux entre sa preuve et le contre-exemple !

Il y a aussi, souvent, des « trous », qui ne mettent pas tant en danger la démonstration mais restent gênants : par exemple, « il est clair que la méthode classique de compactification des espaces Lindelöf s’applique aussi aux espaces quasi-Lindelöf », quand l’auteur pense évident qu’un argument existant s’adapte au cas dont il a besoin mais que ce serait trop de travail de le rédiger entièrement. Donc, assez naturellement, un but possible de la formalisation des maths est de produire des démonstrations qui soient certifiées sans erreur (et sans trou).

Mais c’est loin d’être le seul argument. On peut espérer d’autres avantages, qui pour l’instant restent de la science-fiction, mais après tout ce n’est que le début : par exemple, on peut imaginer que des collaborations à grande échelle entre beaucoup de mathématiciens deviennent possibles, grâce au fait qu’il est beaucoup plus facile de réutiliser le travail partiel de quelqu’un d’autre s’il est formalisé que s’il est donné sous formes d’ébauches informelles pas complètement rédigées.

Brouwer-Heyting-Kolmogorov

Parmi les assistants de preuve existants, la plupart (mais pas tous) se fondent sur une famille de systèmes logiques rangés dans la famille des « théories des types ». L’une des raisons pour lesquelles ces systèmes sont assez naturels pour être utilisés en pratique est qu’en théorie des types, les preuves et les programmes deviennent entièrement confondus ou presque, ce qui rend facile le mélange entre les deux.

Mais comment est-ce qu’un programme devient une preuve, au juste ? L’idée de base est appelée interprétation de Brouwer-Heyting-Kolomogorov et veut que les preuves mathématiques se comprennent de la façon suivante :

• Le moyen de base pour prouver une proposition de la forme « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> » est de fournir d’une part une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">. En d’autres mots, une preuve de « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> » rassemble en un même objet une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">. Mais en termes informatiques, ceci signifie qu’une preuve de « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> » est une paire d’une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et d’une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">.

• De même, pour prouver « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> ou <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> », on peut prouver <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P">, ou on peut prouver <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">. Informatiquement, une preuve de « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> ou <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> » va être une union disjointe : une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> ou une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">, avec un bit pour savoir dans quel cas on est.

• Pour prouver « Vrai », il suffit de dire « c’est vrai » : on a une unique preuve de « Vrai ».

• On ne doit pas pouvoir prouver « Faux », donc une preuve de « Faux » n’existe pas.

• Et le plus intéressant : pour prouver « si <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> alors <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> », on suppose temporairement <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et on en déduit <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">. Informatiquement, ceci doit devenir une fonction qui prend une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et renvoie une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">.

Curry-Howard

L’interprétation de Brouwer-Heyting-Kolmogorov est informelle, et il existe plusieurs manières de la rendre formelle. Par exemple, on peut interpréter tout ceci par des programmes dans un langage complètement non-typé, ce qui s’appelle la réalisabilité.

Mais en théorie des types, on prend plutôt un langage statiquement typé pour suivre l’idée suivante : si une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> est une paire d’une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et d’une preuve de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q">, alors le type des paires de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> peut se comprendre comme le type des preuves de « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> ». On peut faire de même avec les autres types de preuves, et ceci s’appelle la correspondance de Curry-Howard. Autrement dit, là où Brouwer-Heyting-Kolmogorov est une correspondance entre les preuves et les programmes, Curry-Howard est un raffinement qui met aussi en correspondance les propositions logiques avec les types du langage, et la vérification des preuves se confond entièrement avec le type checking.

Sur les cas que j’ai donnés, la correspondance de Curry-Howard donne :

• La proposition « <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoMSAwIDAgLTEgMCAwKSI+PHVzZSB4bGlu%0AazpocmVmPSIjU1RJWFdFQk1BSU5JLTUxIj48L3VzZT48L2c+PC9zdmc+%0A" alt="Q"> » est le type des paires d’un élément de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjgyLjI3NzQ4OTAwMjU0MSA2MTYgNzExLjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS40NDZleDsgaGVpZ2h0OiAxLjY4%0AN2V4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuMTJleDsgbWFyZ2luOiAxcHggMHB4%0AOyBwb3NpdGlvbjogc3RhdGljOyIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3Jn%0ALzIwMDAvc3ZnIj48ZGVmcyBpZD0iTWF0aEpheF9TVkdfZ2x5cGhzIj48cGF0%0AaCBpZD0iU1RJWFdFQk1BSU5JLTUwIiBzdHJva2Utd2lkdGg9IjEwIiBkPSJN%0AMTQ2IDY1M2gyNDFjMTQ3IDAgMjE4IC01MiAyMTggLTE0OGMwIC01NCAtMjcg%0ALTEwOSAtNjggLTE0M2MtNDYgLTM4IC0xMTYgLTU3IC0yMDUgLTU3Yy00MiAw%0AIC02NCAyIC05MCA4bC01MyAtMTkzYy03IC0yNyAtMTQgLTQ4IC0xNCAtNjNj%0AMCAtMjMgMTUgLTM1IDY5IC00MXYtMTZoLTI0NHYxNmM1NyA4IDY2IDE3IDg0%0AIDgybDExNiA0MTRjMTMgNDcgMTcgNjggMTcgODNjMCAyNyAtMTQgMzUgLTcx%0AIDQydjE2ek0zMjAgNTkybC02OSAtMjQ1IGMyOSAtNSAzNCAtNSA1MiAtNWM2%0AMiAwIDk3IDYgMTI4IDI0YzQ0IDI1IDcxIDY5IDcxIDEzNGMwIDg5IC00OCAx%0AMjMgLTEzMCAxMjNjLTI4IDAgLTQ2IC04IC01MiAtMzFaIj48L3BhdGg+PC9k%0AZWZzPjxnIHN0cm9rZT0iYmxhY2siIGZpbGw9ImJsYWNrIiBzdHJva2Utd2lk%0AdGg9IjAiIHRyYW5zZm9ybT0ibWF0cml4KDEgMCAwIC0xIDAgMCkiPjx1c2Ug%0AeGxpbms6aHJlZj0iI1NUSVhXRUJNQUlOSS01MCI+PC91c2U+PC9nPjwvc3Zn%0APg==%0A" alt="P"> et d’un élément de <img style="display: inline; max-height: 1em;" class="mathjax" src="data:image/svg+xml;base64,PHN2ZyB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGlu%0AayIgdmlld0JveD0iMCAtNjk1LjI3NzQ4OTAwMjU0MSA3MjcgOTA2LjU1NDk3%0AODAwNTA4MTgiIHN0eWxlPSJ3aWR0aDogMS42ODdleDsgaGVpZ2h0OiAyLjA0%0AOGV4OyB2ZXJ0aWNhbC1hbGlnbjogLTAuNjAyZXg7IG1hcmdpbjogMXB4IDBw%0AeDsgcG9zaXRpb246IHN0YXRpYzsiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9y%0AZy8yMDAwL3N2ZyI+PGRlZnMgaWQ9Ik1hdGhKYXhfU1ZHX2dseXBocyI+PHBh%0AdGggaWQ9IlNUSVhXRUJNQUlOSS01MSIgc3Ryb2tlLXdpZHRoPSIxMCIgZD0i%0ATTY5IC0xNjlsLTEwIDE2Yzc3IDU0IDg2IDYxIDE3NyAxNDFjLTExNCAyMyAt%0AMTc2IDEwOCAtMTc2IDIzN2MwIDEyMyA2NCAyNTMgMTczIDM0N2M3NyA2NSAx%0ANjUgOTQgMjQxIDk0YzEzNyAwIDIyNSAtMTAyIDIyNSAtMjM3YzAgLTE1NiAt%0AMTA0IC0zMjIgLTI1NiAtNDAyYy01NCAtMjkgLTg5IC0zOCAtMTY0IC00M2wt%0ANTQgLTU3aDI1YzM0IDAgNzkgLTEwIDEyMyAtMjBjNDEgLTEwIDc4IC0yMSAx%0AMTEgLTIxYzcyIDAgMTEyIDE5IDE2OCA3NyBsMTYgLTExYy0xNSAtMjEgLTMy%0AIC00MSAtNTIgLTU5Yy01MCAtNDUgLTExNCAtNzUgLTE5MSAtNzVjLTM4IDAg%0ALTkxIDggLTE0OCAyNmMtNDMgMTQgLTczIDE4IC05MyAxOGMtNDAgMCAtNzcg%0ALTEwIC0xMTUgLTMxek01OTQgNDgwYzAgOTUgLTQ5IDE1MyAtMTI5IDE1M2Mt%0ANzUgMCAtMTM3IC00MCAtMTk0IC0xMjVjLTU4IC04NyAtMTA2IC0yMjUgLTEw%0ANiAtMzI1YzAgLTEwMSA1MCAtMTY2IDEyNCAtMTY2Yzc1IDAgMTQyIDQxIDE5%0AOCAxMjQgYzYyIDkzIDEwNyAyMzYgMTA3IDMzOVoiPjwvcGF0aD48L2RlZnM+%0APGcgc3Ryb2tlPSJibGFjayIgZmlsbD0iYmxhY2siIHN0cm9rZS13aWR0aD0i%0AMCIgdHJhbnNmb3JtPSJtYXRyaXgoM