231–240 of 310 posts
Earlier quoted context omitted.
The model has multiple layers of mechanisms to prevent carbon copy output of the training data.
forgive the skepticism, but this translates directly to "we asked the model pretty please not to do it in the system prompt"
A surprising % of these LLM proofs are coming from amateurs. One wonders if some professional mathematicians are instead choosing to publish LLM proofs without attribution for career purposes.
It's probably from the perennial observation "This LLM is kinda dumb in the thing I'm an expert in"
Earlier quoted context omitted.
It is still possible a proof from someone else with a similar method was in the training set. A proof that Terence Tao and his colleagues have never heard of? If he says the LLM solved the problem with a novel approach, different from what the existing literature describes, I'm certainly not able to argue with him.
> A proof that Terence Tao and his colleagues have never heard of? Tao et al. didn't know of the literature proof that started this subthread.
Sounds like Lean 4/rocq did all the work here
Earlier quoted context omitted.
There is still value on letting these LLMs loose on the periphery and knocking out all the low hanging fruit humanity hasn’t had the time to get around to. Also, I don’t know this, but if it is a problem on Erdos I presume people have tried to solve it atleast a little bit before it makes it to the list.
Is there though? If they are "solved" (as in the tickbox mark them as such, through a validation process, e.g. another model confirming, formal proof passing, etc) but there is no human actually learning from them, what's the benefit? Completing a list? I believe the ones that are NOT studied are precisely because they are seen as uninteresting. Even if they were to be solved in an interesting way, if nobody sees the…
More broadly, I think there’s a perspective that literally just building out thousands more true statements in Lean is going to keep cementing math’s broadening knowledge framework. This is not building a giant castle a-la Wiles, it’s laying bricks in the outhouse, but someday those bricks might be useful.
Earlier quoted context omitted.
> Did not care enough about erdos... This is bad faith. Erdos was an incredibly prolific mathematician, it is unreasonable to expect anyone to have memorized his entire output. Yet, Tao knows enough about Erdos to know which mathematical techniques he regularly used in his proofs. From the forum thread about Erdos problem 281: > I think neither the Birkhoff ergodic theorem nor the Hardy-Littlewood maximal inequality,…
Isn't it bad faith to say no priors solutions was found when a solution published by erdos was ultimately found by the community in 10 minutes?
It does beg the question, if it was so easy to find the prior solution, why has no one posted it already on the erdos problems website?
Earlier quoted context omitted.
Exactly, you're almost getting it. Hence the value of "pure" research in both science and math.
You are not yet getting it I'm afraid. The point of the linked post was that, even assuming an equal degree of expected uselessness, scientific explanations have intrinsic epistemic value, while proving pure math theorems hasn't.
Instead of addressing any of that you're insisting I'm misunderstanding and pointing me back to a linked comment of yours drawing a distinction between epistemic value of science research vs math research. Epistemic value counts for many things, but one thing it can't do is negate the significance of pure math turning into applied research on account of pure science doing the same.
Earlier quoted context omitted.
Isn't it bad faith to say no priors solutions was found when a solution published by erdos was ultimately found by the community in 10 minutes?
Maybe, that's a decent point. I didn't realize it was that quick, I would have appreciated you mentioning that in your previous comment. It does beg the question, if it was so easy to find the prior solution, why has no one posted it already on the erdos problems website?
Somehow an llm generated proof that consist of gigabytes upon gigabytes of unreadable mess is groundbreaking and pushes mathematics forward, a proof proposed by Erdos himself in 5 pages gets buried and lost to time.
Maybe one particular optics fuels the narrative that formal verified compute is the new moat and llms are amazing at that?
Earlier quoted context omitted.
That might be somewhat ungenerous unless you have more detail to provide. I know that at least some LLM products explicitly check output for similarity to training data to prevent direct reproduction.
Should they though? If the answer to a question^Wprompt happens to be in the training set, wouldn't it be disingenuous to not provide that?
Earlier quoted context omitted.
does it? this is a verbatim quote from gemini 3 pro from a chat couple of days ago: "Because I have done this exact project on a hot water tank, I can tell you exactly [...]" I somehow doubt it an LLM did that exact project, what with not having any abilities to do plumbing in real life...
Isn't that easily explicable as hallucination, rather than regurgitation?