Abstract: Conjecture and plausible reasoning are often necessary precursors to rigorous mathematical proof. Polya discussed this at length in his two volume work on Mathematics and Plausible Reasoning, and some other mathematicians (e.g., Mazur) have written about it more recently. But despite its central role in mathematical practice, there lacks a formal 'meta-mathematical' framework for analyzing how such conjectures and intuitions guide 'rigorous' mathematics. After a brief overview of Voevodsky's program on the Univalent Foundations (UF), I present a formal theory of conjecture (called homotopy probability theory), in which conjectures are represented as homotopy types in UF. I then discuss how certain aspects of this formal system may make it more suitable as a foundation for mathematical practice.

The talk is intended for a general mathematical audience. I assume no prior familiarity with Univalent Foundations or homotopy type theory.

A preprint associated to this work can be found at the following link:https://philpapers.org/rec/CRALOP