Formalizing Invisible Mathematics - IPAM at UCLA

Explore the concept of formalizing invisible mathematics in this thought-provoking lecture by Andrej Bauer from the University of Ljubljana. Delve into the challenges of translating mathematical practices into computer-readable formats, examining the unspoken conventions and techniques that enable efficient communication in mathematics. Discover how proof assistants employ strategies like implicit arguments, type classes, and tactics to mimic human mathematical reasoning. Consider the potential for organizing these techniques into a cohesive mathematical theory, drawing inspiration from programming language theory. Gain insights into the design of flexible proof assistants that can be user-extended, and contemplate the fundamental question of why mathematics works as a system of knowledge.