La théorie de la démonstration est issue d'une histoire courte et tumultueuse, construite en marge des mathématiques traditionnelles. Aussi, son langage reste souvent idiosyncratique : calcul des séquents, élimination des coupures, propriété de la sous-formule, etc. Dans cet article, nous avons voulu guider le lecteur à travers la thématique, en lui traçant un chemin progressif et raisonné, qui part des mécanismes symboliques de l'élimination des coupures, pour aboutir à leur transcription algébrique en diagrammes de cohérence dans les catégories monoïdales. Cette promenade spirituelle au point de convergence de l'algèbre et de la linguistique est ardue parfois, mais aussi pleine d'attraits : car à ce jour, aucune langue (formelle ou informelle) n'a été autant étudiée par les mathématiciens que la langue des démonstrations logiques.