Preparing for Networked Mathematics
Networked mathematics is one of my main projects at the Topos Institute (the other is Dialectica categories and its extended family of formalisms). We have not had much luck getting the funding agencies to pay attention to it, yet. But the work is progressing, albeit slowly. We have been working on the suggestion that formalized mathematics will eventually be one of the main ways of producing mathematics. It seems sensible to believe that proof assistants will become really useful tools for mathematicians, and if so, formalized math will become the usual practice, not the exception. To discuss the issues of formalized mathematics and to prepare for the Hausdorff Institute of Mathematics trimester on “Prospects of Formal Mathematics” in 2024 we have had in the Topos Colloquium talks by several people involved with proof assistants and automated deduction.
Networked mathematics is one of my main projects at the Topos Institute (the other is Dialectica categories and its extended family of formalisms). We have not had much luck getting the funding agencies to pay attention to it, yet. But the work is progressing, albeit slowly.
Brendan and I discussed some initial ideas in the blog post Introducing the MathFoldr Project. Then I updated some of the previous ideas in the blog post The many facets of Networked Mathematics, as we consider MathFoldr a key component of Networked Mathematics.
We have been working on the suggestion that formalized mathematics will eventually be one of the main ways of producing mathematics. It seems sensible to believe that proof assistants will become really useful tools for mathematicians, and if so, formalized math will become the usual practice, not the exception.
To discuss the issues of formalized mathematics and to prepare for the Hausdorff Institute of Mathematics trimester on “Prospects of Formal Mathematics” in 2024 we have had in the Topos Colloquium talks by several people involved with proof assistants and automated deduction.
1 July 2021
We started with Larry Paulson on Formalising Contemporary Mathematics in Simple Type Theory. A recent talk by Larry, Formalised Mathematics: Obstacles and Achievements might be a better introduction to his research as far as mathematical formalization in Isabelle is concerned.
I worked for Larry as a postdoc in the Computer Lab, Cambridge University many moons ago, which is possibly the reason I am so fascinated by formalized mathematics. His blog, Machine Logic is super interesting and I always loved the idea that Isabelle was not conceived as a single logic, but as a generic logical framework, and it can represent reasoning in several different systems. (Together with Sara Kalvala I did some small experiments in Linear Logic in Isabelle.) I still want to develop the ideas of a project I wrote with Larry and Prof Roger Needham on modal logics for authentication and privacy, but it is getting late.
The vast library of mathematical results in Isabelle is called AFP, the Archive of Formal Proofs, or as they say, more precisely: A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.
2 August 2021
We had Kevin Buzzard talking to us about What is the point of Lean’s maths library? Kevin’s style of online demo and talk was a huge success with the audience of applied category theorists, which helped to consolidate my ability to invite other speakers not exactly categorically minded. Kevin has this awesome sentence on his website:
“I believe that computers will be able to help humans with proofs within my lifetime, and I am actively trying to make this happen sooner by (a) helping to build a database of modern mathematical theorems and definitions and (b) trying to teach mathematics undergraduates how to use the software.”
Inspiring stuff!
3 September 2021
We had Florian Rabe talking about MMT: A UniFormal Approach to Knowledge Representation. Florian is interested in the more general problem of implementing “a universal framework for the formal representation of knowledge”, not only mathematical knowledge, but also other generic computing systems. His system is described in https://uniformal.github.io/. Florian’s system MMT has been in development since 2006 and he has worked with Prof. Dr. Michael Kohlhase in several versions of knowledge management at KWARC, Erlangen, Germany. One of Florian’s main goals is to obtain foundation-independent mechanized results, thus much effort is spent on languages and meta-languages. (I also worked with Florian and other colleagues on extending the Curry-Howard correspondence to Goguen’s institutions a long time ago.)
4 November 2021
We had Jeremy Avigad talking about Formal mathematics, dependent type theory, and the Topos Institute and Lean. This was similar in some ways to Buzzard’s talk, but coming from a more philosophical perspective, was easier to understand. As Avigad says “Formal mathematics is finally getting some recognition” and the press is ready to acknowledge the big pull of the area. Recent good press exemplified by Quanta: “Building the mathematical library of the future” (2020). Also at Quanta “At the Math Olympiad, computers prepare to go for the gold” (2021), and in Nature “Mathematicians welcome computer-assisted proof in ‘grand unification’ theory”” (2021).
5 June 2022
Christoph Benzmueller talked to us about Logico-pluralistic exploration of foundational theories with computers. Chris discussed his work on formalization of logic, particularly in formalizing computational metaphysics (instead of mathematics) with collaborators, including Dana Scott, Topos’ senior advisor. Personally I am very interested in Chris’ work on modal logic, also in the benchmarking of modal theorems, less so in God’s ontological existence arguments.
6 July 2022
Josef Urban talked about Combining learning and deduction over formal math corpora and his work on combining deep learning with automated deduction. Josef, unlike many others, has an agnostic attitude to the different logical foundations and merits of different provers and implementations, so it’s interesting to discuss those kinds of issues with him.
7 September 2022
Jacques Carette talked to us about What I learned from formalizing Category Theory in Agda, which was particularly interesting to me, as together with Eric Bond and Charlotte Aten I wanted to implement dialectica categories in Agda.
September also had Johan Commelin talking to us about Breaking the one-mind-barrier in mathematics using formal verification. Johan is doing impressive work on formalization of extremely recent work (2020) in Mathematics, the Tensor Liquid Experiment, of Peter Scholze. (if this sounds a bit like a band name, well, it is.)
8 October 2022
We had Angeliki Koutsoukou Argyraki talking about the Project Alexandria in Cambridge (the one on mathematical knowledge, not the Microsoft one on business knowledge). Her talk was entitled The new era of formalised mathematics and the ALEXANDRIA Project. This was very exciting because the project has a strong component in the direction we are working, that is the direction to do with mathematical language. Mathematical English poses special challenges for NLP (Natural Language Processing) tools.
And also in October we had Richard Zanibbi, in the most relevant talk for the directions we’re aiming at with Networked Mathematics. Richard talked about Mathematical Information Retrieval: Searching with Formulas and Text. His project MathSeer and the several demos he showed us were wonderful!
9 November 2022
We had Gilles Dowek talking about Dedukti in From the Universality of Mathematical Truth to the Interoperability of Proof Systems. Dedukti emphasizes the importance of rewriting in proofs. Gilles’ talk made a series of important points, and it reminded me of other work I’m doing with Luiz Carlos Pereira and Elaine Pimentel on Ecumenical Systems, based on an idea of Dag Prawitz.
So slowly, but surely we’re investigating the issues of formalization of mathematics, as well as its affordances. I hope we will continue to do so in the near future, as there are many loose ends that need tying up.
- Goguen, J.A., Mossakowski, T., De Paiva, V., Rabe, F. and Schröder, L., 2007. An Institutional View on Categorical Logic. Int. J. Softw. Informatics, 1(1), pp.129-152.
- E Pimentel, LC Pereira, V de Paiva,2021, An ecumenical notion of entailment, Synthese 198 (22), 5391-541.