undefined

Josef Urban

Principal Researcher at the Czech Institute of Informatics, Robotics, and Cybernetics whose research focuses on artificial intelligence for large-scale computer-assisted reasoning.

Best podcasts with Josef Urban

Ranked by the Snipd community
undefined
Mar 5, 2021 • 1h 25min

[20] Josef Urban - Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics

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.