Josef Urban

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.