Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

3K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

Andrej Bauer

I tried 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)

Google NotebookLM
notebooklm.googleGoogle NotebookLM | Note Taking & Research Assistant Powered by AIUse the power of AI for quick summarization and note taking, NotebookLM is your powerful virtual research assistant rooted in information you can trust.
Jan 13, 2025, 04:19 PM·Public·Web
39boosts·44favorites
Public *
Andrej Bauer

The first example was the paper 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)

arXiv logo
arXiv.orgComodule Representations of Second-Order FunctionalsWe develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show how the notion of comodule representability naturally subsumes classic representations of continuous functionals with well-founded trees. We find other kinds of representations by varying the monad, the comodule, and in some cases the underlying category of containers. Examples include uniformly continuous or finitely supported functionals, functionals querying their arguments precisely once, or at most once, functionals interacting with an ambient environment through computational effects, as well as functionals trivially representing themselves. Many of these rely on our construction of a monad on containers from a monad on shapes and a weak Mendler-style monad algebra on the universe for positions. We show that comodule representability on the category of propositional containers, which have positions valued in a universe of propositions, is closely related to instance reducibility in constructive mathematics, and through it to Weihrauch reducibility in computability theory.
Public *
Andrej Bauer

The second examples was the paper 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)

arXiv logo
arXiv.orgThe Countable RealsWe construct a topos in which the Dedekind reals are countable. To accomplish this, we first define a new kind of toposes that we call parameterized realizability toposes. They are built from partial combinatory algebras whose application operation depends on a parameter, and in which realizers operate uniformly with respect to a given parameter set. Our topos is the parameterized realizability topos whose realizers are oracle-computable partial maps, with oracles serving as parameters and ranging over the representations of a non-diagonalizable sequence, discovered by Joseph Miller. It is a sequence of reals in $[0,1]$ that is non-diagonalizable in the sense that any real in $[0,1]$ that is oracle-computable, uniformly in oracles representing the sequence, must already appear in the sequence. The Dedekind reals are countable in the topos because the non-diagonalizable sequence appears in it as an epimorphism. The topos is intuitionistic, as it invalidates both the law of excluded middle and the axiom of countable choice. The Cauchy reals are uncountable. The Hilbert cube is countable, from which Brouwer's fixed-point theorem follows as an easy corollary of Lawvere's fixed-point theorem. From the 1-dimensional Brouwer's fixed-point theorem we obtain the intermediate value theorem and the lesser limited principle of omniscience. The Kreisel-Lacombe-Shoenfield-Tseitin theorem stating that all real-valued maps are continuous is valid, because the usual proof is uniform with respect to oracles. Lastly, the closed interval $[0,1]$, being countable, can trivially be covered by a sequence of open intervals whose lengths add up to any prescribed $0 < ε< 1$, and such a cover has no finite subcover. However, we show that any sequence of open intervals with rational endpoints covering $[0,1]$ must has a finite subcover.
Public
unnick :verified_mlm:​:vp:

@andrejbauer seems like you accidentally copied the same url twice. whats the correct url? i wanna read the paper

Public
Andrej Bauer

@unnick Oops, sorry, I fixed it, and it's arxiv.org/abs/2404.01256

arXiv logo
arXiv.orgThe Countable RealsWe construct a topos in which the Dedekind reals are countable. To accomplish this, we first define a new kind of toposes that we call parameterized realizability toposes. They are built from partial combinatory algebras whose application operation depends on a parameter, and in which realizers operate uniformly with respect to a given parameter set. Our topos is the parameterized realizability topos whose realizers are oracle-computable partial maps, with oracles serving as parameters and ranging over the representations of a non-diagonalizable sequence, discovered by Joseph Miller. It is a sequence of reals in $[0,1]$ that is non-diagonalizable in the sense that any real in $[0,1]$ that is oracle-computable, uniformly in oracles representing the sequence, must already appear in the sequence. The Dedekind reals are countable in the topos because the non-diagonalizable sequence appears in it as an epimorphism. The topos is intuitionistic, as it invalidates both the law of excluded middle and the axiom of countable choice. The Cauchy reals are uncountable. The Hilbert cube is countable, from which Brouwer's fixed-point theorem follows as an easy corollary of Lawvere's fixed-point theorem. From the 1-dimensional Brouwer's fixed-point theorem we obtain the intermediate value theorem and the lesser limited principle of omniscience. The Kreisel-Lacombe-Shoenfield-Tseitin theorem stating that all real-valued maps are continuous is valid, because the usual proof is uniform with respect to oracles. Lastly, the closed interval $[0,1]$, being countable, can trivially be covered by a sequence of open intervals whose lengths add up to any prescribed $0 < ε< 1$, and such a cover has no finite subcover. However, we show that any sequence of open intervals with rational endpoints covering $[0,1]$ must has a finite subcover.
Public
Tristan Nguyen

@andrejbauer About a year ago, I asked ChatGPT to summarize a White House Executive Order. I forget what it was. But I gave it the entire name of the Executive Order. Well, approximately 1/4 of ChatGPT's summary was made up. That is, the topics therein did not appear in the Executive Order.

Public
TobyBartels

@andrejbauer : I was surprised by your initial statement that it wouldn't take correction, because what I've seen has been, if anything, too eager to be corrected. But that's based on cases where the user flat-out tells the LLM (truthfully or otherwise) that it's wrong. Here you're just trying to lead it to *realize* that it's wrong, and that doesn't work (until you tell it so).

Public
Andrej Bauer

@TobyBartels Nope, I actually told it it was wrong and it didn't buckle. I have the session on the brower in my office, I'll post it tomorrow.

Public
TobyBartels

@andrejbauer No ‘I'm sorry for the confusion. The paper is in fact not restricted to finitely-branching trees’? This actually gives me a little more respect for it; in the transcripts I've seen, they'll deferentially believe any nonsense you tell them.

Public
Antonio Patriarca

@andrejbauer But even if it was good, why would I speak to it instead of my coworkers or colleagues? Maybe I am just growing old and jaded against AI tools, but I don't see the use cases of most of them.

Public *
Andrej Bauer

@antopatriarca Because if it were good you could tell it to read 10000 papers and tell you which ones are relevant for the problem you're trying to solve.

Public
Tom_Drummond

@andrejbauer @antopatriarca I am very concerned about the problem of what happens when time-poor reviewers use this as a tool to help them. My studens have already had to deal with a number of AI generated reviews and the responses from editors/area chairs so far can best be described as crickets...

Public
Antonio Patriarca

@andrejbauer Is that a real or hypothetical scenario? Do you really need to read so many papers to see which ones are related to your problem? In my experience the number of people working on the same problem domain are usually quite limited in number and they all know each other. But maybe I'm biased and it depends on the field. The AI field is surely overcrowded right now. Let's assume we really have that many papers. How many of them are really worth publishing? How many of them are actually saying the same thing with different words? Is this tool actually helping with the real problem (IMHO too many papers) or making it worse?

Public
Andrej Bauer

@antopatriarca It's a realistic scenario, except I won't be the one doing the reading. It's essentially a better Google search engine. The AI should read all papers, and then just tell me which ones I should read.

Public
Antonio Patriarca

@andrejbauer yes, as a search engine could be useful.

Quiet public
J. "Henry" Waugh

@andrejbauer
> [...] an insolent incompetent science journalist. When confronted with its own factual mistakes, it tries to blame the paper instead

I needed a laugh today, thank you 😂

Public
Weekend Editor

@andrejbauer

I fed it my blog, and got pretty much the same conclusion. All facts either incorrect or only approximately correct, lots of explicitly stated stuff ignored.

A friend described the "podcast" as "the verbal equivalent of Muzak".

someweekendreading.blog/somewe

www.someweekendreading.blogAn AI-Generated Podcast About This CLBTNR?!
More from Weekend Editor
Public
Andrej Bauer

@weekend_editor Except that Muzak is not out of tune, but the podcast is factually incorrect.

Public
Weekend Editor

@andrejbauer

I think the most dangerous thing about LLMs is that while they are just high-throughput bluffing machines, they are nonetheless artfully and seductively persuasive.

People *believe* them, because they are masters of rhetoric, not of fact.

Metaphorically, the high-pressure BS firehose is painted pretty colors.

SearchLive feeds
About