Ce sujet de thèse vise à automatiser la génération et la vérification des preuves par déchargement en théorie des graphes, en particulier en coloration. Cette technique de preuve est incontournable dans ce domaine et a conduit à des avancées majeures comme le théorème des quatre couleurs. Bien que puissante, cette méthode est traditionnellement laborieuse car elle a tendance à produire des disjonctions de cas longues et complexes. La thèse a deux objectifs: automatiser la recherche de règles de déchargement en les modélisant par des programmes linéaires, ainsi que le design et l'implémentation d'algorithmes de coloration efficaces pour traiter les nombreux cas générés.