BCAM Scientific Seminar | Proof Mechanization: topological and algebraic methods for the automatic development of proofs

Abstract

Per Martin-Löf's work on the development of functional programming languages with the expressivity to recreate the syntax of Mathematics, produced a broad landscape of possibilities for the development of computational tools for proof assistance, that is, software designed to allow for the translation of mathematical arguments into statements in a programming language, through a Curry-Howard-type correspondence, that would allow to use the results generated by their compilers as evidence of the correctness of the proofs.

This class of tools are recently becoming more attractive due to two phenomena: the great popularization of some of them, like the Lean language, that are supporting the development of huge libraries of formally-verified Maths; and the recent focus on the employment of LLMs for the automated creation of mathematical text, which is pressuring existing channels of peer review by the sheer volume of proposals, and incentivizing the search for new ways to build trust towards text possibly absent of human involvement in its creation. 

In this talk, we will show a paradigmatic example of type theory: the family of univalent theories, covered in the study of Homotopy Type Theory. Of recent apparition, this field has gained a great amount of attention due to its ability to combine mathematical technology from diverse areas of knowledge, such as Algebraic Topology, Logic and (Higher) Category Theory. A study in detail of this area allows us to explore the advantages and limits the theory may impose on commercially viable proof assistants, the kinds of axiom systems that the systems force upon mathematical practice, and their relationship with Classical Maths. Moreover, we will talk about work in progress towards solving certain conjectures in the Model Theory of univalent foundations.