Les humains prouvent des théorèmes en s'appuyant sur un raisonnement de haut niveau substantiel et des intuitions spécifiques au problème. Les assistants de preuve offrent une formalisation qui ressemble au raisonnement mathématique humain, représentant les théorèmes dans la logique d'ordre supérieur et les preuves sous forme de tactiques de haut niveau. Cependant, les experts humains doivent construire manuellement les preuves en entrant des tactiques dans l'assistant de preuve. Dans cet article, nous étudions le problème de l'utilisation de l'apprentissage automatique pour automatiser l'interaction avec les assistants de preuve. Nous avons créé CoqGym, un ensemble de données et un environnement d'apprentissage à grande échelle contenant 71 000 preuves écrites par des humains provenant de 123 projets développés avec l'assistant de preuve Coq. Nous avons développé ASTactic, un modèle basé sur l'apprentissage profond qui génère des tactiques sous forme de programmes structurés en arbres syntaxiques abstraits (ASTs) (abstract syntax trees). Les expériences montrent qu'ASTactic, formé sur CoqGym, peut générer des tactiques efficaces et être utilisé pour prouver de nouveaux théorèmes qui n'étaient pas précédemment démontrables par des méthodes automatisées. Le code est disponible à l'adresse https://github.com/princeton-vl/CoqGym.