=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
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
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
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
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
How to do synthetic mathematics in ten difficult steps:
@cbaberle @jonmsterling @MartinEscardo @chrisamaphone
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
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
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
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.
=> More informations about this toot | View the thread
=> More informations about this toot | View the thread
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:
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
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.
=> More informations about this toot | View the thread
=> This profile without reblog | Go to andrejbauer@mathstodon.xyz account This content has been proxied by September (ba2dc).Proxy Information
text/gemini