Can AI do maths yet? Thoughts from a mathematician

Post by Xcelerate » Mon, Dec 23, 2024, 8:13 PM UTC

wbl wrote: post #102

Xcelerate wrote: post #49

So here's what I'm perplexed about. There are statements in Presburger arithmetic that take time doubly exponential (or worse) in the size of the statement to reach via any path of the formal system whatsoever. These are arithmetic truths about the natural numbers. Can these statements be reached faster in ZFC? Possibly—it's well-known that there exist shorter proofs of true statements in more powerful consistent sys…

2 is definitely true. 3 is much more interesting and likely true but even saying it takes us into deep philosophical waters. If every true theorem had a proof in a computationally bounded length the halting problem would be solvable. So the AI can't find some of those proofs. The reason I say 3 is deep is that ultimately our foundational reasons to assume ZFC+the bits we need for logic come from philosohical groundin…

Post by joe_the_user » Mon, Dec 23, 2024, 8:20 PM UTC

obastani wrote: post #176

joe_the_user wrote: post #173

Earlier quoted context omitted.

The reddit thread is ... interesting (direct link[1]). It seems to be a debate among mathematicians some of whom do have access to the secret set. But they're debating publicly and so naturally avoiding any concrete examples that would give the set away so wind-up with fuzzy-fiddly language for the qualities of the problem tiers. The "reality" of keeping this stuff secret 'cause someone would train on it is itself bi…

It's not about training directly on the test set, it's about people discussing questions in the test set online (e.g., in forums), and then this data is swept up into the training set. That's what makes test set contamination so difficult to avoid.

Post by zifpanachr23 » Mon, Dec 23, 2024, 8:38 PM UTC

joe_the_user wrote: post #173

nebulous1 wrote: post #39

There was a little more information in that reddit thread. Of the three difficulty tiers, 25% are T1 (easiest) and 50% are T2. Of the five public problems that the author looked at, two were T1 and two were T2. Glazer on reddit described T1 as "IMO/undergraduate problems", but the article author says that they don't consider them to be undergraduate problems. So the LLM is already doing what the author says they woul…

The reddit thread is ... interesting (direct link[1]). It seems to be a debate among mathematicians some of whom do have access to the secret set. But they're debating publicly and so naturally avoiding any concrete examples that would give the set away so wind-up with fuzzy-fiddly language for the qualities of the problem tiers. The "reality" of keeping this stuff secret 'cause someone would train on it is itself bi…

Post by hyhconito » Mon, Dec 23, 2024, 9:02 PM UTC

binarymax wrote: post #189

hyhconito wrote: post #186

Earlier quoted context omitted.

Let's put it this way, from another mathematician, and I'm sure I'll probably be shot for this one. Every LLM release moves half of the remaining way to the minimum viable goal of replacing a third class undergrad. If your business or research initiative is fine with that level of competence then you will find utility. The problem is that I don't know anyone who would find that useful. Nor does it fit within any exis…

This is a great point that nobody will shoot you over :) But the main question is still: assuming you replace an undergrad with a model, who checks the work? If you have a good process around that already, and find utility as an augmented system, then get you’ll get value - but I still think it’s better for the undergrad to still have the job and be at the wheel, and does things faster and better when leveraging a po…

Post by bambax » Mon, Dec 23, 2024, 9:09 PM UTC

ludwik wrote: post #81

bambax wrote: post #50

> As an academic mathematician who spent their entire life collaborating openly on research problems and sharing my ideas with other people, it frustrates me [that] I am not even to give you a coherent description of some basic facts about this dataset, for example, its size. However there is a good reason for the secrecy. Language models train on large databases of knowledge, so you moment you make a database of mat…

> But if all models were truly open, then we could simply verify what they had been trained on How do you verify what a particular open model was trained on if you haven’t trained it yourself? Typically, for open models, you only get the architecture and the trained weights. How can you reliably verify what the model was trained on from this? Even if they provide the training set (which is not typically the case), yo…