Extending and Applying Implemented Intuitionistic Mathematics

Whereas standard mathematical discourse is based on classical mathematics, constructive mathematics offers a more computational approach which has been exploited widely in various applications in computer science. The variant of constructive mathematics called intuitionistic mathematics, is however less well-known and investigated despite its unique computational capabilities. lntuitionistic mathematics which originated in the ideas of Brouwer, extends the standard notion of Computability by incorporating novel forms of computation that are not governed by any law (for example, ones generated by throwing a dice). However, despite considerable work on the theoretical foundations of Brouwer’s intuitionistic theory, it has not yet been studied in a formal, computational setting.

To fill this gap, the proposed study aims to develop a new mechanized tool for formal reasoning that fully integrates the extended notion of computation and use the unique resulting computational setting to explore the wider implications of the theory. We will then use the powerful resulting framework to develop novel intuitionistic mathematical theories, namely, intuitionistic calculus and intuitionistic homotopy theory.

Leveraging the novel computational capabilities is expected to have major implications, both theoretical and practical, across different areas. In particular, it will improve the capabilities of mechanized tools and facilitate significant advances in formal verification, make calculus more elegant and practical, and help physicists explore continuous phenomena.