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

relay.nostr.bg

relay.damus.io

nos.lol

Author Public Key

npub14a5755aglz3euvetuy8z7x25akaz42lgvrgkr8qj2a55ghpwaelqjf9fse

Show more details

Last Notes

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-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-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 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-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-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-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-09-10 20:21:41 UTC

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