The main goal of the project is to:

Project workpackages:

• WP A) uniform representation and learning for TP
• WP B) ATP encoding components for different foundational aspects
• WP C) proof reconstruction and reverification, and
• WP D) knowledge reuse, content merging, and evaluations

Main results so far:

• CoqHammer: First Hammer for Type Theory

  Able to completely automatically prove half of the goals in the Coq standard library; helped a number of other projects.
  Try it out!

• HOL(y)Hammer and TacticToe

  Strong automation for HOL systems. Our systems are included in the HOL4 distribution!

• Tactician

  Tactic-based proof search for Coq. Try it out!

• Isabelle Enigma

  The experimental extension of Isabelle/Sledgehammer, lets you run it with [prover=remote_enigma], that can prove more than any other S/H prover!

Selected results for the workpackages:

• Representations for ITP learning (Work Package A)

  • More expressive graph neural networks IJCNN'20
  • Property invariant GNNs ECAI'20
  • Autoencoding first-order logic JLC'21
  • HOLStep dataset for inference usefulness ICLR'17
  • Grunge dataset of ATP problems CADE'19
  • Dataset for learning first-order properties GCAI'20
  • Characterization using SMT-Lib subsets SMT'21

• Superposition based automation (Work Package B)

  • Tensorflow integrated in E-prover LPAR'17
  • Enigma Prototype IJCAR'20
  • GNN for Superposition Tableaux'21c
  • Combining fast and slow prediction FroCos'21a
  • Weighted Path Order in theorem proving ICMS'18
  • Relaxed Weighted Path Order MCS'20

• Automation using Monte-Carlo Tableaux (Work Package B)

  • Monte Carlo Proof Search CADE'17
  • Reinforcement Learning for Tableaux NIPS'18
  • Combined Policy-Value learning JAR'19
  • Policy Optimization for long proofs Tableaux'21a
  • Certifying non-clausal tableaux Tableaux'19

• Internal Automation for Type Theory (Work Package C)

  • CoqHammer JAR'18
  • Trees in Tactician CICM'21
  • Bit-vectors in SMTCoq PxTP'19
  • Program verification with CoqHammer CICM'18

• Reverification of Mizar in Isabelle/Mizar (Work Package C)

  • Mizar object logic JAR'19
  • Mizar structures MACIS'17
  • Parts of the library FedCSis'17
  • Mizar-like syntax CICM'17
  • Auto-translate statements CICM'18
  • Import library part ITP'19a
  • Define a model of HOTG ITP'19b

• Evaluations of the methods in formalizations (Work Package D)

  • Isabelle: Formal Microeconomic Foundations CPP'18,
  • First Welfare Theorem in Isabelle AFP'17
  • Isabelle Linear Programming AFP'19
  • Isabelle Formalization of Von-Neumann-Morgenstern Theorem AFP'18
  • Isabelle Homotopy Theory ITP'21
  • Impure Programming Languages in Coq DMTCS'18
  • Coq: Category Theory FMM'18, MCS'20

• Knowledge Re-use by Concept merging (Workpackage D)

  • Syntactic alignments for formal corpora JAR'19
  • Classification of alignments CICM'17
  • Statistical parsing for Mizar SYNASC'17
  • Statistical parsing with deep trees ITP'17
  • First supervised neural translation CICM'18
  • Unsupervised neural translation CPP'20
  • Intermediate formalization languages CICM'20
  • Joint embedding of proof libraries FroCoS'21
  • Disambiguating Latex to sTeX ICLR'21
  • Formalizing geometric constructions from images ICMS'20
  • Solving geometric construction problems from images CICM'21

For all results see the publications list