Lightnews — Scholar-powered news

Andrej Bauer

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

92 followers 0 following 54 posts

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

Posts Media Videos Starter Packs

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 16d

This may be Girard's most brilliant contribution to humanity.

https://girard.perso.math.cnrs.fr/mustard/article.html

Untitled Document

girard.perso.math.cnrs.fr

Reposted by Andrej Bauer

Christian Lawson-Perfect @christianp.mathstodon.xyz.ap.brid.gy · 16d

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

finance [mathstodon.xyz wiki]

wiki.mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 22d

@MartinEscardo
> To give a trivial example, if you hover over link in Firefox, you see its url, and this is not available in Safari.

Use "View → Hide/Show status bar" to enable Status bar, then when you hover on a link the URL appears at the bottom.

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 24d

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 · 26d

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.

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · 26d

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

Reposted by Andrej Bauer

theHigherGeometer @highergeometer.mathstodon.xyz.ap.brid.gy · Aug 18

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Sep 2

[Spoilers!]

@highergeometer Let C = {-1,0,1}^ℕ be the ternary Cantor space and D = {-1, 0, 1} the Davey space. Define f : C → D by

f(α) := if ∃ n . f α = 0 then 0 else (limsup_n α(n)).

In words; if α contains a 0 then f(α) = 0, otherwise if α attains 1 infinitely often then f(α) = 1 […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Aug 26

@highergeometer Who first detached received meaning from concepts such as number, bigness, and quantity? Who was the first formalist?

It wasn't Euclid, for he defines a point is that which has no parts. (Is that an irreducible closed set?)

It wasn't Russell, although he came close to it […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Aug 22

@dougmerritt @MartinEscardo Actually, nonstandard analysis is not what physicists need. They use nilpotent infinitesimals, which are not available in nonstandard analysis.

It is the synthetic differential geometry, as developed by Dobus, Kock, Lawvere and others, that does the job.

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Aug 21

@MartinEscardo I would venture to say that mathematicians naturally do make the distinction, but the intuition is defeated by formal education, when they're told that "existence is ∃". The problem isn't even what ∃ is – but simply that they're taught *only one* notion of formal existence.

P.S […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Aug 21

@MartinEscardo I prefer to call (2) "abstract eistence".

In practice, mathematicans operate with the distinction between concrete and abstract existence, but they're never thought the distinction formally because they're told first-order logic is The One True Way.

This situation is akin to […]

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Aug 20

Has anyone ever actually seen Kleene's T predicate?

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Aug 16

Emacs 30.1 freezing on MacOS 15.5 (Intel MacBookPro) is getting a bit tiresome.

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jul 21

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

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jul 10

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jul 9

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jul 6

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

Reposted by Andrej Bauer

Martin Escardo @martinescardo.mathstodon.xyz.ap.brid.gy · Jun 21

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jun 21

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

Original post on mathstodon.xyz

Reposted by Andrej Bauer

Martin Escardo @martinescardo.mathstodon.xyz.ap.brid.gy · Jun 17

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jun 16

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · Jun 16

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · May 29

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

Original post on mathstodon.xyz

Andrej Bauer @andrejbauer.mathstodon.xyz.ap.brid.gy · May 29

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