The Thesis Review [20] Josef Urban - Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics
Mar 5, 2021
Josef Urban, Principal Researcher at the Czech Institute of Informatics, shares his insights into artificial intelligence and automated theorem proving. He discusses the balance between deductive and inductive reasoning in formal mathematics, alongside the significance of the Mizar system. Topics include the philosophy of mathematics as invention versus discovery and the challenges of formalization. He also highlights advances in premise selection using machine learning, and reflects on his PhD journey that shaped his dedication to meaningful scientific inquiry.
AI Snips
Chapters
Transcript
Episode notes
Math: Invented or Discovered?
- Gödel believed in a platonic mathematical world, where mathematicians discover truths.
- Formalists see math as symbol manipulation within a rule-based environment, detached from real-world interpretation.
Foundational Flame Wars
- While living in the Netherlands, Josef Urban considered creating a mailing list called "foundational flame wars" due to the strong opinions on mathematical foundations.
- Constructive mathematicians, for example, reject the law of excluded middle, impacting computational interpretations of proofs.
Path to Formalization and AI
- Josef Urban's interest in formalizing mathematics stemmed from a desire to understand its nature and its relation to computer science.
- His masters' thesis explored machine learning on large mathematical corpora, driven by his interest in automating theorem proving.