Interview with Bruno Bentzen
Can you briefly introduce yourself?
I am an Assistant Professor in the School of Philosophy at Zhejiang University, formally appointed through the New Hundred Talents Program as a research professor. I am interested in the foundations of type theory and enthusiastic about the applications of type theory in the formalization of mathematics using theorem provers. I joined Zhejiang University in 2021 and since then I have also been collaborating with Professor Beishui Liao and his group in the area of AI and related fields.
What are the main research challenges you are working on now?
My work revolves around the use of constructive reasoning in mathematics and the foundations of mathematical constructivism. One of my guiding principles is that type theory should be taken seriously as the underlying foundational system of constructive mathematics. Constructive type theory, the form of type theory I work with, was developed by Per Martin-Löf to serve as a full-scale formalization of constructive mathematics as done initially by Erret Bishop.
What are your favorite online resources?
Mailing lists (FOM, PHILOS-L, TYPES, logica-l) and social networking services such as PhilPeople, Google Scholar, ResearchGate, and Github, and online repositories such as ArXiV, PhilSci-Archive, and HAL archives.
What are in your opinion the main research challenges in AIs, robotics and reasoning?
I can only speak about the challenges involving the use of formal methods in mathematics. Present-day pen-and-paper mathematical proofs are getting longer and harder to check, so the process of formally verifying an informal proof using a computer offers essential contributions that can potentially shape the future of mathematics. Type theory is closely related to computer science through type systems. Its constructive character makes it a practical computer programming language. For that reason, it is often easier to mechanically verify the correctness of formal proofs written in formal systems based on type theory than set theory. There are, however, many open questions about what different kinds of type theory (simple vs dependent, intensional vs extensional, etc.) are better suited for the job.
What are your aims outside of academia?
When not busy at work, I enjoy spending my time with my wife and family, traveling together, having meals with friends, watching series, playing board games, etc.