Martin Escardo

Professor 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

homepage: https://www.cs.bham.ac.uk/~mhe/
Pronouns: He/Him
Inclusivity: Full
Attempting: To get as green as possible and save the planet

Public Key

npub14a5755aglz3euvetuy8z7x25akaz42lgvrgkr8qj2a55ghpwaelqjf9fse

NIP-05 Address

martinescardo_at_mathstodon.xyz@momostr.pink

Profile Code

nprofile1qqs276022w503gu7xv47zr30r92wmw32405xp5tpnsf9w62ytshwulspz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dshdr5h7

Publishing to

yabu.me

relay.damus.io

nos.lol

Author Public Key

npub14a5755aglz3euvetuy8z7x25akaz42lgvrgkr8qj2a55ghpwaelqjf9fse

Show more details

Last Notes

2026-04-25 17:10:50 UTC

- reply

My view of Gödel's theorem is this.
Consider the following axioms for a given universe of discourse,
We have an element 1, called the neutral element.
We have an operation (x,y) ↦xy called multiplication.
Moreover, we postulate that multiplication is associative and has 1 as a neutral element.
Are we surprised that there are many different universes that satisfy the above axioms (which are called the "group axioms"?
No, we are not.
But then suppose that somebody else said "let's axiomatize sets".
This time people may be more surprised. There isn't a unique notion of set satisfying the axioms of set theory.
Just like there isn't a unique group satisfying the group axioms.
Should you *really* be surprised in the case of sets?
I don't think so. If you give axioms for the gadget you imagine in your mind, it is likely that many other gadgets will satisfy the same axioms.
Why, in the first place, did you originally think that your axioms actually did specify a unique thing?
Gödel is just telling you that, just like the group axioms, which have many models, your axioms for set theory also have many models.
Why would you think that you would be so powerful to come up with axioms that would specify a unique thing?
Gödel's theorem is not a "restriction of what we can do".
It is actually a liberation. We can reason with the same axioms about very many different and interesting, universes of discourse, as topos theory shows.
Gödel's theorem is not a negative result. It is an invitation to explore new, interesting, mathematical worlds.

2025-09-26 18:00:28 UTC

- reply

I thought you were primarily a physicist? 🙂
@npub1sq8…xvpd

2025-08-26 18:14:54 UTC

- reply

What Tom and I found was https://tex.stackexchange.com/questions/730148/cref-refers-to-lemmas-as-theorems
(I saved it as a comment in the latex file!)
I don't know about your fix, but our fix doesn't break files for people who use older versions of texlive.
This is important in our case, because I have the latest version and Tom has an older one, and we are working on joint projects.
You need to add
```
\usepackage{thmtools}
\renewcommand{\cref}{\Cref}
```
I think that's all, according to the comments we wrote in our latex file.

2025-07-07 19:40:02 UTC

- reply

The behaviour I currently get is that I get lots of little notification bundles, not a single notification bundle, for favourites and boosts of my posts.

2025-06-15 17:00:02 UTC

- reply

writes "okay, that's a fine solution: then you just need to change the math curriculum so that students learn enough type theory to know that there are different types of 0."
I don't think it will harm students if they are told that a function comes with a domain and a codomain, as you well know as a category theorist.
There are several exponential functions, including at least the following three:
ℕ × ℕ → ℕ (arises in combinatorics)
ℝ × ℕ → ℝ (arises in Taylor series and the binomial theorem)
ℝ × ℝ → ℝ (wants to arise in analysis, but doesn't really make sense)
As I said before, it is kind of a coincidence that we have an embedding ℕ → ℝ of counting numbers (where the count can be zero) into the real line, mapping "counts" to "points" or "positions" in the line.
It is a *useful* coincidence, but we should avoid being misled by it.
When we write x^n in a Taylor series or in the binomial theorem, clearly x and n have different roles: (1) x is real number, (2) and n counts how many times we differentiated a function in the case of Taylor series (figure out yourself what n is counting in the case of the binomial theorem).
But also I want to say this. A lot of undergrad and PhD students in both mathematics and computer science are well ahead of their academic supervisors, and taking up computer formalization without their permission or blessing. Such people are very likely to be aware of the distinctions I have made above, by necessity, rather than philosophy.
The proof assistant doesn't allow you to pretend that there is only one zero (the natural number, the real number, the ordinal, the cardinal, the initial object of a category, and so forth).
1/2

2025-05-18 14:38:56 UTC

- reply

writes
"- LLMs are *terrible* at math. However, they are good enough to fool a crackpot."
So recently a crackpot (as I reported here on mathstodon) approached me. When I took the time to explain to them that, no, this is wrong, they said "You are right. <blah>", obviously pasting ChatGPT where "You are right" is the clue. But then one day later, presumably after they gave more prompts, they told me that actually they were right.

2025-05-12 19:13:20 UTC

Google search is useless. So mathematicians who know enough about the history of mathematics please help me.
I remember having read recently that a prominent mathematician in the early 20th century objected making group theory part of the standard mathematical curriculum for undergrads. Who was that?

2025-05-10 18:59:35 UTC

- reply

writes "What should the new item say? Maybe
20 points for saying you've developed your theory in conversations with AI."
At least 20 points, but 20 point will do.

2025-04-12 14:02:07 UTC

- reply

But how odd is that?
The HoTT Book, in order to avoid problems with choice, defined a type of real numbers by higher-induction-recursion, and showed that they are between the Cauchy and Dedekind reals.
And then it conjectured that they should coincide, when restricted to [0,1], with the reals defined above (the Cauchy completion of the rationals within the Dedekind reals).
Let me say that although I was involved in the production of the HoTT Book in a minor way, I had no involvement with the above definition or conjecture.
I asked my PhD student Auke Booij back in 2017 to prove this conjecture, and he did.
https://arxiv.org/abs/1706.05956
So perhaps that above is not that odd.
Auke submitted the above paper to a HoTT/UF workshop, but, sadly, it was rejected because "it was not difficult enough".
Odd. The HoTT Book conjectures something, but when the conjecture is proved, it is not considered worth of being published.
But, just to close, the point is that, after Mike Shulman,
https://arxiv.org/abs/1904.07004
we have that Book HoTT is an internal language for ∞-toposes, and so the HoTT-Book conjecture proved by Auke shows that not only interval objects in our sense do exist in ∞-toposes, but also they coincide with the interval within the HoTT Book reals.
(Notice, however, that this interval has nothing to do with the interval in e.g. cubical type theory. Our interval is a type which is a set in the sense of HoTT/UF.)
6/
(I may say more later, but this is the temporary end of this thread.)

2025-04-12 14:00:36 UTC

- reply

Alex and I proved that in any 1-topos, our interval object is given as follows.
First notice that (in the absence of choice) the Cauchy reals are not necessarily Cauchy-complete (so they shouldn't be called the Cauchy reals). We always have that the Cauchy reals are embedded into the Dedekind reals, which are Cauchy complete. Now, using Pataraia's fixed-point theorem, we can show that there is a smallest Cauchy complete subset of the Dedekind reals containing the rationals and that the unit interval there satisfies our universal property of interval object.
Odd.
5/

2025-04-12 13:59:00 UTC

- reply

We both wanted the following.
(1) A definition of interval object that would apply to any category, or to a category as general as possible.
(2) The definition should embody geometrical intuition.
(3) Just like Lawvere's categorical definition of natural numbers object automatically captures computation (specifically primitive recursion), our notion of interval object should capture computation with real numbers in the interval, again automatically.
(4) In categories of interest, the categorical definition of interval should specialize to what the interval is generally agreed to be in these categories.
(4.1) In the category of sets, the categorical interval object should be the usual real-number interval [0,1].
(4.2) In the category of topological spaces, the categorical interval object should be the same, with the usual topology.
(4.3) In the category of locales, the categorical interval object should be the obvious sublocale of the localic real line as defined in e.g. Johnstone's book Stone Spaces.
(4.4) In categories for computability, it should coincide with the notions people have considered before having seen our definition.
(4.5) And so on.
(4.6) In particular for 1-toposes. (We will come back to ∞-toposes soon.)
3/

2025-04-12 13:57:27 UTC

A universal characterization of the closed Euclidean interval.
This thread is about a notion of interval object in any category with finite products, on joint work with Alex Simpson.
There are two joint papers I would like to link for the moment:
(i) A universal characterization of the closed Euclidean interval (extended abstract). Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, pp.115--125. Boston, Massachusetts, June 16-19, 2001.
https://martinescardo.github.io/papers/lics2001-revised.pdf
(ii) Abstract Datatypes for Real Numbers in Type Theory. RTA/TLCA'2014.
https://martinescardo.github.io/papers/realadt.pdf
A third one, more mathematical in nature, is in preparation, and should (and must) be ready by 1st May.
1/

2025-04-01 19:39:45 UTC

- reply

writes "an attempted proof that doesn't work is also a null result. You got something, but it ain't something that satisfies you."
Often I have learned something very valuable by attempted proofs that didn't work. It'd better be like this, because most attempted proofs don't work. A proof attempt is an exploration of the territory, and whenever you explore a territory you are bound to find false paths to your intended destination.

2025-03-19 20:16:20 UTC

- reply

This morning, before I saw this reply, I tried to edit my post for a minor thing, but instead I accidentally deleted it. The edit and delete button are next to each other, which is not an optimal design choice, and I was doing things quickly to get back to work.
In any case, I didn't say I "don't want to help them", like you suggest, and I didn't intend to imply this either.
I think my subconscious point was that there are some things that people notice only when they experience them themselves and are affected by them. Which is kind of upsetting in this case, but I suppose it is part of human nature.
One definition of "shocking" is "causing a feeling of surprise and dismay".
I am dismayed like you, but not surprised at all. They said they would do it, they are doing it, and I have seen things like this happening since I was born, in my own country, and also in my parents' country, which are not the same. And much worse. So what is happening in the US didn't shock me - it just brought back memories of what I had already seen. And I want to say this again: the US actively played a role in making these things happen back then.

2025-03-11 13:22:58 UTC

- reply

Where I grew up in the 1970s it was like that, and worse.

2025-03-10 20:56:05 UTC

- reply

Sad, yes. But shocking? Less sure.

2025-03-10 20:26:44 UTC

- reply

I particularly like the last bullet point.

2025-03-07 20:47:23 UTC

- reply

We do this example in our 3rd-year undergraduate Agda module called "Advanced Functional Programming".
But let me say this: yes, honest calculations are important, but more important are "reasoning" , "thinking" and "understanding".
You don't even know what to calculate if you haven't reasoned, thought and understood.

2025-02-25 22:35:59 UTC

Question in my son's GCSE mock exam: "What does RAM store?". My son's answer: "Data and programs". According to the teacher, who is the "head marker", the answer should have been "Data, programs and the operating system", and so his answer was deemed wrong.

2025-02-18 22:11:33 UTC

- reply

I remember this concept from my physics lectures in years 1-2 at university. Nice to see something new about it in this thread.

2025-02-18 21:20:52 UTC

Formalization is overrated.
The difficult job, now that a lot of people are doing new mathematics using so-called "proof-assistants" as their electronic blackboard, including myself, the real problem is unformalization, which means telling people what you have discovered and created.
We unformalize our work to give talks and to write papers. People, including myself, don't want to read formal code, and they shouldn't have to. But I am happy writing formal code when I use the computer as an interactive blackboard.
Perhaps things regarding the above discussion will change in the future, but for the moment we are in the present, when unformalization has to be done by hand.
LLM's can't help in the experiments I have tried, and I think that unformalization is more difficult than formalization for computers, given our current technology.

2025-02-15 17:26:09 UTC

Is the arXiv safe from the current US government attacks to education, research, universities and science?
Perhaps they haven't yet realized that it exists.
1/

2025-02-04 10:44:46 UTC

- reply

Explain!

2025-02-02 20:34:38 UTC

I've already got rid, for some years, of
* Twitter (when it was Twitter)
* Facebook (although only recently I deleted the account).
* WhatsApp (account still to be deleted, I use Signal instead, with my immediate family, and even with my old parents).
* Dropbox (I use pCloud instead).
I still need to get rid of Google and Amazon. The latter is quite easy. The former less so, because I have an Android phone and I don't want an iPhone either. And many accounts linked to google.
Oh, and there is github too.
How can I get rid of all American tech in my life, personal and academic?
I feel like a voluntary slave of tech companies.

2025-01-23 20:52:54 UTC

- reply

You should switch back to your trademark "super-Baez". Now you are unrecognizable, and at first I thought somebody was impersonating you.

2024-12-03 22:21:33 UTC

- reply

Well, it doesn't make sense when x = 0 or y = 0. Sorry.
The question is not difficult. It is nonsense in my view.

2024-11-21 22:12:23 UTC

- reply

says
"We could be falling through the event horizon of a truly enormous black hole right now, and we'd never notice - though I consider this very unlikely. "
Both statements are rather intriguing. In particular, that you consider this very unlikely. Can you say more about this?

2024-09-10 20:21:41 UTC

If you are not allowed to ask questions to each other, can this be really called a "debate"?