Nous explorons l'application des modèles de langage basés sur les transformateurs à la démonstration automatique de théorèmes. Ce travail s'inscrit dans une perspective motivée par la possibilité que l'une des principales limitations des prouveurs automatiques par rapport aux humains — la génération de termes mathématiques originaux — puisse être atténuée grâce à la génération de contenus par des modèles de langage. Nous présentons un prouveur automatisé et un assistant de preuve, appelé GPT-f, conçu pour le langage formel Metamath, et analysons ses performances. GPT-f a découvert de nouvelles preuves courtes qui ont été acceptées dans la bibliothèque principale de Metamath, ce qui, à notre connaissance, constitue la première fois qu'un système fondé sur l'apprentissage profond contribue à des preuves adoptées par une communauté mathématique formelle.