# The main goal of the project is to:

### develop a strong and uniform learning-reasoning system

available for multiple logical foundations

# 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)

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

### 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