Le théorème d'élimination des coupures (ou Hauptsatz de Gentzen) a été prouvé par Gerhard Gentzen en 1934 dans son article « Investigations in Logical Deduction » pour les systèmes formalisant les logiques intuitionniste et classique. Il dit que si l'on peut prouver une déclaration dans le calcul des séquents en faisant usage de la règle de coupure, alors cette déclaration possède aussi une preuve sans coupure.
Ce théorème fut toutefois impuissant à sauver le peintre Mark Rothko — qui l'ignorait sans doute. Devenu hypochondriaque, et n'en pouvant plus d'être classé parmi les représentants de l'expressionnisme abstrait américain, catégorisation qu'il jugeait « aliénante », Rothko se suicide début 1970 à New York.
Le 25 février, son assistant trouve le peintre dans sa cuisine, allongé, mort, couvert de sang, devant l'évier. Il s'était tailladé les bras au-dessus de l'articulation des coudes avec un rasoir !
(Włodzisław Szczur, Mathématique du néant)
