Andrej Bauer

Professor of computational mathematics at University of Ljubljana, Slovenia.

web: https://www.andrej.com/
blog: https://math.andrej.com/

Public Key

npub18a63tjqchu08dmrzfs644v3wysydjq4kdqjx2xh66qdx02zk4a9qtkszuj

NIP-05 Address

[email protected]

Profile Code

nprofile1qqsr7ag4eqvt78nka33ycd26kghzgzxeq2mxsfr9rtadqxn84pt27jspz4mhxue69uhhyetvv9ujumn0wd68ytnwv46qzrthwden5te0dehhxtnvdakqzcj5f4

Publishing to

relay.nostr.net

nos.lol

relay.damus.io

Author Public Key

npub18a63tjqchu08dmrzfs644v3wysydjq4kdqjx2xh66qdx02zk4a9qtkszuj

Show more details

Last Notes

2026-03-31 22:23:03 CEST

- reply

Well, it should be obvious, but let me say it anyway.
We need mathematicians of every kind: the thinkers, the dreamers, the formalizers, and even physicists.

2026-03-31 15:48:12 CEST

- reply

Somewhat unexpectedly, I find myself on the same side as @npub1vzx…ncd7 on this one, but for different reasons that @npub1nf4…nqe4 seems to be expounding.
Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty.
Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time in history, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule.
Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each paddling its own foundation, has only contributed to plurality of mathematical thought.
Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @npub14a5…9fse and myself), testifying to their creative potential.
Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is an empty one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.

2026-03-27 00:43:47 CET

- reply

Thanks for humoring me, I appreciate it.
ℝ⁴ to model a small portion of the universe, presumably, not too close to a black hole and such?
It is hard to reconcile the two replies. One tells me fields are sections of bundles, and the other tells me we work with complex Hilbert spaces. What's going on?

2026-03-26 22:14:36 CET

- reply

May we back up a bit (or a lot)?
> 𝔰𝔲(3)⊕𝔰𝔲(2)⊕𝔲(1)-gauge 𝔰𝔬(3,1)-spinor bundle
So we'll work with bundles? Over what? What is their physical meaning? (And it seems like there's a relationship between bundles and fields. Are the fields sections of bundles?)

2026-03-26 22:04:20 CET

- reply

> Would this expansion help @npub18a6…szuj much? I doubt it.
It would not, especially not without a general definition. To my mind, perturbations have no place in the basic conceptual setup, they may at best be technique.
I looked at https://en.wikipedia.org/wiki/Fock_space It's quite low-level from a mathematical point of view. Surely there's a universal property that the Fock space is trying to capture, all those sums seem very computation-oriented (not a suprise).

2026-03-25 20:34:59 CET

- reply

Thanks for the great answer. I knew I couldn't just absorb all of physics, so I'd be quite happy with snippets. I'll have a look at your book!

2026-03-25 09:37:35 CET

- reply

As a mathematician I have always imagined that I would understand the universe if someone described the Standard Model as a really fancy mathematical something-or-other, without saying things like "a neutron is a soup of quarks and anti-quarks" – these just distract from the math.
I only got a snippet of such a story from a physicist once, and I loved it. I asked what a particle really was, mathematically, and he said something like "eigenvector of a linear approximation to some-field-thing". I may be misremembering the "approximation part", but the important thing was that it was a straight mathematical answer. I felt comforted.
Where could I find out more of this? Is the Standard Model a huge vector field on a vector space, or on a manifold with Riemann metric? Can someone write down the type of the Standard Model in in type theory?

2025-10-25 11:44:25 CEST

- reply

A summary for us to revel in, plesase. (Or a link to the relevant portion of the video.)

2025-10-20 21:15:33 CEST

- reply

Wikipedia links U₁(1)-bundle to U(1)-bundle, so I guess they're the same thing.

2025-10-20 10:20:34 CEST

- reply

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

2025-09-12 15:55:39 CEST

- reply

https://media.mathstodon.xyz/media_attachments/files/115/191/660/054/845/470/original/25a99a42c54945f1.png
https://media.mathstodon.xyz/media_attachments/files/115/191/661/116/110/424/original/d6d480bed0989d05.png
https://media.mathstodon.xyz/media_attachments/files/115/191/662/008/854/335/original/bee3abcb2c87499d.png

2025-09-12 15:44:36 CEST

- reply

When I was freshly out of my PhD Mike Wright paid out of his pocket to organize a conference in Firenze and he paid for my travel expenses. He is a true supporter of science. I am gladly repaying a little of his kindness after all these years.

2025-06-16 10:59:59 CEST

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 takes Lean only a moment to formally compute that there are
3734642804542694673304928339684903440360290548300415176063232044682349196517954782034451010203315482100413928177255823637569999967383129500169880004095283194405966596476413742304023127572767115899
distinct colorings of a necklace with 99 beads and 99 colors. See Luka's blueprint for details (and give his repository a star while you're at it).
https://github.com/Luka-O/polya-enumeration-theorem
#Leanprover

2025-05-05 20:09:17 CEST

- reply

Are you quite sure that the ducks exist?

2025-01-28 17:56:39 CET

- reply

You assume nobody will be able to defend against this scenario. The most obvious defense is to make web obsolete and pass to a new form of social connectedness that isn't as easy to control. I am envisioning the members of a tribe drawing on cave walls, but there may be other scenarios.

2024-12-16 16:32:28 CET

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 learning for mathematics
* proof assistants and formalized mathematics
* theoretical and practical aspects of type theory
There is no specific date-limited call for positions, as we are somewhat flexible with starting dates and duration of postdocs. However, we would like to fill the available positions sooner rather than later.
See https://www.fmf.uni-lj.si/en/research/seminar-for-foundations-of-mathematics/ for basic information on the local research group. We are a moderately sized but active and varied group. We seek candidates with some degree of experience in the topics of interest.
Potential candidates should contact me at [email protected]. Candidates who are specifically interested in machine learning for mathematics are encouraged to also contact Ljupčo Todorovski at [email protected].
#postdoc #typetheory #machinelearning #job

2024-12-12 08:46:35 CET

A team of our students made a programmable Christmas tree that is on display at the entrance to the math building.
It's a real feat of engineering and programming, and I am very proud of our students. It has 500 color led lights that are fully programmable. The students wrote software for measuring the xyz coordinates of each light, and made a programmable interface that anyone can use at https://jelka.fmf.uni-lj.si (in Slovenian “jelka” means "fir") to make their own pattern. They wrote a Python library, a Docker interface, and even created a custom Scratch-like visual programming language for controlling the lights. And 3 simulators, as apparently one was not enough. It's all at the web site.
If you are or know a teacher who would like their students to participate, see the contact tab on the web page.
https://media.mathstodon.xyz/media_attachments/files/113/638/709/732/194/367/original/35fdfc77a7e581c0.jpeg

2024-11-28 17:51:26 CET

I am teaching a course on formalized mathematics in Lean (https://www.andrej.com/zapiski/MAT-FORMATH-2024/book/). I let the students pick their own formalization projects, and this is what they've come up with:
1. The tripos-to-topos construction
2. Elementary toposes
3. Kripke models of modal logic
4. (Localic) Stone duality
5. Master theorem https://en.wikipedia.org/wiki/Master_theorem_(analysis_of_algorithms)
6. Wedderburn–Artin theorem https://en.wikipedia.org/wiki/Wedderburn–Artin_theorem
7. Blossoms https://en.wikipedia.org/wiki/Blossom_(functional)
8. Relative monads
9. Nyquist-Shannon sampling theorem https://en.wikipedia.org/wiki/Nyquist–Shannon_sampling_theorem
10. Steiner systems https://en.wikipedia.org/wiki/Steiner_system
11. Pólya enumeration theorem https://en.wikipedia.org/wiki/Pólya_enumeration_theorem
I wonder whether I am a pessimist or they are all optimists. Anyhow, it's going to be fun to watch their blueprints turn green.
P.S. To show the students how it's done, I am doing my own project on partial combinatory algebras https://github.com/andrejbauer/partial-combinatory-algebras It's a race!

2024-09-25 14:44:06 CEST

- reply

Consider a ball on top of a spherical hill. Classical Newtonian dynamics predicts infinitely many solutions for its future trajectories. (It rolls off the hill after any amount of waiting there.) Is the Newtonian world really deterministic?

2024-09-22 09:27:05 CEST

A fascinating read about implementing a solver for quadratic equations. Floating point arithmetic makes it incredibely hard to get it right. Clearly, IEEE 754 is the result of evolution, it could not have been designed.
https://cnrs.hal.science/hal-04116310/document

2024-09-19 08:58:23 CEST

This paper, titled "An Imperative Language for Verified Exact Real-Number Computation", took entirely too long to be written, but I like the end result: https://arxiv.org/abs/2409.11946
It's about programming with exact real number where non-deterministic guarded choice is used to "patch" together partial expressions to give a total one (think "sheaf-style" glueing). And it's not just an idea, it's also implemented using #ocaml 5 effect handlers: https://github.com/andrejbauer/clerical
And Sewon Park also formalized it in Coq. With a bit of polishing, I think the Hoare-style specification logic presented in the paper could give a workable tool in Coq.

2024-08-01 17:12:36 CEST

Of 111 people who answered the question "are logically equivalent statements entirely interchangeable in every situation" https://mathstodon.xyz/@andrejbauer/112881057575938533, 38% answered affirmatively and 62% negatively.
I have found it to be a misconception both by students and mathematicians that A ⇔ B makes A and B "totally the same thing". But this is very much not the case!
As @npub14a5…9fse quipped, if a statement could always be replaced with an equivalent one, one could take a paper and replace all theorems with "True". They are all equivalent to true after all.
Speaking a bit more formally, a statement can be exchanged with an equivalent one so long as we are only concerned with their truth values. However, once we start paying attention to proofs, it becomes clear that the precise form of a statement matters in some situations. A proof p of statement A only becomes a valid proof of an equivalent statement B once we *transport* it along the proof e of equivalence A ⇔ B.
In fact, this sort of phenomenon happens more generally: an element p of a structure A is not itself an element of an isomorphic structure B, but must be mapped to the corresponding element e(p) by an isomorphism e : A → B. Which element we get may depend on which isomorphism e we pick.
(If you are itching to expose the subliminal messages in this post, please don't and just enjoy the fact that you know what my ulterior motives are.)