私は、深層学習を用いて手動で構築された特徴量に頼らず、高階論理における自動定理証明システムを提案します。HolophrasmはMetamath言語の形式主義を活用し、ニューラルネットワーク強化バンディットアルゴリズムとシーケンス・ツー・シーケンスモデルを使用して部分証明木を探求します（action enumeration）。このシステムは、Metamathのset.mmモジュールからテスト定理の14％を証明しています。