andrejbauer - Network

Reviewing of math papers takes forever. Is this because math reviewers are expected to be, or think they are, guarantors of correctness? If...

Reviewing of math papers takes forever. Is this because math reviewers are expected to be, or think they are, guarantors of correctness? If not, why does ti take so long?

I am happy to report that project "9. Nyquist-Shannon sampling theorem" has been completed. There is now a Mathlib-based...

I am happy to report that project "9. Nyquist-Shannon sampling theorem" has been completed. There is now a Mathlib-based formalization of the theorem at https://gitlab.com/keremgunes/lean4-sampling-theorem

Before you ask if it's going to be imported into Mathlib: that's not a course requirement, and I suspect it would require a non-trivial amount of additional work to conform to Mathlib, so I don't know.

It's giving me ideas for very interesting exam questions in category theory that would ask the students to appraise a ChatGPT answer and...

It's giving me ideas for very interesting exam questions in category theory that would ask the students to appraise a ChatGPT answer and either confirm it to be correct, or spot the error.

Daily reminder on how good ChatGPT is. I asked it to show me the diagrams for 𝑓 : 𝑇𝐴 → 𝐴 being an algebra for the monad 𝑇.

Daily reminder on how good ChatGPT is. I asked it to show me the diagrams for 𝑓 : 𝑇𝐴 → 𝐴 being an algebra for the monad 𝑇.

I just noticed that synthetic computability is my go-to idea for birthday presents. My paper on fixed-point theorems was for the...

I just noticed that synthetic computability is my go-to idea for birthday presents. My paper on fixed-point theorems was for the Lawvere-Freyd issue of Tbilisi journal https://doi.org/10.1515/tmj-2017-0107, the continuity theorems for Dieter Spreen's issue of Logic & Analysis https://arxiv.org/abs/2307.07830 (why hasn't that been published yet?!), and now @aws and I are cooking up Turing reductions for Jaap van Oosten's symposium in Amsterdam.

So people, if you want to see more progress in synthetic computability, you'll have to celebrate some birthdays.

TIL I made the types.pl logo.

TIL I made the types.pl logo.

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

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)

The first example was the paper https://arxiv.org/abs/2409.17664 on Comodule representations of second-order functionals, co-authored with...

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)

I tried https://notebooklm.google on two papers of mine. It's advertised as "Your Personalized AI Research Assistant". The...

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)

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

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

In the formalization class I am teaching I am doing a class project on formalizing partial combinatory algebras...

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.

I can never remember the formula for the closure operator 𝑗 : 𝖯𝗋𝗈𝗉 → 𝖯𝗋𝗈𝗉 forcing a predicate 𝑃 : 𝐴 →...

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.

There are several postdoctoral positions available at the Faculty of mathematics and physics, University of Ljubljana, as well as at the...

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

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

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.

I am teaching a course on formalized mathematics in Lean (https://www.andrej.com/zapiski/MAT-FORMATH-2024/book/). I let the students pick...

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!

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

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

Here's a challenge: find a description of finite injury priority method, for example Friedberg-Muchnik theorem, which does not use...

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.

An impressive formalization by @rahulc29 of realizability toposes (for total combinatory algebras)...

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.

Discussing the existence property with a very smart master's student resulted in the following epiphany: existence property with...

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.

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

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