Les preuves informatiques de grande envergure comprennent des millions d'étapes logiques intermédiaires. La majorité écrasante de ces étapes proviennent d'heuristiques sélectionnées et guidées manuellement, appliquées aux objectifs intermédiaires. Jusqu'à présent, l'apprentissage automatique n'a généralement pas été utilisé pour filtrer ou générer ces étapes. Dans cet article, nous introduisons un nouveau jeu de données basé sur des preuves en Logique d'Ordre Supérieur (HOL), dans le but de développer de nouvelles stratégies de démonstration de théorèmes fondées sur l'apprentissage automatique. Nous mettons ce jeu de données à disposition du public sous licence BSD. Nous proposons diverses tâches d'apprentissage automatique qui peuvent être réalisées à partir de ce jeu de données, et discutons de leur importance pour la démonstration de théorèmes. Nous évaluons également un ensemble de modèles d'apprentissage automatique simples servant de référence pour ces tâches (y compris la régression logistique, les réseaux neuronaux convolutifs et les réseaux neuronaux récurrents). Les résultats obtenus avec nos modèles de référence montrent le potentiel prometteur d'appliquer l'apprentissage automatique à la démonstration de théorèmes en logique d'ordre supérieur (HOL).