Les preuves combinatoires sont-elles de vraies preuves ?

Cyrano

Bonjour,

Quand on cherche à démontrer certaines identités impliquant des combinaisons et des factorielles, il est parfois considéré comme "plus élégant" d'utiliser la technique du double comptage. 

Prenons par exemple ce fil ouvert sur mathstackexchange. On cherche à y prouver l'identité : $$\sum_{k=0}^n \binom{2k}{k}\binom{2(n-k)}{n-k}=2^{2n}.$$ Ceci peut se prouver de façon totalement formelle, par exemple via l'usage de séries génératrices ou encore en faisant une récurrence particulièrement lourde, exploitant les propriétés du triangle de Pascal. Cependant, on peut aussi imaginer une situation combinatoire où le "comptage" peut s'effectuer de deux façons différentes, chaque façon correspondant à des membres de l'égalité qu'on veut prouver. Par exemple, pour l'égalité sus-mentionnée, on peut s'amuser à compter certains chemins sur un quadrillage où les sommets sont à coordonnées entières. 

Ma question est la suivante : est-ce que les preuves dites "combinatoires" sont des véritables preuves au sens de l'informatique théorique et des vérificateurs de preuve ? Ces preuves s'apparentent souvent à des textes écrits en français, et qui sont particulièrement convaincants, mais je suis dubitatif sur leur statut au niveau purement formel.

Magnéthorax

Je n'ai aucune idée de ce qu'on appelle une véritable preuve au sens de l'informatique. Faire une preuve combinatoire consiste à montrer l'existence  d'une bijection, souvent entre un ensemble que l'on cherche à dénombrer et un ensemble que l'on sait dénombrer. Comme dans d'autres domaines, le style "littéraire" permet de gagner du temps.

Foys

Je plussoie @Magnéthorax ; en réalité la prose des preuves dites combinatoires consiste (en supposant qu'on formalise les maths en théorie des ensembles; les prouveurs communs comme COQ ne le font pas et la manipulation de ce genre d'objet devient réellement pénible, dans mon expérience en tout cas; de façon générale l'écriture de preuves dans ce genre de logiciel est une corvée) à décrire des bijections entre l'ensemble visé et un autre ensemble dont le cardinal est connu. Des phrases comme "on a vérifié que chaque objet est compté exactement une seule fois" ne signifient rien d'autre que le fait que la fonction employée est bijective et qu'on l'a prouvé.

On se sert aussi de ce que pour tout ensemble fini $X$ et toute partiton $(X_j)_{j\in J}$ de $X$, on a $\text{card} (X) = \sum_{j\in J} \text{card} (X_j)$. Avec ça on s'en sort.