Ada Lovelace Day in December?

 

 

My Ada Lovelace heroine of 2023 is
Andrée C. Ehresmann from the
Université de Picardie Jules Verne 

(Photo by Rabatakeu CC BY-SA 3.0, Wikimedia)

"Better late, than never," I say. Yes, Ada Lovelace Day (ALD) is in October, and it varies a little each year, a convenient leeway, for chronically late people, like myself. This year I have less of an excuse, as I had decided to honour Andrée in July already. But the year was hectic, in a good way, so I didn't get around to posting my ALD "hommage" so far. But today is the last day of the year, so here it goes, before the clock chimes, and we change back into pumpkins.

Andrée has been a role model for me in many ways. She's been a mathematician for longer than I have been alive, and I am very old indeed. She has this awesome description of her research work in her webpage. I share with her a diversified academic career (I will try to imitate the lovely graph below) and a love for category theory and its explanatory power.

I have meant to write about Andrée before. In 10/27/2016 I posted a message of Marta Bunge's in the blog "Women in Logic". Like today's post, that one was hastily written, rushing to some function or something else. But at least it was written and records my indebtedness to Marta and her friendship to me and to Andrée. So I could write lots about Andrée's work, but you can look at her pages, the "Cahiers" work for more than 40 years, and the lovely diagram above. So I'd rather leave you with Marta's words in 2016 and a picture of Marta, since I have not mourned her absence enough. The volume celebrating her work is now almost totally ready, so I will be writing more about Marta soon. She wrote:

"There is recently an article in the journal Nature about the presence of women in science and on how to improve what seems to be an unfair situation, which I believe. I hope that someone more qualified than I can do this since I believe it is important for our field. Without a shadow of a doubt I consider Andree C. Ehresmann as someone who has done a lot for our field - not just by continuing the work of Charles Ehresmann by publishing his Oeuvres Completes and continuing with the journal Cahiers de Topologie et Geometrie Differentielle (Categoriques), but by encouraging many researchers in our field - both men and women. She certainly deserves mention as a woman and a mathematician. I leave you with that. All the best."

Happy New Year!

Network Mathematics: small approaches to a big problem

 

 

 

 

 

 

 

 

 

The reason for this blog post is to find easily a presentation of mine that has not been recorded. 

 I have discussed this subject at least three times already: once in the Topos Institute internal seminar, once with a physicist friend interested in information theory and mathematics (Simone Severini), and once in a talk for the Brazilian UD (Universal Dependencies) group. This last occasion has produced the slide deck at "Networked Mathematics: NLP tools for Better Math", May 2023. 

Now Networked Mathematics is a big problem. I have talked about it in several blog posts in the Topos blog, namely:

1.  Introducing the MathFoldr Project 

2. The many facets of Networked Mathematics

3. Mathematical concepts: how do you recognize them? 

4. Preparing for Networked Mathematics 

One of our partial approaches for solving the problem is the idea of recognizing and extracting mathematical concepts from mathematical text. That means using NLP technologies for the specific domain of Mathematics. 

But I have been working on other, related solutions to the problem, discussed in the presentation above. I hope to write more about these other solutions soon. 

For the time being I leave you with an interesting, old blog post about another problem that has not been solved, so far: Connecting The Dots: Lessons in Rebellion From the Math Network

Now, because this reminded me of the Math Genealogy, I cannot resist posting this other picture. Of course there are several ways to connect a mathematician to Paul Erdős and some are nicer than others. For many years the AMS tool gave me as my shortest connection to Erdős the one via Vaughan Pratt and Frances Yao. Now it is given me the one below, which I think it is even nicer.

The road to Networked Mathematics

 [Source]

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.

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.

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!

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.)

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).

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.

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.

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.)

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!

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.

Login