← Feed

Posts

• Post #4396919

  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.

• Post #4298531

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

• Post #4298530

  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.

• Post #4298529

  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?

• Post #4298528

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

• Post #4069368

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

• Post #3736956

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

• Post #2599038

  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/

• Post #2599037

  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.

• Post #2415618

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

• Post #2181932

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

• Post #2181929

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

• Post #2181928

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

• Post #2181927

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

• Post #2181926

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

• Post #2118875

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

• Post #2065649

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

• Post #1890831

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

• Post #1890821

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

• Post #1868053

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

• Post #1816034

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

• Post #1671203

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

• Post #1510503

  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.

• Post #1471249

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

• Post #1378697

  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

• Post #1158590

  @TheBreadmonkey A very articulate statement.

• Post #1158586

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

• Post #982927

  Is there any command line utility to get a topological sort of a directed graph written down in graphviz `dot` format? Preferably, I would prefer that instead of a linear order, I was given a list of lists, where each list has the next level of dependency. For example, something in homebrew or github? Or, is there a tool to convert a graph in `dot` format to a graph in the format required by unix `tsort`? In any case, `tsort` is less than what I want, as discussed above.

• Post #982926

  Agda is getting damn fast. In 2019, I asked for a new, fast desktop computer, because running Agda was getting annoying. I don't remember how long the old desktop from 2012 took. But the 2019 one took 7mins to type check TypeTopology. That was so fast! And then I got a MacBook Air M1, because they gave one to everyone in our department. At that time, this reduced the time of TypeTopology to 4min, compared to the 7min above. Now it is 9min in the M1 with the current released version...

• Post #879771

  I like the fact that the first person to implement a full-fledged proof assistant in a computer was a mathematician. Not a computer scientist. Not a logician. Not a philosopher. His name is de Bruijn. More precisely, Nicolaas Govert de Bruijn. And he conceived and implemented Automath. https://en.wikipedia.org/wiki/Nicolaas_Govert_de_Bruijn Like Brouwer, he is Dutch. Unlike Brouwer, he was a formalist. I don't think this is recorded anywhere. But I vividly remember a talk de Bru...