Mathematics of Proof Assistant
Date: 29/09/2025
Time: 13:30 - 15:00
Time: 13:30 - 15:00
Location:
Abstract In this talk, we give an overview of a foundational mathematical theory based on the notion of concept. This theory, which we call HyperMath, will be used as a framework upon which we wish to implement a new proof assistant. We first give a short survey of currently influential proof assistants Coq, Agda, and Lean. They are all based on dependent type theory equipped with a countable hierarchy of non-cumulative universes. And, this design choice was inevitable to avoid Russell-type paradox. However, we will argue that a theory having infinitely many universes is very unnatural. Then, we show that by taking the notion of concept, rather than the notion of dependent type, we can develop a new foundational mathematical theory (HyperMath) that is free from Russell-type paradox. In particular, we show that concepts of symbolic computation and logic are the two key concepts of HyperMath. We coclude by explaining our strategy of implementing a sound and natural proof assistant based on HyperMath.