Je propose un système d'Automatisation de la Démonstration de Théorèmes en logique d'ordre supérieur utilisant l'apprentissage profond et évitant les caractéristiques construites manuellement. Holophrasm exploite le formalisme du langage Metamath et explore des arbres de preuve partiels à l'aide d'un algorithme de bandit augmenté par un réseau neuronal et d'un modèle séquence-à-séquence pour l'énumération des actions. Le système démontre 14 % des théorèmes de test issus du module set.mm de Metamath.