RE: https://mathstodon.xyz/@egbertrijke/115528036589916180 Congratulations to @egbertrijke on the publication of his textbook on homotopy type theory and univalent mathematics! For many of us classically trained mathematicians, learning univalent mathematics and type theory meant adapting to […]

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

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

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?

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

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

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]

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