This may be Girard's most brilliant contribution to humanity. https://girard.perso.math.cnrs.fr/mustard/article.html

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

If you are a student who would prefer your advisor to have more gray hair, then you should converse with them like this on Discord: Me: "Good luck with your final exam and thesis defense today! If you'd like me to peek at your slides, send them to me." Student: "Oh no, I totally forgot about […]

Chatting with PhD students during a coffee break at the school where I lectured; (The student shall remain nameless.) Student: Are you really a student of Dana Scott's? Me: Yes, of course. Student: Oh my god, you're so old.

This week I gave a lecture series at the School on Logical Frameworks and Proof Systems Interoperability. I spoke about programming language techniques for proof assistants. The lecture slides and the reference implementations of a minimalist type theory are available at […]

Mike Wright has been a long-time recorder of talks at conferences, including category theory conferences. He has a huge archive of recordings (>100k hours) and needs support to digitise them and make the archive freely available online. There are talks going back 50 years, and the project will […]

Has anyone ever actually seen Kleene's T predicate?

Emacs 30.1 freezing on MacOS 15.5 (Intel MacBookPro) is getting a bit tiresome.

Mini-rant: logic texts that think 0=1 is a reasonable replacement for ⊥.

I wonder how much work it would be to convert my blog to @jonmsterling forest. My blog is based on jekyll and is experiencing distinct bitrot. Although, one fun part of the blog are reader comment's (which currently don't work).

The type of all families in a universe 𝓤, Σ X : 𝓤 , (X → 𝓤), is isomorphic to the type of all functions in 𝓤, Σ X : 𝓤 , Σ Y : 𝓤 , (X → Y). Take this as an interesting puzzle, which will be easy for you if you know HoTT/UF. This can be proved with univalence. I haven't thought whether any […]

Dana Scott gave a model of classical set theory that violates extensionality. It's a bit hard to get the paper: Scott, Dana: More on the axiom of extensionality.Essays on the foundations of mathematics, pp. 115–131 Magnes Press, The Hebrew University, Jerusalem, 1961 Randall Holmes has a note […]

Today when writing a paper in LaTeX based on Agda code in TypeTopology, I was about to write a comment justifying why something is done in a certain particular way rather than in another more general, and more transparent, way. Thinking about this on paper turned out to be a bit tricky, so I […]

The second student formalization project was a piece of classic algebra, the Artin Wedderburn theorem, which states that a simple left artinian ring is isomorphic to the ring of matrices over a division ring. Job Petrovčič, Matevž Miščič and Maša Žaucer worked on it. (At first just one of them […]

I taught a class on formalized mathematics in Lean. Today two projects were handed in, and both of them are quite impressive. In the first project, Luka Opravš formalized Polya's enumeration theorem, and then proceeded to also implement and formally verify an efficient algorithmic version. It […]

Computing all optimal plays of a sequential game. This morning I finished some work with Paulo Oliva, which I want to report here. In a previous thread, I discussed sequential games defined with dependent types, and how to compute optimal strategies for these games using selection functions […]

The set up for the above previously published work is the selection monad J X = (X → R) → X, where R is a type of outcomes. For example, for tic-tac-toe, it is R = {-1,0,1}. One player wants to minimize the outcome, and the other player wants to maximize it. We work with the selection […]

Now, suppose you want to compute *all* optimal plays, not just one (for example, you may want to count how many optimal plays there are in tic-tac-toe). Then we can consider the monad JT := (X → R) → T X, defined from a monad T and an algebra α : T R → R. ( […]

The Clerical language for exact real number computation has a non-deterministic guarded case statement which requires concurrent execution of guards. A student of mine made it run in parallel on multiple CPU cores. It got slower. Parallell programming is hard […]

I guess almost all academics are approached by crackpots regularly. In the last few days, I've been approached by a ChatGPT-assisted crackpot. At the beginning I tried to help them, in case they were not crackpots, but just somebody trying their best. They, indeed, were somebody trying their […]

Now would be a good time to start petitioning the EU to enforce the Right to turn off AI. Upon opening a MSc thesis, Acrobat Reader just told me "this appears to be a long document, would you prefer to read a summary?" Are they completely insane?

With my free time, I've done a bit of accounting for mathstodon.xyz. You can see the latest numbers at https://wiki.mathstodon.xyz/finance. At the moment we're running a slight surplus. I recently reduced our server costs so that should improve a little bit. @ColinTheMathmo and I are pleased […]

If you're interested in learning how proof assistants and proof checkers work, and what their underlying formalisms are, consider applying to the International School on Logical Frameworks and Proof Systems Interoperability, which will take place on 8–11 September 2025 in Orsay. France. There […]

I need to pick five random art pictures that will be part of an exhibition. I am having a hard time choosing. What do y'all like? https://www.random-art.org/?liked=0&sort=popularity

Speaking from personal experience, the Grand Bazaar in Instanbul enjoys a translation symmetry – in more than one sense of "translation".

Myhill isomorphism theorem is a kind of "ambiental" variation of Cantor-Schröder-Bernstein theorem. Let X be a set. Given A, B ⊆ X, a map f : X → X is a *reduction* from A to B when ∀ a ∈ X. x ∈ A ⇔ f x ∈ B. Write A ≤₁ B if there is an injective reduction from A to B. Write A ≡ B if there is […]

Hey, Haskell hackers, how much shorter can you make the construction of Myhill's Isomorphism Theorem? https://gist.github.com/andrejbauer/5ead3af68457bcfe724cbb7bef19b298

May I just say that the OCaml libraries have really bad documentation.

One only has to diss constructive math to get upvotes by mathematicians. https://mathoverflow.net/a/491478/1176

A while ago I received a phone call from a man who lives in a small Slovenian town. He claimed to have squared the circle, finally after 10 years of efforts. He wanted to come to talk to me about it in Ljubljana. I asked that he first send me his construction […] [Original post on mathstodon.xyz]

Today I had to read 7 abstracts and then the respective papers. Can the authors please say in the first sentence what the paper is doing? Don't start by giving background, or saying why (you think) the problem is important. Just please say right away what you have done. Then, if you feel it is […]

Here is a new reasoning principle which I have not encountered before. Majority Decision Principle: Given propositions p₁, p₂, p₃ and q, suppose (1) pᵢ ⇒ ¬q ∨ ¬¬q, for i = 1, 2, 3 (2) pᵢ ⇒ ¬pⱼ, for i ≠ j Then ¬q ∨ ¬¬q. The principle is classically valid, but not intuitionistically provable […]

A revised version of the “The countable reals“ paper is available. We threw out the faulty proof of "all maps are continuous", which therefore been relegated to an open problem. The topos is very good at defying proofs that use the recursion theorem from computability. This is not a surprise […]

Reviewing of math papers takes forever. Do math reviewers think they are guarantors of correctness? That seems unreasonable to me.

Daily reminder on how good ChatGPT is. I asked it to show me the diagrams for 𝑓 : 𝑇𝐴 → 𝐴 being an algebra for the monad 𝑇.

I just noticed that synthetic computability is my go-to idea for birthday presents. My paper on fixed-point theorems was for the Lawvere-Freyd issue of Tbilisi journal https://doi.org/10.1515/tmj-2017-0107, the continuity theorems for Dieter Spreen's issue of Logic & Analysis […]

TIL I made the types.pl logo.

I tried https://notebooklm.google on two papers of mine. It's advertised as "Your Personalized AI Research Assistant". The short summary is that the tool is exactly as good as an incompetent science journalist, except that it is stubborn. When confronted with factual mistakes it made, it tries […]

How to do synthetic mathematics in ten difficult steps: 1. Take off your programmer's hat – not everything is a language. 2. Put on your mathematician's hat – keep in mind that language matters. 4. Clear your mind and prepare yourself for mental discipline that will be required for what lies […]

In the formalization class I am teaching I am doing a class project on formalizing partial combinatory algebras https://andrejbauer.github.io/partial-combinatory-algebras/ (Isn't it a cool idea that the teacher should also do a class project?) As expected, the genereralities, such as […]

I can never remember the formula for the closure operator 𝑗 : 𝖯𝗋𝗈𝗉 → 𝖯𝗋𝗈𝗉 forcing a predicate 𝑃 : 𝐴 → 𝖯𝗋𝗈𝗉 to be true. It is this \\[j(q) = \forall r .\, (q \Rightarrow r) \Rightarrow (\forall x \in A.\, ((P\,x \Rightarrow r) \Rightarrow r) […] [Original post on mathstodon.xyz]

There are several postdoctoral positions available at the Faculty of mathematics and physics, University of Ljubljana, as well as at the Institute for mathematics, physics and mechanics. We are looking for researchers with strong interest in working in any of the following areas: * machine […]