RE: odon.xyz/@egbertrijke/115528036589916180" class="hover:underline text-blue-600 dark:text-sky-400 no-card-link" target="_blank" rel="noopener" data-link="bsky">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 […]