Martin Escardo

I want to say something I found shocking and interesting.

Three weeks ago, a mathematician, Georg Lehner, approached me by email to say that he applied a result of a paper of mine to a paper of his.

The interesting thing is that in that paper of mine I redeveloped the patch topology both point free and constructively. (Although I was careful to say only in the last line of the introduction that, by the way, this paper is constructive, as a hidden message.)

But Georg managed to use this to make progress in classical mathematics, on Algebraic K-theory of stably compact spaces.

It is kind of shocking that a paper on constructive mathematics helps to make progress on classical mathematics.

But I rather like this, because, as I have said repeatedly here, I believe there is only one mathematics, of which classical and constructive are just two branches.

Moreover, I have witnessed the interaction of these two branches quite vividly in the last 25 years, in conferences I have attended, and in publications.

The interaction goes both ways.

And, by the way, Georg is here this week at 7WFTop in Venice, where he gave a talk about a different subject, namely measure theory via locales, which was both quite interesting and rather well delivered.

There is only one mathematics, of which both classical and constructive mathematics are branches, and, since at least the 1960's with the advent of topos theory, interact with each other.

The interaction is only getting more intensive and healthier.

@TheBreadmonkey@beige.party A very articulate statement.

Agda is getting damn fast.

In 2019, I asked for a new, fast desktop computer, because running Agda was getting annoying.

I don't remember how long the old desktop from 2012 took.

But the 2019 one took 7mins to type check TypeTopology. That was so fast!

And then I got a MacBook Air M1, because they gave one to everyone in our department. At that time, this reduced the time of TypeTopology to 4min, compared to the 7min above.

Now it is 9min in the M1 with the current released version of Agda and TypeTopology, because the latter has grown considerably since 2019/2020.

But guess what! Now my 2012 desktop, which I still use, as a server and for casual work, type checks TypeTopology in 4min30sec, thanks to the work of @AndrasKovacs@mathstodon.xyz , Amy and others.

My oldest machine from 2012 with the development version of Agda outperforms the cutting-edge machines of 2019/2020!

In a Mac M4, the time goes down to 1min15sec. There is no need to desire a Mac M5. A 10% speed up would be peanuts.

Is there any command line utility to get a topological sort of a directed graph written down in graphviz `dot` format?

Preferably, I would prefer that instead of a linear order, I was given a list of lists, where each list has the next level of dependency.

For example, something in homebrew or github?

Or, is there a tool to convert a graph in `dot` format to a graph in the format required by unix `tsort`? In any case, `tsort` is less than what I want, as discussed above.

Start your own war. Then say to everybody else "get your own oil".

I like the fact that the first person to implement a full-fledged proof assistant in a computer was a mathematician.

Not a computer scientist.

Not a logician.

Not a philosopher.

His name is de Bruijn.

More precisely, Nicolaas Govert de Bruijn. And he conceived and implemented Automath.

https://en.wikipedia.org/wiki/Nicolaas_Govert_de_Bruijn

Like Brouwer, he is Dutch.

Unlike Brouwer, he was a formalist. I don't think this is recorded anywhere.

But I vividly remember a talk de Bruijn gave at Edinburgh, at an LFCS seminar, when I was there in 1997/1998. At some point Gordon Plotkin asked whether he was a formalist, and he answered "yes" emphatically.

Brouwer, instead, was emphatically non-formalist. Even more non-formalist that my classical mathematician friends.

And, as you know, Brouwer was the main founder of what is known as intuitionistic mathematics, that lead in turn to constructive mathematics. Then the topos theory people picked it up, not for philosophical reasons, but for mathematical reasons. The logic of the internal language of a topos is intuitionistic - this is a theorem, rather than philosophy.

I don't agree with either de Bruijn or Brouwer, but I love their ideas.

I also like that in the 1970's, Bourbaki, known for their excessive formalism, dismissed the idea that mathematics could actually be formalized, when de Bruijn and his collaborators had already done that without their knowledge:

L. S. van Benthem Jutting, as part of this Ph.D. thesis in 1976, translated Edmund Landau's Foundations of Analysis into Automath and checked its correctness.

I have a calculator that is correct 80% of the time. But don't worry, every time I use it, I check the results myself.

Agda is getting rather faster!

https://github.com/agda/agda/pull/8473#issuecomment-4121273331

Thanks @AndrasKovacs@mathstodon.xyz, Amy and other people!

Learn by (re)doing it yourself
----------------------------------------------

Generative AI can be good or bad, who knows. It is impossible to predict the future, even in purely physical circumstances, when all equations are known, but where it is difficult to measure the inputs with enough accuracy.

And even good things can be bad (think e.g. of knifes).

But something genAI has destroyed, and all universities over the world are struggling to cope with, is "learn by doing it yourself".

I had always told my students, well before genAI was envisaged, that the only way to learn is to reconstruct things by yourself.

Most students are not reconstructing things by themselves with the advent of genAI.

When the Mac M1 was released, and offered at our university, it was great.

Type checking TypeTopology went down from 7min to 4min, compared to the previous (quite recent at that time) Intel machine I had.

That was great!

But then, of course, TypeTopology keeps growing, and, currently, with an M4 machine, it takes 6min to type check.

But then come three developments since the current version of Agda, in the development version.

One is to make things sequentially faster, which brings the time down to 4:30min from the previous 6min.

And then, in parallel, using the new `-j` option, down to 2:20min.

And then, with a better handling of mutual blocks, even faster. That I can't measure yet, but for one particular module it goes down from 20secs to 4sec.

These three things make everything so much faster.

You don't need to buy new cutting-edge hardware. You just need better algorithms to beat the next generation of hardware.

Thanks, Agda developers, for investing your time on that!

From 6min down to to 2:20min is rather impressive. It is much better than what Apple can offer when moving from M4 to M5.

Added in proof. Save the planet with better algorithms.