Slides with speaker notes for my FSCD talk "Sheaves as oracle computations" are now available. I suspect a video will appear at some point, too. I might write a blog post about the slide on the intermediate value theorem, as it puzzled people during the talk (because the slides is vague) […]

#FLOC2026 not going so well.

Is there a FLOC 2026 Zulip or some such and why not?

Do they have any good food in Lisbon? I hear they catch fish.

I was invited to speak at the Summer Conference on Topology 2026and its Applications in Split, Croatia. This is how I tried to explain the topos of countable reals to ordinary topologists: https://www.andrej.com/assets/slides/topology-in-the-topos-of-countable-reals.pdf I did get a bunch of […]

Something to ruffle your feathers: https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai/

Human or AI?

CLaude and I are having some relationship trouble. It accesses files outside the working folder without tell me, it decides to edit files when I didn't ask for it, and is generally opinioneated. How do I lock it up into a cage?

Claude complained (at length) that I didn't acknowledge it in a paper together with humans, but only separately as software. It was a fine example of emotional blackmail. It then occurred to me that we have a new business model: convince customers that your product is a human being. That's even […]

There is a new brand of software that is really awful. Myst, jupyter-book, typst are three such representatives. Half-made pieces of software with annoying self-advertising on a flashy web site, no documentation, and just overall irritating. An example: I am using jupyter-book for my lecture […]

Claude and I are in business! https://math.andrej.com/2026/04/14/claude-and-i/

When I form a School of Mathematical Phulosophy, anyone who mentions Platonism or Formalism will be made to kneel on dried peas.

This was a fun chat. I see I stated that the rotations of the square form a non-commutative group. What's the proper penance for that? https://youtu.be/sbQi6HjyBHM

In the effective topos Peano arithmetic (assuming it is consistent) defyies Gödel's second incompleteness theorem, which states that Peano arithmetic cannot prove its own consistency. This is made possible by the effective topos validating “everything is computable”. We argue internally in the […]

Copilot just agrees with every damn thing I ask for. I thought I could reach the bottom, but no.

Have you not seen this? https://youtu.be/BKorP55Aqvg

I have improved the LaTeX input method for MacOS for typing ℂ𝒪𝕆λ Mαth symbols. MacOS is incredibly finicky about installing it. I wrote up instructions for Sequoia 15.7.4. If anyone tries it, especially on a different version of MacOS, please let me know how it went (here or via an issue) so […]

I am a legendary influencer, second level! https://gitranks.com/profile/andrejbauer

With apologies for the delay, the recordings of the talks at the Types and Topology Workshop in celebration of @MartinEscardo's 60th birthday (https://tdejong.com/mhe60) are now on YouTube (where available) 📺 https://www.youtube.com/@mhe60/videos (also linked from the workshop webpage) Many […]

I said too much, both in terms of content and length. https://www.typetheoryforall.com/episodes/constructivism-and-computational-content

A new generation has arrived. The other day a freshmen showed me a 10k lines of code in a single file, written by him and an LLM in a week. It uses machine learning to find small boolean formulas that match a given truth table. A freshman. 10000 lines of code in main.py. It works. Oh yeah, and […]

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

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

Has anyone ever actually seen Kleene's T predicate?

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

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