Position 1 requires knowledge of (automatic) first-order theorem proving and will involve programming Vampire.

The aim of direction 2 is understanding capabilities and limitations of modern automatic theorem provers for conducting textbook proofs in math. An ideal candidate for Position 2 should have knowledge of interactive theorem proving and be able to make experiments with Vampire.

When applying, please specify which of the positions you are applying to (1, 2 or both).

Position 1 requires knowledge of (automatic) first-order theorem proving and will involve programming Vampire.

The aim of direction 2 is understanding capabilities and limitations of modern automatic theorem provers for conducting textbook proofs in math. An ideal candidate for Position 2 should have knowledge of interactive theorem proving and be able to make experiments with Vampire.

When applying, please specify which of the positions you are applying to (1, 2 or both).