The annual award is granted by the BSF to the most outstanding and original BSF supported project in mathematics and computer science.
The BSF Board of Governors chose to grant the 2021 award to Dr. Liron Cohen, a senior faculty member at the department of Computer Science, who co-authored (together with Prof. Robert Constable from Cornell University) the proposal entitled "Extending and Applying Implemented Intuitionist Mathematics".
Whereas standard mathematical discourse is based on classical mathematics, constructive mathematics offers a more computational approach that has been exploited widely in computer science applications. The variant of constructive mathematics called intuitionistic mathematics, however, is less well-known and little investigated despite its unique computational capabilities. Intuitionistic mathematics, which originated in the ideas of Brouwer, extends the Church-Turing notion of computability by incorporating novel forms of computation, namely, choice sequences, the Bar Induction Principle and the Continuity Principle. Despite considerable work on the theoretical foundations of Brouwer's intuitionistic theory, it has not yet been studied in a formal, computational setting and, in particular, has not been incorporated into a proof assistant.
To fill this gap, the proposed study will develop a new version of the Nuprl proof assistant that fully integrates the notion of choice sequences and use the unique resulting computational setting to explore the theory's wider implications, especially with respect to the broader notion of computation. This implementation includes providing computational interpretations of intuitionistic principles and developing semantics to support them. We will then use the powerful resulting framework to develop novel intuitionistic theories, namely, intuitionistic calculus and intuitionistic homotopy theory.
Leveraging the novel computational capabilities is expected to have major theoretical and practical implications across different areas. In particular, it will improve the capabilities of theorem proving tools and facilitate significant advances in the internal verification of complex systems, make calculus more elegant and practical, and help physicists explore continuous phenomena.
