Toots for andrejbauer@mathstodon.xyz account

Written by Andrej Bauer on 2025-01-13 at 16:19

The second examples was the paper https://arxiv.org/abs/2404.01256 on countable reals, co-authored with James Hanson. Here the AI told me that both exacluded middle and the axiom of choice are needed to carry out Cantor's diagonal argument. When I asked whether it meant "and" or "or", it doubled down and claimed the authors of the paper claim both are needed. I asked for the specific quote from the paper, and received one that used the word "or". I pointed out to the AI that that is clearly an "or", and it responded by blaiming the authors for making the mistake of interpreting "or" as an "and". Again it took a couple more iterations to get things straight.

LLMs may be good for some things, but extracting factually correct summaries from scientific papers isn't one of them. (3/3)

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2025-01-13 at 16:19

The first example was the paper https://arxiv.org/abs/2409.17664 on Comodule representations of second-order functionals, co-authored with Danel Ahman. The AI told me that the paper restricted to representations to only finitely-branching trees. When asked to cite the place in the paper where such a restriction is enforced, it said that finite branching is "strongly implied" by the requirement that the trees must be well-founded. Then I confronted it with the fact that the introduction gives the example of countably branching trees, so clearly the authors did not intend finite branching. The response was that the authors misrepresented their work by giving such an example. When forcilby told that it was wrong, the AI eventually admitted its initial summary of the paper was incorrect. (2/3)

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2025-01-13 at 16:19

I tried https://notebooklm.google on two papers of mine. It's advertised as "Your Personalized AI Research Assistant". The short summary is that the tool is exactly as good as an insolent incompetent science journalist. When confronted with its own factual mistakes, it tries to blame the paper instead. (1/3)

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2025-01-02 at 14:14

How to do synthetic mathematics in ten difficult steps:

1. Take off your programmer's hat – not everything is a language.

2. Put on your mathematician's hat – but keep in mind that language matters.

4. Clear your mind and prepare yourself for mental discipline that will be required for what lies ahead.

3. Pick a mathematical topic.

5. Create a new world of mathematics that tailored to the chosen topic.

6. Relocate into the new world.

7. Learn to speak and think like the indigenous mathematicians.

8. Prove old theorems by new methods.

9. Look for new phenomena, especially those that mathematize what people on the outside experience as folk wisdom.

10. Build a model through which people on the outside can peep in.

@cbaberle @jonmsterling @MartinEscardo @chrisamaphone

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-12-31 at 17:05

In the formalization class I am teaching I am doing a class project on formalizing partial combinatory algebras https://andrejbauer.github.io/partial-combinatory-algebras/ (Isn't it a cool idea that the teacher should also do a class project?)

As expected, the genereralities, such as combinatory completeness, are easy. Defining concrete partial combinatory algebras is a whole different story, though. I got the graph model and the free combinatory algebra, but I shudder at the thought of defining Kleene's first and second algebras.

Is there a Lean formalization of partial recursive functions, with smn and utm theorems? That would be really helpful.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-12-22 at 09:34

I can never remember the formula for the closure operator 𝑗 : 𝖯𝗋𝗈𝗉 → 𝖯𝗋𝗈𝗉 forcing a predicate 𝑃 : 𝐴 → 𝖯𝗋𝗈𝗉 to be true. It is this:

[j(q) = \forall r \in \mathsf{Prop} ., (q \Rightarrow r) \Rightarrow (\forall x \in A., ((P,x \Rightarrow r) \Rightarrow r)) \Rightarrow r]

Would you remember it? I first saw it as a PhD student in a talk by Jaap van Oosten, and had a “wtf” sort of reaction to it, which I still do. I think it shaped my mental image of Jaap (in a good way).

Anyhow, every once in a while I spend 15 minutes looking for it in Jaap's book on realizability, after which I remember it's also in Martin Hyland's paper on the effective topos. The paper is very old, but someone converted it to PDF and it's online, and the formula is in there (see pasted image).

In the hope that the next time I need the formula I will remember I formalized it in Coq (because Agda is predicative and Lean classical), here is the gist: https://gist.github.com/andrejbauer/4f984149fc6694efdbe61b0f9dc55999

All this is doable in HoTT, see @aws's paper on Oracle modalities https://arxiv.org/abs/2406.05818, which has much more than just the homotopy-theoretic construction of the closure operator.

A task worthy of a social network: tell a a story about what the formula is doing. It should explain why (r \mapsto \forall x \in A., (P,x \Rightarrow r)) is the wrong answer.

=> View attached media

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-12-16 at 15:32

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 Andrej.Bauer@fmf.uni-lj.si. Candidates who are specifically interested in machine learning for mathematics are encouraged to also contact Ljupčo Todorovski at ljupco.todorovski@fmf.uni-lj.si.

[#]postdoc #typetheory #machinelearning #job

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-12-12 at 07:46

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.

=> View attached media

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-11-28 at 16:51

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!

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-11-20 at 09:15

I found a construction of a low set that is explained the way I imagine things should be explained in Lecture 38 of Dexter Kozen's book "Theory of Computation" (https://doi.org/10.1007/1-84628-477-5_48).

Still trying to penetrate the "tree method" and "pinball machines".

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-11-19 at 22:17

Here's a challenge: find a description of finite injury priority method, for example Friedberg-Muchnik theorem, which does not use unexplained terminology, contains all the details, is technically correct, and does not say non-sensical things that need to be "understood correctly".

Typical problems:

1. Define the restraint function r(e,s) as something involving A_s, but A_s has not been defined yet (and its definition relies on r).

2. Say things like "now compute r(e,s) for all e". Now? How long will that take?

3. Say "x enters A_{s+1}" without explaining whether A_{s+1} also contains A_s.

4. Use the word "strategy" for two different concepts.

5. Say "choose the least i such that ..." where it is not clear that such an i exists (and in fact it might not). Discuss i for half a page, and only after that explain what to do if i does not exist.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-11-18 at 00:01

An impressive formalization by @rahulc29 of realizability toposes (for total combinatory algebras) https://github.com/rahulc29/realizability. The things undergrads do these days are amazing. I don't want to hear another word about what's wrong with today's youth.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-11-06 at 10:07

Discussing the existence property with a very smart master's student resulted in the following epiphany: existence property with parameters is the same thing as equating ∃ and Σ.

Allow me to explain. The usual existence property states that if a closed statement ∃ (y : B) . φ(y) has a proof, then there is a closed term t : B such that φ(t).

Let "existence property with parameters" be the principle: for any provable statement ∃ (y : B) . φ(x, y), where x : A indicates that parameters are allowed, there is a term t(x) : B such that φ(x, t(x)) has a proof.

Well, if this principle holds then we will be able to show that ∃ (y : B) . φ(y) and Σ (y : B) . φ(y) are equivalent (in an arbitrary context). Indeed, suppose p : ∃ (y : B) . φ(y). By the existence property with parameters there is a term t(p) : B and a proof u(p) : φ(t(p)). The map taking p to (t(p), u(p)) is going to be an equivalence from ∃ (y : B) . φ(y) to Σ (y : B) . φ(y).

(The above argument can be made parametric in B and φ if we let B be a variable ranging over a universe and φ a variable of type B → Prop.)

Probably I just rediscovered something that's already in the HoTT book or TypeTopology or somewhere. I'd be interested in knowing about it.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-10-30 at 20:25

It's a ratio thing: one spider is equivalent to a cloud of flies.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-10-12 at 17:49

After a bit more thinking, the following should be a better version. Suppose 𝐿 is a set of levels and 𝗌𝗎𝖼𝖼 : 𝐿 → 𝐿 an endomap without cycles. Is there a type theory with universes indexed by 𝐿, such that (U_i : U_{\mathsf{succ}(i)}) for all (i \in L)? Once again, each universe should be non-trivial, as described above.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-10-12 at 16:14

Consider an irreflexive transitive relation < on a set L of “levels”. Can we have a type theory with universes ((U_i){i \in L}) such that 𝑈ᵢ : 𝑈ⱼ whenever 𝑖 < 𝑗? Each universe (U_i) should be non-trivial (not contractible) closed under (\Pi{x : A} B(x)) for any (A : U_i) and (B : A \to U_i), and not every type is inhabited.

This sounds like a set-theoretic question.

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-10-11 at 22:01

I asked ChatGPT to give me some witty paper titles.

=> View attached media

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-10-07 at 19:30

@jeanas @tito Fixed: https://github.com/andrejbauer/notes-on-realizability/commit/0a161837161831650750a16cf0eda8636f84a278

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-10-07 at 17:44

@jeanas @tito

The attribution about the discovery of the λ-calculus definition of predecessor in my realizability notes is mistaken (and now it has found its way into https://jean.abou-samra.fr/blog/science-amusante): it was Stephen Klenee, not Alfred Tarski, as documented at the bottom of page 56 of

Stephen C. Klene: Origins of Recursive Function Theory, IEEE Annals of the History of Computing, Jan.-Mar. 1981, pp. 52-67, vol. 3, https://doi.ieeecomputersociety.org/10.1109/MAHC.1981.10004

Let me fix the notes right away.

=> View attached media

=> More informations about this toot | View the thread

Written by Andrej Bauer on 2024-09-27 at 07:17

To blog or not to blog about the paper https://arxiv.org/abs/2409.17664

=> More informations about this toot | View the thread

=> This profile with reblog | Go to andrejbauer@mathstodon.xyz account