[20] Josef Urban - Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics
Mar 5, 2021
auto_awesome
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.
Josef Urban discusses the evolution of automated theorem proving and its significant advancements in making formalized mathematics accessible to AI.
The integration of machine learning techniques, particularly in premise selection, is transforming mathematical reasoning and enhancing theorem proving capacities.
The philosophical debate about whether mathematics is invented or discovered influences mathematical exploration and the technical work of formalizing mathematics.
Deep dives
The Evolution of Theorem Proving
The discussion explores the significant advancements in theorem proving, particularly focusing on automated theorem proving and its historical context. It highlights how researchers, like Joseph Urban, have contributed to making formalized mathematics more accessible to automated systems. Urban's efforts included translating the Mizar library into a format usable by these automated systems, revealing that, even at the time, about 40% of theorems could be proven automatically. This evolution indicates a move towards integrating machine learning techniques to enhance theorem proving capabilities.
Integrating Machine Learning with Mathematics
Machine learning has started to play a pivotal role in mathematical reasoning, especially in tasks like premise selection. Urban's thesis introduced a machine learning framework to select relevant premises from large mathematical libraries for automated theorem proving, demonstrating initial successes with simple models. This effort laid the groundwork for more sophisticated approaches that have since emerged, such as the use of graph neural networks, which enable a more complex understanding of relationships between mathematical premises. The intersection of machine learning and formal mathematics illustrates the potential for AI to tackle long-standing challenges in the field.
The Philosophy of Mathematics
The podcast delves into the philosophical debate surrounding whether mathematics is invented or discovered, with insights from both Urban and historical perspectives. This discussion reinforces contrasting views, where some believe mathematics is an inherent truth waiting to be uncovered, while others see it as a construct designed to navigate the natural world. This philosophical discourse is connected to the technical work of theorem proving and formalization, emphasizing the foundational beliefs that underpin mathematical exploration. Such philosophical considerations are critical for researchers, influencing how they approach problems in formalized mathematics.
Challenges of Formalization in Mathematics
Urban discusses the challenges faced in formalizing mathematics and translating informal mathematical expressions into formal ones, revealing inherent complexities within the task. Initial experiments utilizing probabilistic grammars and neural networks yielded promising results, indicating potential pathways for effective translation methods. Despite successes in syntactically generated datasets, real-world applications highlight the difficulties of accuracy and reliability in translations. This ongoing challenge emphasizes the need for further exploration into robust machine learning applications that can bridge the gap between informal and formal mathematical representation.
Advice for Emerging Researchers
To support new researchers, Urban emphasizes the importance of independent thinking and focusing on profound underlying problems rather than following trends. He encourages individuals to deeply analyze their motivations and to pursue questions that hold the potential for significant advancements in their field. Additionally, he highlights the practical necessity of acquiring proficient data processing skills as vital to research success. This dual approach of intellectual curiosity and technical competence is crucial for navigating the complexities of modern research environments.
Josef Urban is a Principal Researcher at the Czech Institute of Informatics, Robotics, and Cybernetics. His research focuses on artificial intelligence for large-scale computer-assisted reasoning.
Josef's PhD thesis is titled "Exploring and Combining Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics", which he completed in 2004 at Charles University in Prague. We discuss his PhD work on the Mizar Problems for Theorem Proving, machine learning for premise selection, and how it evolved into his recent research.
Episode notes: https://cs.nyu.edu/~welleck/episode20.html
Follow the Thesis Review (@thesisreview) and Sean Welleck (@wellecks) on Twitter, and find out more info about the show at https://cs.nyu.edu/~welleck/podcast.html
Support The Thesis Review at www.patreon.com/thesisreview or www.buymeacoffee.com/thesisreview
Remember Everything You Learn from Podcasts
Save insights instantly, chat with episodes, and build lasting knowledge - all powered by AI.
