Sunday, March 3, 2024

Dagstuhl in the Fall (2023)

 

In the spring of 2022 I got sick, not as sick as I thought then, but sick enough to end up in the emergency room of the hospital in Stanford twice in the same week in May. So the whole year of 2022 got pear-shaped and many of my plans had be cancelled. I had a small procedure at the end of the year--on the day before Thanksgiving exactly-- and this made the year of 2023 a year of recovery.

The year of recovery meant I was going to try to do  three trips (since I had to cancel many in 2022): one simply to Chapman, South California, one to Bloomington, Indiana and one to  Pisa and Padova, in Italy.  All of them went well, mostly: I got covid when returning from Indiana. So I  decided to do another three trips: to St. Louis, Missouri, to Dagstuhl, Germany and to Pasadena, CA.

The one I was most worried about was the one to Dagstuhl, as I do not speak German and Dagstuhl can be fairly inaccessible. But I partnered with Jacques Carrette and Stefania Dumbrova and all went well getting there and getting back home. And being at Dagstuhl is always a pleasure! I have met several people who, like me, are concerned about using digital tools to make mathematics more accessible.

The schedule of the talks and discussions is in https://www.dagstuhl.de/23401/schedule.pdf. I really need to read a bit more about some of the work that I did not manage to grasp while there.

Tuesday, February 27, 2024

Preparing for Network Mathematics 2023

 

 

(source: Twitter/X account Stonehenge UK)


This post is a continuation of Preparing for Networked Mathematics.

During 2023 we had a few more talks on theorem provers and automated deduction. And on how the work in math provers can impact the world.

Not exactly like the picture below, but close:












which wasn't so much about math provers, but about why category theory matters so much right now. And, as usual with Michael, how to study the `relationship between abstract knowledge and the modern world'.























On 18th May we had Clark Barrett on

and on the 31st August we had Nat Shankar on

Then we had Leonardo de Moura on the 7th September talking about

Lean 4: Empowering the Formal Mathematics Revolution and Beyond

Yes, we already had Jeremy Avigad, Kevin Buzzard and Johan Commelin talking about LEAN in 2022, but it was good to hear from the main creator of the Lean  prover too!


 

(He even talked on the 7th September, a Brazilian National Holiday, and neither of us noticed it!) 

In 12th October we had Dominic Orchard talking on           Programming for the Planet























 Tom Leinster from Edinburgh University on

and then in November we had Minhyong Kim with a beautiful talk on

Of course these last three talks say more about how I feel about the role of mathematics in the world than about how we can use provers to do more  mathematics. But I think this is essential too!





































Sunday, February 25, 2024

Formal Math: are we there yet?


 I have not touched my blog much this last year. A shame. I need to write more and I need to try to correct pictures and links that stopped working. Now the programme in Bonn, on Prospects of Formal Mathematics is coming closer, so writing should help me decide to organize my time in Germany. But first things first. I need to email a few more people about our arrangements.



Sunday, December 31, 2023

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!

Monday, June 12, 2023

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.



Monday, March 13, 2023

Women in Logic: the history so far


[First appeared in the Topos Institute blog, March 6th, 2023]

This year we’re having the 7th Women in Logic (WiL) Workshop in Rome, associated with FSCD and CADE. Considering that we never had grants to help us defray costs of the workshop, I think getting to our seventh anniversary is a big milestone. Everyone who works for Women in Logic does it for free and because they find the cause important. You may be wondering, “what is Women in Logic?”

Women, like some other demographics groups, are very badly represented in STEM (Science, Technology, Engineering and Mathematics) subjects. While on paper we have the right to be part of our STEM communities, in reality the obstacles are very strong and sometimes even insurmountable for women participation in Academia. The infamous “glass ceiling” is still very much with us and many of our colleagues do not notice it. (ha, this is why it’s called a “glass” ceiling, right?) Even the colleagues that are notionally aware of the issues, many times do not see them, when they happen in their own lives. The sexism in STEM is systemic and entrenched, it affects both men and women. And it is not a small action like WiL that will defeat it, but WiL does help, a little, to shed some light on some of the issues.

Women in Logic (WiL) started for me in 2013, when Orna Kupferman, who was the Program Chair of LICS that year, presented her LICS chair findings and showed this slide:

Until then, while I knew about all the prevalent sexism in society, (it’s hard to ignore the many manifestations, from murdered women to silenced ones) I thought that my community was a bit better than most. My colleagues seemed to me more helpful and more enlightened. Thus when I saw the numbers, it was a shock: how come there were no awards for women? How come there were no women on the advisory board(*)? how come only 3.7% of the submissions in 2013 were by women? It all did seem TERRIBLE!

Much more disturbing was the discovery that, despite many efforts, things were not getting better, they were even getting worse! A representative graph was provided by the AAUW (American Association of University Women) in their report entitled “Solving the Equation”, 159 pages of dismaying facts. As you can see below, while the numbers of women in Mathematics and Computer Science improved from 1960 till around 1990, from then on they dropped, being in 2013 lower than they were in 1960! Engineering, traditionally considered one of the worst areas for women, at least has increasing numbers, but from 9% in 1990 to 12% in 2013. This is a minuscule improvement, leading to, in general, the prediction that at the current rate of progress, the pay gap will not close until 2111.

So I started to think about how to do something about this sad state of affairs. Three years later, at LICS2016, Nat Shankar asked me if I wanted to say a few words about LICS and I said I’d love to, but he might not be pleased with what I had to say. Having talked about how bad things were in the LICS community, I decided to organize the first Women in Logic Workshop, which happened as an associated workshop to LICS in Reykjavik, Iceland the next year. It was easy to find several friends who wanted to do this too, so our collective was formed.

Since then the Workshop has occurred in Oxford 2018 (UK), Vancouver 2019 (CA), Paris 2020 (online), Rome 2021 (online) and Haifa, 2022 (Israel). By most accounts the workshops have been very successful. The invited speakers, so far always two in each workshop, have been excellent and they showcased many different facets of logic in computing, mathematics and philosophy: from Software Engineering to Automated Reasoning to Computational Biology and Artificial Intelligence.

We have received some small grants from the Special Interest Group of the ACM for Logic (SIGLOG), the Vienna Center for Logic and Algorithms (VCLA), the Institute of Logic, Language and Computation of the University of Amsterdam (ILLC).These allowed us to help students and young researchers attend our workshop. We also had some donations to help us to organize dinners after the workshop in Oxford and Haifa, from Prof Ursula Martin (EPSRC and Wadham College) and from Microsoft Outreach, via Nikolaj Bjorner, to whom we’re also very grateful.

(Dinner at Haifa, 2022, with Alexandra Silva speaking)

Most recently we have also received important clerical support from the Topos Institute, to process these smaller grants. More substantial effort from the Topos Institute came in the shape of the help to establish a Women in Logic website. Producing this website has been an important step to consolidate the several activities of the collective. Many thanks are due to, especially Juliet Szatko and Tim Hosgood, for all the help provided!

After the worst (we hope) of the COVID19 pandemic, we are now in the process of restructuring and rethinking how to make the collective Women in Logic more efficient. We have several social media channels, managed by several members of the original group. So we are present on the web (Women in Logic), on Facebook (Women on Logic group), on Twitter ([@WomeninLogic1](https://twitter.com/WomenInLogic1)) and on Slack (wilcrew.slack.com). We also have our blog (womeninlogic.blogspot.com) and a YouTube channel, which we haven’t, as yet, populated much. Instead we have, so far, collected already recorded talks by women in logic and posted them on our GitHub (womeninlogic.github.io/RecordedTalks/).

But much remains to be done and we want to count on all of you, women in STEM and allies, to help change the terrible state that we still find ourselves in. Because as we know is not

Nature or nurture? No, it’s bias

Research shows that there is no inherent difference in math and science capability between girls and boys. It’s also a myth that girls aren’t interested in science: In elementary, middle, and high school, girls and boys take math and science courses in roughly equal numbers, except in engineering and AP computer science, according to the National Science Foundation. One study found that the apparent gender gap in mathematics is smaller in countries with greater gender equality, suggesting that gender differences in math are largely due to cultural and environmental factors, not ability.

 The STEM Gap, Why it Matters?

So join us, let us make a difference together!





Thursday, February 2, 2023

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.