Hilbert wanted an algorithm to solve all mathematical problems.
Turing showed it doesn't exist.
But then we have it now, after all, and most mathematicians are upset as a result.
Remote
Martin Escardo
@MartinEscardo@mathstodon.xyz
mastodon 4.7.2Professor at the University of Birmingham, UK.
I am interested in constructive mathematics and (constructive and non-constructive) homotopy type theory and univalent foundations, connections of topology with computation, (infinity) topos theory, locale theory, domain theory, combinatorial game theory and much more.
See my meta-blog:
https://cs.bham.ac.uk/~mhe/blog.html
3866 Followers
121 Following
50 Posts
Joined October 28, 2022
homepage:
Pronouns:
He/Him
Inclusivity:
Full
Attempting:
To get as green as possible and save the planet
When I was young, I learned, and was taught, how to make the computer to work efficiently and correctly, in my computer science degree.
Now it is the opposite. Do brute-force search using giant farms of computers, using a huge amount of energy and water, and get results that are not guaranteed to be correct any more.
And I was discussing with a colleague this morning that my 2001 laptop ran faster than my current top-range computer for everyday tasks. Of course, it had a much worse CPU and much less ram. And of course the software for things we still do *now* was much faster *then*.
I still have that laptop from that time running Ubuntu 4.10 from 2004 in my personal museum of computers. You would be amazed how responsive the system is for everything we do every day with a computer. I recently tested it with my son, because he was curious to see how things were then.
So we are using more powerful hardware for getting a poorer experience.
The new computers are much better for some things, such as running Agda. But, for everything else I happen to do, they were just as fast, because people programmed them in a more efficient way (they had to - there was no other way).
1/ TypeTopology is searchable now:
There is one advantage of a fanless laptop. You notice quickly when there is a runaway process that you didn't start and starts using all your cores and ram as your keyboard gets boiling hot.
The advent of AI in mathematics has turned some prominent mathematicians into philosophers.
RE: https://mathstodon.xyz/@tao/116975504347111605
This is interesting.
But I am the kind of person who gets impatient with videos and prefers to read, at my own pace, sometimes faster than what a video offers, and sometimes slower.
In fact, when I was a student I was the kind of person who got quickly distracted during lectures. The lecturer would say something rather interesting at some point, and then my mind would switch off from the lecture and think only about that, and then I would realize much later that I missed everything after that point. Luckily books existed to both catch up and then go further.
One more thing. During the pandemic, I asked my students in a poll whether they preferred (1) the prerecorded lectures, (2) the lecture notes, or (3) to have both. The answers were evenly split among the three possibilities.
Quoting
Pre-announcement: the website for "Mathematical Discourse", a new peer-reviewed video journal that will referee and publish mathematical *videos* rather than papers, is now online: https://www.mathematicaldiscourse.org/ . I am serving as one of the editors. (A more detailed announcement will be forthcoming.)
Open quoted postReplying to
3/ Two things happened to me along the way.
I still think it is more fun to work with people, in particular PhD students, than with so-called AI's.
And the machine was actually OK. But just OK.
Also it was impressive, e.g. writing Agda code we know we could have written ourselves, if we wanted to and if we were patient enough.
Everything I discuss here is public [3], including the AI's own first-person account and every prompt I gave it.
You will have to judge by yourself.
I don't think I know what this means for the future, and I don't think anybody else knows either.
But I am kind of sad after this experiment.
[3] https://github.com/martinescardo/ClaudeExperiment
Two things I wish hadn't happened:
- The pandemic.
- AI.
But both did. The main people affected are students, although all of us are too.
But the way students have been affected is much worse, and much more difficult to deal with. Nobody has the answer. And very few people recognize this as a genuine problem, both for the students and more generally for society.
Replying to
2/ The open problem I chose is a 2013 conjecture, namely that the height of the dialogue tree of a System T term of type (ι⇒ι)⇒ι is below the ordinal ε₀.
The results are mixed, with both progress and walls, as usual.
Claude built a proof framework and an ordinal-arithmetic library from scratch, and proved the bound for a first-order fragment of the language. But the conjecture itself is still open.
I do like that Claude decided on its own to consider a first-order fragment to get partial results. I didn't ask it to do that.
For full disclosure, there is exactly one file in the repository I wrote by my own hand, namely [2]; everything else was written by Claude, after my prompts.
[2] https://github.com/martinescardo/ClaudeExperiment/blob/master/source/MartinEscardo/README.md
So a free Firefox plugin I've been using for years tells me
"... A majority of users use our products for free, and the relatively small percentage of Premium subscribers is all that is subsidizing our continuously increasing server costs. To improve our Premium experience and to sustain our business model, we’ll be making the LanguageTool browser extension available exclusively for paying customers. "
Summary: not free any more.
Am I surprised?
Yesterday I rebooted a Linux computer whose "uptime" in the command line gave 180 days.
I only did this because of the vulnerability reported in recent days.
But, no, the update didn't fix it. Never mind, because the vulnerability doesn't affect me. I am using this rather old computer just for data backup.
It runs Ubuntu with Live Patch, which means it updates itself and installs the updates without the need for rebooting.
In any case, I find it impressive that a computer can run for 180 days, keep itself updated (mostly) without wifi ever breaking during this time.
I rebooted it remotely by ssh - except that, because its partition is encrypted, I had to enter the decryption password manually, in the computer which is fine to do every 180 days.
Replying to
@jonmsterling I agree with everything except the last paragraph.
I would replace it by saying that people who design proof assistants should interact more with mathematicians. Many of them already do.
Replying to
@fullyabstract@fosstodon.org Yes, of course, I fully agree.
I don't know how people are going to read my thread.
The way I read it myself is this:
"Some people told me not to get behind, so I tried, and I had mixed views, mostly negative, but who knows where this is going."
Remember, the thread is called "An experiment".
The same thing can be organized in more than just one useful way.
Replying to
@JacquesC2@types.pl writes "I quite like formalizations that are made to look like encyclopedia pages."
I am sorry to disappoint you, but this is precisely what I don't like.
What I like about mathematics is the narrative, the story that keeps us engaged, and give us intuitions of various sorts.
TypeTopology chooses this view.
In any case, it couldn't choose the encyclopedic point of view, because it is work in progress.
You can only get an encyclopedia for work that has already been done.
Work in the making requires a different organization, while it is done, and then after it is done and established in the mathematical literature.
In TypeToopology we focus in the "while" rather than in the "after", because life is short.
But of course sometimes we try to clean up and get things organized.
For the purpose we use TypeTopology, namely to be a blackboard for producing ideas, including for publication, the encyclopedic point of view doesn't make any sense at all.
Replying to
@AndrasKovacs
PS. My 16-year old son also tells me off that I use Ubuntu rather than his preferred Linux distribution.
To my credit, I introduced him to Linux years ago.
@liamoc @jonmsterling
I've finished preparing my MFPS talk, two weeks in advance. First time ever in my life.
But I still need to prepare a second talk for an MFPS special session.
Replying to
Tim Gowers "A recent experience with ChatGPT 5.5 Pro" https://gowers.wordpress.com/2026/05/08/a-recent-experience-with-chatgpt-5-5-pro/
Logical order is different from genetic order in mathematics.
Bourbaki chose logical order.
Genetic order is so much more pleasant and informative - but this is only my personal view.
This also gets reflected in the way people choose how to organize their mathematical ideas in proof assistants.
There is *no single way* which is better than all other ways.
However, let me say that I love the genetic way much better than the logical way. It is just the way my brain happens to work.
Of course, people are allowed to have their own personal views of the "graph of mathematical ideas"
(Is this a so-called "subtweet"?)
Replying to
@jonmsterling Remember that Hyland was Gandy's student and that Andy Pitts was his student in turn.
So perhaps it is not so surprising that the effective topos and triposes are using similar techniques.
@jonasfrey @dgb37 @zwarich
Replying to
@olynch@mathstodon.xyz What if you had two parsers?
-
One damn fast, prone to formal verification, following known theory, that is bad at error recovery.
-
The other ad hoc and slower that is better at error recovery and giving useful information about errors, triggered when the first one reports a failure.
In a large codebase, the first one would be used most of the time. The second one would be applicable only at the file you are currently developing or modifying.
So I've learned a lot about a little of TypeTopology, by exploring its graph, in the last few days.
It is so interesting to see how things depend or not depend on each other, and what we consider in practice to be "the foundation of everything else".
One thing I have learned in my experiments this weekend is that its *chosen* module graph differs considerably from the actual dependencies of the functions/definitions within the various modules, which is a completely different graph.
And I suspect the same happens in unformalized mathematics as recorded in the literature. We organize things by mathematical subjects, rather than logical dependencies (except if you are Bourbaki, but, even then, I am not completely sure).
It was painful to explore this systematically, by the lack of tools I could find, even with your help here, and there is a lot more work to be done, but I am really interested in learning how mathematical ideas connect to each other "in practice and foundationally", from an experimental point of view, given the mathematics recorded in various repositories, including TypeTopology.
Replying to
@liamoc
It also reminds of people who use Arch Linux.
They are constantly fiddling with their operating system.
I like operating systems that just work. Two examples(*) I like, but are hated by many, are Ubuntu and macOS, in this order. I am sure many other flavours of Linux are likeable too, but life is short.
I was among the first users of Ubuntu in 2004, because I had tried every distribution of Linux at that time, and for each of them some piece of hardware wouldn't work. Then a postdoc at my institution told me: "I've got this CD in my post, which claims to be a distribution of Linux which just works in any existing hardware". I tried it, and it solved all my problems 22 years ago. Since then, I use only Ubuntu in my Linux machines. And still, despite all what people complain about, it just works.
Other distributions are not bad at all. It is just that I would have to learn their different ways, and I have no time, patience or interest in learning them.
If I could use just Linux, I would. It just works, particularly with Ubuntu.
And Windows is a no-no, because things are just ugly in every respect.
(*) Well, these two examples do give trouble sometimes. But only rarely.
@jonmsterling
Replying to
2/
(7) Now the neat thing is this:
(7.1) This accommodates both the classical and constructive meanings of "exists" and "or", by choosing suitable toposes.
(7.2) There is a topos for classical mathematics.
(7.3) There is a topos for computability.
(7.4) And, I claim, all toposes are for constructive mathematics. This is because of the following item.
(7.5) If you want to prove something in *all* toposes, all you have to do is not appeal to excluded middle or choice in your proof.
(7.6) This is why I prefer to speak of "neutral" rather than "constructive" mathematics.
(7.7) This is like working in "all groups" rather than, say, "just abelian groups". Both activities are interesting. The former is more general, and the latter can get more theorems, at the expense of considering fewer groups.
I would like to, once again, link to my blog post
https://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/
In that post, I use geometry, rather the group theory, as an analogy. But the point is exactly the same.
Now, should I be constructive or classical? I prefer to be allowed to be both, just like people are allowed to discuss arbitrary groups, but also just abelian groups when their ideas apply to just them.
The counter-intuitive idea here, of course, is that "exists" and "or" may mean multiple different things. But this surely did happen at the beginning when mathematicians realized that multiplication can mean multiple different things (in particular, addition in abelian groups).
@RobJLow@mathstodon.xyz
Replying to
1/
@RobJLow@mathstodon.xyz writes "MartinEscardo I suspect that there are at least some people who think that when they find the 'right' axioms, the scales will fall from everybody's eyes and those axioms will define the right mathematics."
Let me try to explain my point of view in more detail. Which, by the way, is shared by many people in my mathematical community.
(1) The sign "·" may mean many things. Multiplication on the reals, or in any group are examples (among others!).
(2) In constructive mathematics "exists" means something different from what it means in classical mathematics. And the same goes for "or".
(3) But it is perfectly possible, and it has been done, to accommodate both meanings in a single "foundation" (I so hate this terminology).
(4) But now, more darlingly, just like "·" may mean different things (in different groups), "exists" and "or" may mean even more things than discussed in (2).
(5) Oh, wait! Don't "exists" and "or" have fixed meanings? No, like "·" doesn't.
(6) Just like we may let the meaning of "·" depend on the group we are working with, we can let the meaning of "exists" and "or" to depend on what "topos" we are working with.
Never mind what toposes are, for the moment, but they are the analogues of groups in this discussion.
Replying to
4/ The LICENSE.
"... Whether copyright subsists in AI-generated output is legally and morally unsettled; no copyright is asserted here by any person, and none should be inferred. To the extent that any rights nonetheless subsist in this work, it is made available under the terms of the MIT License"
I made the AI to write this. 🙂
Replying to
@pigworker@types.pl
When you just know that something is true, and then you battle with your mind, with your proof assistant, or your literal backboard, or you paper notebook, or your brain in the shower.
This is the *genetic* way. You just "see" things before you can justify them. And they turn out to be true.
Then there are at least two ways of writing them: the genetic one (how they came to your mind) or the logical one (start from first principles getting a different explanation than what your mid first suggested to you intuitively).
Which then may need you to look at the logical order of things. But you first have your idea independently of any logical order, and, indeed, independently of any logic at all.
I believe this, no matter how competent I am in "logic". It is the intuitive ideas that drive things forward. Of course you need to be competent in (intuitive) logic, but this is not enough.
@egbertrijke@mathstodon.xyz I am happy to disagree with you and still be your friend!
Replying to
@jaycech3n
I have a colleague, a professor, who I shall not name, who constantly has Agda broken as a result of updates to other things.
@liamoc @jonmsterling
Replying to
@maxleibman@beige.party writes "Never post a joke about anything on Mastodon unless you are willing to listen to strangers argue about it in your mentions for hours!”
It's even worse when you tell a joke and people take it as a fact.
Replying to
@seabass@social.seabass.systems
I use KDE Connect, from both Linux and macOS.
Additionally, I use scrcpy (to display my Android tablet in my laptops when giving lectures and writing in the tablet) and moonligth/sunshine (to be able to handwrite in my machines (typically using xournal++) using my Android tablet.
(I do have an iPad, but the Android tablet is much better for handwriting.)
Replying to
If you are formalizing e.g. category theory, where everything is already done and organized in textbooks, then it is much easier to adopt the encyclopedic approach.
If you are investigating a new subject, e.g. injective types, you don't know in advance what the better definitions are, what theorems will end up with some parts of their proofs reused somewhere else, and what you are going to discover in this journey.
So there is a big difference.
Doing new mathematics is trial-and-error and exploration.
Formalizing mathematics that somebody else has already organized, post-fact, in textbooks is an entirely different matter, because somebody else did the organization for us.
You can only organize something after it has been done. Things don't grow in an organized way.
It is hopeless, as mathematical practice shows, to try to do this in advance. In the process of doing new mathematics, you always discover, the next day, that something you did yesterday can be generalized, simplified, and refactored. And this goes on day after day.
This is what a blackboard looks like. A collection of better and better ideas. An encyclopedia, on the other hand, is the result of this journey + a big reorganization effort.
Replying to
@ryanbrewer@mathstodon.xyz Yes, "genetic" in the sense of how things "originate", rather than how they are "explained later".
@egbertrijke@mathstodon.xyz I was just trying to discuss perspectives, rather than saying that anybody is wrong.
I don't think you, or I, or anybody else can claim to be "absolutely correct" in this discussion.
Let's just carry on discussing, providing different perspectives.
Replying to
By the way, in my 7WTop talk a few weeks ago, I did mention Gandy, Bishop and Martin Hofmann in page 5 of my slides, for the record:
https://martinescardo.github.io/.talks/escardo-venice2026-stone-types.pdf
@jonasfrey @dgb37 @jonmsterling @zwarich
Replying to
@dgb37 Gandy cites unpublished work by Turing as a possible precursor.
@jonasfrey @jonmsterling @zwarich
Replying to
@jonmsterling I think that (with enough personpower) it should be possible in Agda to control which subtype theory of Agda one wants to work with, in particular to disable everything that is not MLTT.
Replying to
@mjd@mathstodon.xyz Interesting.
I am not sure what you are alluding to in this case.
My experience was that Claude (in particular Fab 5) was not up to the job in this particular case, but otherwise it behaved quite well regarding my orders and requests.
But this just my personal experience in a two-week experiment.
Replying to
@pigworker@types.pl I didn't mean genetic in the sense of DNA or evolution, but rather in the sense of generating/producing things.
If you have a better word, I will be happy to adopt it. The idea is that we produce ideas before we can work out their logic, which we dutifully do, in any case, eventually.
Replying to
@JacquesC2@types.pl
Happy to disagree.
TypeTopology follows the flow of ideas, given that its main purpose is to be a giant blackboard to produce new mathematics rather than record already-existing mathematics.
Proof-engineering tools should be used to make them into encyclopaedic format in the sense you want, not the other way round.
Sadly, such tools don't exist, but I think they are perfectly possible (without the need of any AI nonsense).
(And you comparison of LaTeX and PDF are not related to this discussion, as far as I can see. In fact, LaTeX contains more logical information than PDF, which, of course, trained people can recognize from the PDF.)
@egbertrijke@mathstodon.xyz @gallais@mamot.fr