Perhaps funny story. Today I met with one of my collaborators regarding a paper we are writing, where all but two theorems are formalized in TypeTopology. We discussed how to formalize one of them. In the end, we concluded that the opposite of what the alleged theorem says is true. 🙂 The […]

Rhetorical questions, when written down, should not end with a question mark. They should end with a full stop. I practice this preaching.

I've used `bash` forever (first on Linux and then on MacOS). I've also used symbolic links forever. But never did I realize, until yesterday, Friday, that if you do $ cd <some directory which is a symlink> $ ls .. then you don't get a listing of the files from the directory you started from […]

As some of you know, from time to time I write expository threads here and elsewhere. An index to all (?) of them is here: https://martinescardo.github.io/blog.html

In this thread, I'd like to (re)advertise my MGS'2019 lecture notes "Introduction to Univalent Foundations of Mathematics with Agda" https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#contents In the lengthy Introduction, I explain how univalent foundations differ […]

In our Advanced Functional Programming module, we secretly teach students dependent type theory and even univalent foundations, without the students knowing we are doing this. Or the people who allow us to teach this module. 🙂 In any case, this has been rather successful in practice with most […]

All sciences have their internal battles, including mathematics. And this is healthy, unavoidable, but tiresome, too. But in Computer Science, people seem to be much more prone to battles, including public battles. And this manifests itself in damaging ways, in grant applications, in […]

I have been postponing, for about three months, to try to prove something "I know is true"s, either on paper or in Agda in TypeTopology. Or, rather, my schedule is against me. I have recorded 5 starting points on paper (or actually on my tablet in handwritten notes) where I start thinking […]

Peter Freyd said that "Perhaps the purpose of categorical algebra is to show that which is trivial is trivially trivial". In my experience, however, mathematics is non-trivially trivial. Including category theory and everything else.

Progress. Less is more. I meet with Paulo Oliva weekly, online (and very occasionally in person) to work on game theory and more generally the selection monad, since 2007 (Skype, Google meet, Zoom, or whatever is available when we meet). Today's meeting (without a plan in advance) amounted to […]

First year student: I don't understand this notation (there is a lot of information I have to reconstruct by myself, and I don't know where to start with). Later years' student using a proof assistant: Damn, the notation requires me to write down so much obvious information.

It is good to rediscover things. I keep rediscovering things all the time. This doesn't disappoint me. It rather tells me I am on the right track.

Today we had an internet outage at home and I ended up in a chat to try to get this sorted. I was sure that this was not a chatbox when (1) I was first put in a queue, and then, more convincingly, (2) one of the answers had a typo.

A lot of students who do genuine work of their own are using AI to "improve" their writing. Particularly, but not only, students whose first language is not the same language as that of their host institution. The downside is that people will immediately see that this is AI written, and will […]

The extended version of our LICS'25 paper, titled Constructive Ordinal Exponentiation, is now on arXiv. It has two new sections (Section 6 and 8) on ordinal arithmetic. Everything is formalized in Agda and merged into @MartinEscardo's TypeTopology repository. https://arxiv.org/abs/2501.14542v5 […]

I am thinking about how to increase interaction in my lectures. Particularly when I ask a question, based on what I've just explained, to the students. So here is an idea. Give 1 point for a correct answer. Give 2 points for an answer that is half correct. Give 3 points to a completely wrong […]

Is there a name for this paradox? "It might seem surprising after the massive global disruption caused by today’s AWS outage that Amazon’s shares are actually on the front foot, but for many investors the issues put into perspective exactly how much of the internet relies on its services."

Signal doesn't seem to be working in Birmingham UK.

My 15-year old son saw that Matt Parker was coming to The Rep for "Getting Triggy With It". So my wife bought tickets for the three of us at his request. Then our two older sons with their respective girlfriends visited us, and my wife decided to invite them too, which resulted in 7 of us being […]

This should have been big news! Ten funding agencies from eight European countries have pledged to support a public infrastructure that is poised to replace academic journals: FWF 🇦🇹 RCN 🇳🇴 Forte 🇸🇪 ARIS 🇸🇮 SRC 🇸🇪 FCT 🇵🇹 CSIC 🇪🇸 DFG 🇩🇪 Formas 🇸🇪 ANR 🇫🇷 Only two of them issued press releases in […]

One day, whichever operating system you are using in your many devices, you will be able to access all your files without thinking, from any device. This day is not there yet, although we are getting close. My use case is writing by hand to do mathematics or prepare talks. Here I want to […]

I am not sure who to attribute this to, but it came up in personal discussions with Bezem, Coquand and Dybjer. Proofs assistants are the new way of doing mathematics **informally**. (Yes, I know, you would have expected me to say **formally** instead.) The users **don't know the formal […]

"Babbage saw the analytical engine as a mathematical device. After all, it primarily stored and operated on numbers. But Lovelace recognized that a machine de­­signed to crunch numbers could do much more if the numbers represented other things. “Supposing, for instance, that the fundamental […]

It is very useful, mathematically speaking, but also it is philosophically satisfying, that HoTT/UF proves unique choice. (And, for that matter, also the internal logic of 1-toposes validates unique choice.) There is a price to pay for this in HoTT/UF: (1) You have to *prove* that the […]

The US is at a point now where a professor who got bullied by the far-right sends a message basically saying "Phew, we made it out of the country". It is worth reflecting on this for a minute.

Following the Heyting Day symposium held in honour of Jaap van Oosten, Benno van den Berg and I wrote a brief popular article on Jaap's life, his scientific work (categorical realizability) and his other contributions to academic life. Jaap has done a great deal for mathematical logic in the […]

Online sellers: Do you think it is reasonable to deliver such a small thing in such a large box? An almost invisible thing, 2.5cm, in a box 23x20x18 cm^3. This is better seen with your eyes, in the attached picture.

1. 4 months ago, The Supreme Court gave families a right to opt out of LGBTQ+ education in schools. Now, in Montgomery County, Maryland, where the case originated, the results are in. Only 43 families out of 160,000 students have exercised that new right. Subscribe to support our journalism.

Buy a car 20 years ago, and get notified today by the manufacturer that they have been hacked and that all my details with them are leaked. Renault.

Conventional wisdom says motherhood should wait for tenure as before you land a permanent post, #academia is just not that family friendly🙁 @carersinstemm.bsky.social are calling for change and to celebrate their new report, a Saturday🧵on parenting & academia! 1/9 👩‍🔬🧪🔭⚛️ ℹ️: carersinstemm.co.uk

I've just attended this workshop in honour of Peter Dybjer retirement: https://www.chalmers.se/en/current/calendar/cse-workshop-in-honor-of-prof-peter-dybjer/ It was really nice, with lots of research friends attending, and rather well planned by Ana Bove. Flying back home tomorrow.

Fun fact. Two of my undergrad / MSci students this year want to do their final-year projects on category theory. I never advertise category theory as something I propose (computer science!) students to do. But I will be happy to have them to contribute category theory to TypeTopology, because […]

I remember a book on topology (published or unpublished? maybe only online?) for which I can't find a reference or a link. Can you help? In any case, it is a book that has no proofs. The idea of the book is to create a sequence of lemmas, each of which is obvious, so that the diligent […]

It is WILD that we now live in a time where my job as an astrophysics professor has gone from "learn cool things about space" to "try to get someone to hold billionaires accountable for dropping shit on us from orbit"

I've updated the accounting page on our wiki with actual numbers about where money is and where it's going: https://wiki.mathstodon.xyz/finance

Whenever I have a new PhD student, I try to give them a relatively easy, but sufficiently hard, project that forces them to explore the literature. I am scratching my head regarding my incoming PhD student. And I've asked former PhD students for ideas. 🙂 In any case, it is always nice to have a […]

A lot of what Bill Thurston says here resonates with my personal experience: https://arxiv.org/abs/math/9404236 I don't understand his mathematical work, and, if he were alive, he probably wouldn't understand mine. But this is precisely the kind of thing he discusses! Among many other […]

Idle thoughts about computer life. So in the last two days, I tried Safari, as opposed to Firefox, because it is more (memory) efficient. Indeed it is. But otherwise everything is worse for my particular experience. And, ignoring the limitations, it feels like a foreign land with everything […]

The transparency doesn't annoy me. Maybe because I disabled it immediately after upgrade. 🙂

I enjoyed talking about my expository paper (https://doi.org/10.4230/LIPIcs.TYPES.2024.1) at this wonderful CIRM event this morning. https://conferences.cirm-math.fr/3377.html Thanks to Jacopo Emmenegger for the photo! #typetheory #HomotopyTypeTheory #hott

Hacking thread. I have a Samsung tablet with their S-pen, which I got in 2020, replacing one I had got in 2016. (I examined an MSc thesis by a student in Singapore in 2020, and the honorarium was exactly what the table cost.) I use it often, writing notes by hand as in a blackboard, to […]

TypeTopology thing. (*) Sometimes you can prove that a type, with arbitrary types as parameters, is a proposition using univalence in an unavoidable way. This is fine if we want to use TypeTopology as a language to prove theorems about arbitrary ∞-toposes. But sometimes I want to use […]

Assistant/Associate Professor at University of Birmingham UK (apply by 30 September). The University of Birmingham is recruiting assistant/associate professors in the School of Computer Science. The Theory of Computation group at Birmingham is world-renowned and we have been actively […]

PhD position with Benno van den Berg on the semantics of Homotopy Type Theory (esp. effective Kan fibrations) at the ILLC in Amsterdam! https://www.illc.uva.nl/NewsandEvents/News/Positions/newsitem/15777/PhD-Position-in-the-Semantics-of-Homotopy-Type-Theory Application deadline: 27 September […]

There is a program that will print "yes" if it will rain tomorrow, and "no" otherwise. Proof. Tomorrow it will either rain or not. If it does, the program that prints "yes" will do. Otherwise, take the program that prints "no". QED.

I **hate** the conflation of constructivity with computability. Constructive reasoning is not computable reasoning. I said this in a thread here, but I want to say it loudly as a separate post.

I keep the AI option on Google, not only for entertainment, but also to train myself that, at least in my case, everything I ask to be found is got wrong by the first AI response. In any case, jokes aside, I may switch it off, because it just makes my mathematical search life more difficult […]

Dear people who are saying that the CDC directors who quit yesterday should have “stayed and fought”, With all due respect, you do not grasp the magnitude of the problem of RFK Jr. He is asking them to do unethical and immoral things that will actively harm the people of the United States. 1/3

I am a big fan of command line man pages. But, I wish people who write cool programs could also write cool man pages. Man pages that can do the job.

I hate I have to deal with my email during the evening so that I can actually work during the day. Some people do it the other way round, which is equally bad.