Episode 20 | Josef Urban

Exploring and Combining Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics

Papers and Links:

• Josef's Homepage
• QED Manifesto
• Mizar
• DeepMath - Deep Sequence Models for Premise Selection
• First Neural Conjecturing Datasets and Experiments
• Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
• Stateful Premise Selection by Recurrent Neural Networks

Listen: