# The main goal of the project is to:

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

available for multiple logical foundations

# Project workpackages and tasks:

- (A) uniform learning methods
- (B) reusable ATP encoding components for different foundational aspects
- (C) integration of proof reconstruction, and
- (D) methods for knowledge extraction, reuse and content merging

# Main results so far:

### CoqHammer: First Hammer for Type Theory

It is already able to completely automatically prove half of the goals in the Coq standard library and has 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

Try it out!# Various results categorised:

### WP A: Better Representation and Learning for ITPs

- Embedding and autoencoding first-order logic: GCAI'20, JLC'21
- Graph neural networks for theorem proving: IJCNN'20, ECAI'20, Tableaux'21c
- Datasets: HOLStep, Grunge, learning benchmarks: ICLR'17, CADE'19, SMT'21

### WP B: Monte-Carlo Tableaux

- Monte Carlo Proof Search CADE'17, NIPS'18, JAR'19
- Policy Optimization for long proofs Tableaux'21a
- Good GNN for connection tableaux Tableaux'21b
- Certifying non-clausal tableaux Tableaux'19

### WB B: Guidance for Superposition

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

### WP C: Isabelle/Mizar and Automation for it

- 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

### WP C: Automation for Type Theory

### WP D: Knowledge Re-use: Concept and libary merging

- Thibault-style alignments for (in)formal corpora CICM'17, JAR'19
- Statistical parsing SYNASC'17, ITP'17
- First supervised neural translation CICM'18
- Unsupervised neural translation CPP'20
- Intermediate formalization languages CICM'18
- Joint embedding of proof libraries FroCoS'21
- Disambiguating Latex to sTeX ICLR'21
- Formalizing geometric constructions from images ICMS'20, CICM'21

### WP D: Evaluations for the methods for various provers

- Isabelle: Microeconomics, Linear Programming, Homotopy Theory CPP'18, AFP'17, AFP'18, AFP'19, ITP'21
- Coq: Category Theory, Program Semantics FMM'18, DMTCS'18, MCS'20, CICM'18