La réalisation d'une preuve formelle dans un assistant à la preuve comme le système Coq comporte souvent une part de travail significative pour établir des résultats qui sont laissés implicites dans une preuve sur papier. Prouver la réalisation ou l'absurdité d'un jeu de contraintes (égalités/inégalités) polynomiales est un exemple représentatif de ce type de problèmes dont le contenu mathématique est faible mais dont le coût de la preuve formelle « à la main » peut s'avérer important.
Il est donc crucial pour la faisabilité de preuves variées et bien plus élaborées de fournir des outils d'automatisation adaptés pour décharger l'utilisateur de ce travail et lui permettre de se concentrer sur les étapes significatives de sa preuve. La terminaison de systèmes de réécriture, le théorème de répartition des nombres premiers ou la théorie des courbes elliptiques sont des exemples récents de telles applications.
De tels outils peuvent revêtir des formes très différentes. Il sera ici question en particulier du problème de décision efficace dans les structures d'anneaux et de la conception d'une procédure de décision certifiée pour l'arithmétique (ordonnée) réelle, basée sur l'algorithme de décomposition algébrique cylindrique de Collins.