iiinova — where your digital self keeps evolving

Andrej Bauer

@andrejbauer.mathstodon.xyz.ap.brid.gy

124 followers 0 following 85 posts

Professor of computational mathematics at University of Ljubljana, Slovenia. [bridged from mathstodon.xyz/@andrejbauer on the fediverse by fed.brid.gy ]

Posts Replies Media

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 01/10/2026

The new scarce resource is "thinking at human speed".

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 24/09/2026

Is it too late or too early to teach undergraduate math students how to prove original results in math, with the help of thoes who shall not be named? It our department the basic requirement for a MSc thesis does not require original research (sensibly), but I wonder if we're past that point […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 16/09/2026

Having done bidding for papers at the next Certified Proofs and Programs (CPP), I have this to say: "Formalization of X in Y" isn't gonna cut it anymore. When calculators first came out, did people try to publish "We computed √(5 + log 2) to 15 decimals"?

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 19/08/2026

@jeanas The bug is not really fixed because the kernel still does the wrong thing when deciding whether projections are allowed. The rule seems to be "if it's not in Prop then we may project", but it should be "if it is in Type i for i > 0 then we may project". Not only is this mathematically […]

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 17/08/2026

@highergeometer Resistance is futile. You will be assimilated.

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 08/08/2026

Was Brouwer an impredicativist or not?

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 24/07/2026

@jeanas doi.org/10.2307/2275292 doi.org/10.2307/2275292 dx.doi.org/10.3217/jucs-011-12-2076 www.jstor.org/stable/27590337 doi.org/10.1007/s00153-005-0291-1 doi.org/10.1007/3-540-45793-3_7 doi.org/10.2178/jsl/1230396756 Let me know […]

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 24/07/2026

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 24/07/2026

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 20/07/2026

#FLOC2026 not going so well.

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 19/07/2026

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

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 18/07/2026

@dpiponi en.wikipedia.org/wiki/Balut_(food)

en.wikipedia.org

Balut (food) - Wikipedia

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 18/07/2026

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

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 15/07/2026

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: www.andrej.com/assets/slides/topolo… I did get a bunch of […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 12/07/2026

@jeanas Not the bit where I am wrestling with some AI and always falling for it’s promises it will do the right thing. But the stuff about using databases of math to improve AI, and also figuring out how to formally verifies gigabytes-sized math databases - I think that’s cool. It pushes the […]

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 11/07/2026

Something to ruffle your feathers: math.andrej.com/2026/07/11/making-a…

math.andrej.com

Mathematics and Computation | Making AI smarter with AI

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 29/06/2026

@jeanas @ncf Uhm, that's not what people who remember living in the second millenium mean by "parallel or". But still a nice question.

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 29/06/2026

@jeanas @ncf How do you specify parallel or in type theory?

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 22/06/2026

Human or AI?

C : Carrier
x✝¹ : (Γ : Shape C) ×'
(Λ : Shape C) ×'
(Θ : Shape C) ×'
(Ψ : Shape C) ×'
(Ω : Shape C) ×'
(Φ : Shape C) ×'
(Χ : Shape C) ×'
(_ : Proper Λ) ×'
(_ : Proper Θ) ×'
(_ : Proper Ψ) ×'
(_ : Proper Ω) ×'
(_ : Proper Φ) ×'
(_ : Proper Χ) ×'
(_ : Subst Ψ (Γ ⋈ Θ ⋈ Ω)) ×' (_ : Subst Λ (Γ ⋈ Θ ⋈ Ψ ⋈ Φ)) ×' Expr (Γ ⋈ Λ ⋈ Χ) ⊕'
(Γ : Shape C) ×'
(Δ : Shape C) ×'
(Ξ : Shape C) ×'
(Θ : Shape C) ×'
(Ψ : Shape C) ×'
(Ω : Shape C) ×'
(_ : Proper Δ) ×'
(_ : Proper Ξ) ×'
(_ : Proper Θ) ×'
(_ : Proper Ψ) ×'
(_ : Proper Ω) ×'
(_ : Subst Δ (Γ ⋈ Ξ)) ×'
(_ : Subst Ψ (Γ ⋈ Δ ⋈ Θ ⋈ Ω)) ×' (Φ : Shape C) ×' (_ :

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 17/06/2026

@jeanas @iblech @jameshanson @MartinEscardo In realizability over ITTM the Cauchy reals are sequence-avoiding (and thus uncountable) and at the saem time subcountable (embed into ℕ). They also coincide with the Dedekind reals there. I do not know if they can be countable. However, any setting […]

Original post on mathstodon.xyz

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 13/06/2026

@jeanas Hmm, I was afraid of that. The naive attempt would be this: a family indexed by an object (X, ∼) is a map A : X → Obj(Eff). The problem is that morphisms aren't functions, so reindexing along a morphism r : (Y, ≈) → (X, ∼) isn't just A ∘ r. In contrast, this works for assemblies, where […]

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 12/06/2026

@jeanas For assemblies uniform families definitely work. For the topos I do not know of the top of my head, but look at Lars Birkedal's PhD thesis.

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 30/04/2026

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?

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 28/04/2026

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 21/04/2026

So after some suffering it turns out that the main culprit is jupter-book version 2, which has nothing to do with version 1. Someone has a sick sense of humor when it comes to naming software. Reverting back to version 1 made life much easier (and also non-dependent on typst).

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 20/04/2026

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

Original post on mathstodon.xyz

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 14/04/2026

Claude and I are in business! math.andrej.com/2026/04/14/claude-a…

math.andrej.com

Mathematics and Computation | Claude and I

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 11/04/2026

@wtgowers Close, close, but not quite there.

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 10/04/2026

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

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 08/04/2026

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? youtu.be/sbQi6HjyBHM

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 02/04/2026

Y'all notice the date on that was April 1, right?

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 01/04/2026

(contd.) Note further that for any such path α and any k ∈ ℕ we have (∃ n . Prf(k, n)) ⇒ αₖ = 1. Indeed, if there is n such that Prf(k, n) then from a := [α₀, ..., aₙ] ∈ T follows αₖ = aₖ = 1. Moreover, since α is Turing-computable by some x ∈ ℕ, as above, Peano arithmetic proves (∃ n […]

Original post on mathstodon.xyz

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 01/04/2026

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

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 23/03/2026

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

Savory Rice Casserole with Grasshoppers, Cracklings & Gorgonzola (Honey Finish)
Ingredients

453 g cooked basmati (cold)
120–150 g edible grasshoppers (cleaned)
60–80 g pork cracklings
3 eggs, separated
50 g semolina, 150 ml water
30 g butter (plus for pan) or 2 tbsp oil
80–100 g Gorgonzola dolce, in 1–1.5 cm cubes
Salt, pepper; optional pinch paprika/chili
Breadcrumbs for pan; Finish: 1–2 tbsp honey

Method

Heat oven 180 °C; grease and breadcrumb a baking dish.
Dry‑toast grasshoppers 3–5 min (or 160 °C for 8–10 min); season lightly. Crisp cracklings if needed.
Boil 150 ml water + pinch salt; whisk in 50 g semolina, cook 3–4 min very thick; stir in 30 g butter. Cool to warm.
Whisk yolks with seasoning → stir in warm semolina → fold in rice + 2/3 grasshoppers + 2/3 cracklings.
Beat whites to stiff peaks; gently fold in. Fold in Gorgonzola last (keep cheese pockets).
Spread in pan; top with remaining insects/cracklings; dot with butter/oil. Bake 30–35 min until set and golden. Rest 10 min.
Finish: drizzle 1–2 tbsp honey just before serving.

Go easy on salt—cracklings & Gorgonzola are salty.

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 22/03/2026

Have you not seen this? youtu.be/BKorP55Aqvg

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 25/02/2026

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 22/02/2026

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

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 31/12/2025

@MartinEscardo I was hoping you'd say "modalities" 🙂

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 31/12/2025

@MartinEscardo How would you quantify the amount of information or constructivity?

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 27/12/2025

@de_Jong_Tom Make the best of it: "I am sorry but I don't know what email you're talking about. My university disposes of email after 90 days to preserve disk space."

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 18/12/2025

I said too much, both in terms of content and length. www.typetheoryforall.com/episodes/c…

typetheoryforall.com

Type Theory Forall

Type Theory much beyond inference rules

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 21/11/2025

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

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 19/11/2025

@highergeometer Lawvere's fixed point theorem is a favorite of mine. Did you know Lawvere in his original paper did not present any non-trivial examples of it? He used it in the contra-positive form only "If f : B → B has no fixed points then e : A → B^A is not a surjection". When I looked for […]

Original post on mathstodon.xyz

000

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 16/11/2025

@MartinEscardo I teach mappings by first saying that they are "rules", i.e., λ-abstractions, except we write them using x ↦ ... A bit later, when we discuss definitions, I explain definite descriptions "the unique x ∈ A such that φ(x)", written using Russell's notation ι(x ∈ A). φ(x). Still a […]

Original post on mathstodon.xyz

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 11/11/2025

RE: mathstodon.xyz/@egbertrijke/1155280… 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 […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 20/10/2025

@highergeometer Why did they have to call it "electromagnetism" when all the time it was just a connection on a U₁(1) bundle?

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 22/09/2025

This may be Girard's most brilliant contribution to humanity. girard.perso.math.cnrs.fr/mustard/a…

girard.perso.math.cnrs.fr

Untitled Document

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 15/09/2025

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 12/09/2025

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.

100

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 12/09/2025

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

Original post on mathstodon.xyz