Je présenterai d'abord un développement formel à propos des fondements de la géométrie. Celui-ci consiste en la formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie. Ensuite, je décrirai l'implantation en Coq d'une procédure de décision pour la géométrie affine plane: la méthode des aires de Chou, Gao et Zhang. Dans la troisième partie, nous nous intéresserons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof (http://home.gna.org/geoproof/). GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq. Enfin, je presenterai un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.