How are academics going to assess AI-coauthored research for appointment and promotion?
“Erdos problem #728 was solved more or less autonomously by AI”
71–80 of 385 posts
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#72It took Andrew Wiles 7 years of intense work to solve Fermat's Last Theorem. The METR institute predicts that the length of tasks AI agents can complete doubles every 7 months. We should expect it to take until 2033 before AI solves Clay Institute-level problems with 50% reliability.
There is an ongoing effort to formalize a modern, streamlined proof of FLT in Lean, with all the needed prereqs. It's estimated that it will take approx. 5 years, but perhaps AI will lead to some meaningful speedup.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#73Earlier quoted context omitted.
Please don't respond to a bad comment by breaking the site guidelines yourself. That only makes things worse. https://news.ycombinator.com/newsguidelines.html
[flagged]
What scientific field do you reckon the regular usage of LLMs falls under? Do you genuinely think Tao was making scientific claims or just provided evidence that may eventually feed into some? It reads to me like just a plain recollection of events, an anecdotal experience.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#74Reconfiguring existing proofs in ways that have been tedious or obscured from humans, or using well framed methods in novel ways, will be done at superhuman speeds, and it'll unlock all sorts of capabilities well before we have to be concerned about AGI. It's going to be awesome to see what mathematicians start to do with AI tools as the tools become capable of truly keeping up with what the mathematicians want from…
> Reconfiguring existing proofs in ways that have been tedious or obscured from humans, To a layman, that doesn't sound like very AI-like? Surely there must be a dozen algorithms to effectively search this space already, given that mathematics is pretty logical?
Define laymen here
The fact of how you use the term AI tells me that you are a representative of laymen so what precisely are you trying to define?
It might be helpful to understand the term artificial intelligence first:
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#75You can try out Aristotle yourself today https://aristotle.harmonic.fun/ . No more waitlist!
This deserves a HN thread in its own right! Do you want to submit it and email hn@ycombinator.com so we can put it in the SCP (https://news.ycombinator.com/item?id=26998308)?
Edit: I just realized from https://news.ycombinator.com/item?id=46296801 that you're the CEO! - in that case maybe you, or whoever you think most appropriate from your organization, could submit it along with a text description of what it is, and what is the easiest and/or most fun way to try it out?
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#76Based on Tao’s description of how the proof came about - a human is taking results backwards and forwards between two separate AI tools and using an AI tool to fill in gaps the human found? I don’t think it can really be said to have occurred autonomously then? Looks more like a 50/50 partnership with a super expert human one the one side which makes this way more vague in my opinion - and in line with my own AI test…
You're understanding correctly, this is back and forth between Aristotle and ChatGPT and a (very smart) user.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#77Reconfiguring existing proofs in ways that have been tedious or obscured from humans, or using well framed methods in novel ways, will be done at superhuman speeds, and it'll unlock all sorts of capabilities well before we have to be concerned about AGI. It's going to be awesome to see what mathematicians start to do with AI tools as the tools become capable of truly keeping up with what the mathematicians want from…
If this isn't AGI, what is? It seems unavoidable that an AI which can prove complex mathematical theorems would lead to something like AGI very quickly.
The "G" in "AGI" stands for "General".
While quickly I noticed that my pre-ChatGPT-3.5 use of the term was satisfied by ChatGPT-3.5, this turned out to be completely useless for 99% of discussions, as everyone turned out to have different boolean cut-offs for not only the generality, but also the artificiality and the intelligence, and also what counts as "intelligence" in the first place.
That everyone can pick a different boolean cut-off for each initial, means they're not really booleans.
Therefore, consider that this can't drive a car, so it's not fully general. And even those AI which can drive a car, can't do so in genuinely all conditions expected of a human, just most of them. Stuff like that.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#78Earlier quoted context omitted.
If you think "transformer" = LLM, you don't understand the basic terminology of the field. This is like calling AlphaFold an LLM because it uses a transformer.
No, it isn't. They call out ExIt as an inspiration as well as AlphaZero, and the implementation of these things (available in many of their authors' papers) is almost indistinguishable from LLMs. The architecture isn't novel, which is why this paper is about the pipeline instead of about any of the actual processing tools. Getting prickly about meaningless terminology differences is definitely your right, but for any…
Equating LLMs and transformers is not a meaningless terminology difference at all, Aristotle is so different from the things people call LLMs in terms of training data, loss function, and training that this is a grievous error.
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#79Can anyone with specific knowledge in a sophisticated/complex field such as physics or math tell me: do you regularly talk to AI models? Do feel like there's anything to learn? As a programmer, I can come to the AI with a problem and it can come up with a few different solutions, some I may have thought about, some not. Are you getting the same value in your work, in your field?
I work in quantum computing. There is quite a lot of material about quantum computing out there that these LLMs must have been trained on. I have tried a few different ones, but they all start spouting nonsense about anything that is not super basic. But maybe that is just me. I have read some of Terence Tao's transcripts, and the questions he asks LLMs are higher complexity than what I ask. Yet, he often gets reason…
"I don't yet know how I can get these tools to do better."
I have wondered if he has access to a better model than I, the way some people get promotional merchandise. A year or two ago he was saying the models were as good as an average math grad student when to me they were like a bad undergrad. In the current models I don't get solutions to new problems. I guess we could do some debugging and try prompting our models with this Erdos problem and see how far we get. (edit: Or maybe not; I guess LLMs search the web now.)
Re: “Erdos problem #728 was solved more or less autonomously by AI”
#80Based on Tao’s description of how the proof came about - a human is taking results backwards and forwards between two separate AI tools and using an AI tool to fill in gaps the human found? I don’t think it can really be said to have occurred autonomously then? Looks more like a 50/50 partnership with a super expert human one the one side which makes this way more vague in my opinion - and in line with my own AI test…
Is a good economic decision to hype a bit the importance of the LLM$.