← Feed

Posts

• View post

  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.

• View post

  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.

• View post

  1/ TypeTopology is searchable now: https://martinescardo.github.io/TypeTopologySearch.html

• View post

  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.

• View post

  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?

• View post

  The advent of AI in mathematics has turned some prominent mathematicians into philosophers.

• View post

  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 rea...

• View post

  1/ An experiment. Can an AI help me do my own mathematics? [1] A number of people have been advocating using AI to develop mathematics. I was accused by some peers of dismissing this, and, at the same time, attacked by other peers for even considering it as a possibility. So I took this challenge seriously, from both opposing parties, and decided to check what the latest so-called AI could contribute to something I actually care about. Thierry Coquand had already performed two experiments, g...

• View post

  @dlakelan@mastodon.sdf.org In our university, in the UK, we are told we use Microsoft 365, as opposed to anything else, for compliance with GDPR. Sigh.

• View post

  @ErikJonker@mastodon.social Nice. And what are the EU alternatives to US computers? I would like to de-US-ify everything in my computer life, both academic and personal.

• View post

  Thread about #UnivalentCombinatorics, in the sense of @egbertrijke. Usually people think of #ConstructiveMathematics as being more restrictive than #ClassicalMathematics. In this thread, I want to give a concrete example illustrating that constructive mathematics is more general than classical mathematics. 1/

• View post

  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.

• View post

  What is happening to "to do mathematics, you need only paper and pencil"?

• View post

  @egbertrijke I am happy to disagree with you and still be your friend!

• View post

  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...

• View post

  @egbertrijke 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.

• View post

  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 di...

• View post

  The same thing can be organized in more than just one useful way.

• View post

  The hardest thing in academic life is "context switch". And maybe in other lives here on earth, too. With a packed week, with teaching, unavoidable admin, my own work, and my work with collaborators, not mentioning family life, not only there is little time for each of these things, but when it comes to switch to the next thing there is a significant overhead involved, trying to remember what happened last time and make progress from there. And I didn't mention email...

• View post

  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 mu...

• View post

  TypeTopology is not a library. It is a huge blackboard.

• View post

  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 t...

• View post

  I propose that "universe of discourse" is more interesting and appropriate than "foundations". Do we want to talk about sets? Do we want to talk about types? Do we want to talk about whatever we have in our minds? I propose that ZFC, MLTT, and also HoTT/UF, are *not* foundations. They are universes of discourse. They are things we want to talk about, rather than "foundations".

• View post

  I am going to repeat something I believe I have already said here: there is only one mathematics, which includes both classical and constructive mathematics, and all possible mathematics that we haven't seen yet. Mathematics is something that people do. The philosophy of mathematics should not be about what kind of mathematics is "the right one". It instead should be about understanding what people do, in all directions. To some extent it is. But the philosophy of...

• View post

  I like the sense of community I get here on mathstodon and related mastodon instances. It is so nice. Occasionally, but rather rarely, things get nasty, as you would expect from normal human interactions, but in most cases they are resolved positively. And this is important to me. I moved here from twitter, which doesn't exist any more, at least not under that name, and certainly not in spirit. This was in Oct 28, 2022. At that time, the move was strange, to say the least, and...

• View post

  A lot of people embrace constructive mathematics for purely philosophical reasons, and I am fine with that. In my particular case, I love it for 90% mathematical reasons, and 10% philosophical reasons.

• View post

  Glad to see Ingo Blechschmidt (@iblech) joining us!

• View post

  David Wärn just sent me this [1]. Namely Peter Scholze mentioning Escardo-Xu two years ago. How did I miss this for that long? [1] https://www.youtube.com/watch?v=_4G582SIo28&t=5040s

• View post

  @TheBreadmonkey A very articulate statement.

• View post

  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 mak...