Andrej Bauer

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

@MartinEscardo I am happy to see that Cécilia Pradic (whose obviously reads these posts but I cannot find the username) has put some real thought into questions about the Myhill Isomorphism theorem and its genralizations: https://arxiv.org/abs/2507.05028

The verdict: it doesn't generalize much […]

@soaproot @jonmsterling The ghost.org web site is giving me all the wrong vibes. They use 50% of available space for useless pictures of successful white male business types, they keep saying how perfect and easy it is, and I would clearly need at least 10 minutes to determine that there is no […]

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 […]

@highergeometer With my hands free, and to explain it to students, I would probably define `ln` as the inverse of `exp`, show that `exp` is strictly increasing, and reduce the problem to `e^0.69 < 2 < e^0.70`. Then it comes down to having good rational bounds for `e`, which we can get from its […]

@highergeometer Using the technology developed by Assia Mahboub, Guillaume Melquiond, and Thomas Sibut-Pinotei in https://inria.hal.science/hal-01630143/file/main.pdf (the problem you posed is a baby example of what they do)

@johncarlosbaez May I forward mine to you?

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.

( […]

@MartinEscardo I can't believe you didn't tell us how many optimal plays there are in tic-tac-toe.

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?

Colin the Mathmo (@ColinTheMathmo@mathstodon.xyz) 29.4K Posts, 7.29K Following, 5.28K Followers · Fulltime freelance provider of outreach and enhancement in maths ... I talk a lot. About maths. I talk about other stuff too, like ballroom dancing, juggling, unicycling, education, engineering, software, and "other things". But mostly about maths. I tend to follow back, but only if you have something in your profile.

@christianp @ColinTheMathmo Thank you for reporting on how the money is spent. People will more easily donate if they know whether the money is going. And I join the others in saying that your time is money, too!

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 […]

@sibrosan @highergeometer @johncarlosbaez Are you quite sure that the ducks exist?

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

@MartinEscardo Hatcher (https://pi.math.cornell.edu/~hatcher/AT/AT+.pdf) gets close to what you want on page 10 when discussing the wedge sum.

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 […]

A Haskell implementation of Myhill's isomorphism theorem A Haskell implementation of Myhill's isomorphism theorem - Myhill.hs

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.

Why is it so difficult to define constructive cardinality? Consider Frege's cardinality and HoTT set-truncation cardinality, both of which can be well-defined in constructive theory (as SetoidTT and CubicalTT, respectively). Why don’t we regard them as well

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