Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

“Erdos problem #728 was solved more or less autonomously by AI”

mathstodon.xyz

Post reply on HN
Print view View original

131–140 of 385 posts

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#131

Post by feastingonslop »

falcor84 wrote: post #125
markusde wrote: post #100

Earlier quoted context omitted.

Yes, the contributions of the people promoting the AI should be considered, as well as the people who designed the Lean libraries used in-the-loop while the AI was writing the solution. Any talk of "AGI" is, as always, ridiculous. But speaking as a specialist in theorem proving, this result is pretty impressive! It would have likely taken me a lot longer to formalize this result even if it was in my area of specialty…

> Any talk of "AGI" is, as always, ridiculous. How did you arrive at "ridiculous"? What we're seeing here is incredible progress over what we had a year ago. Even ARC-AGI-2 is now at over 50%. Given that this sort of process is also being applied to AI development itself, it's really not clear to me that humans would be a valuable component in knowledge work for much longer.

Excellent! Humans can then spend their time on other activities, rather than get bogged down in the mundane.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#132

Post by TeMPOraL »

XCSme wrote: post #114
TeMPOraL wrote: post #95

Earlier quoted context omitted.

> Aristotle integrates three main components (...) The second one being backed by a model. > It is far more than an LLM It's an LLM with a bunch of tools around it, and a slightly different runtime that ChatGPT. It's "only" that, but people - even here, of all places - keep underestimating just how much power there is in that. > math != "language". How so?

I kind of agree, "math" can be a "language". Same as "images" can be a language. You can use anything as tokens.

That's true, and a good fundamental point. But here it's much simpler than that: math is a language the same way code is, and if there's one thing LLMs excel at, it's reading and writing code and translating back and forth between code and natural language.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#133

Post by pvillano »

maxwells-daemon wrote: post #122

I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling. - Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here. - Once a pr…

Is anyone working on applying these techniques to formal verification of software?

My limited understanding of Rust is that it applies a fixed set of rules to guarantee memory safety. The rules are somewhat simple and limiting, for ease of understanding and implementation, but also because of undecidability.

Programmers run into situations where they know that their code won't cause memory errors, but it doesn't follow the rules. Wouldn't it be cool if something like Aristotle was integrated into the compiler? Any code for which a proof of correctness could be written would pass/compile, without having to add more and more rules

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#134

Post by TeMPOraL »

D-Machine wrote: post #106
TeMPOraL wrote: post #95

Earlier quoted context omitted.

> Aristotle integrates three main components (...) The second one being backed by a model. > It is far more than an LLM It's an LLM with a bunch of tools around it, and a slightly different runtime that ChatGPT. It's "only" that, but people - even here, of all places - keep underestimating just how much power there is in that. > math != "language". How so?

Transformer != LLM. See my edited top-level post. Just because Aristotle uses a transformer doesn't mean it is an LLM, just as Vision Transformers and AlphaFold use transformers but are not LLMs. LLM = Large Language Model. Large refers to both the number of parameters (and in practice, depth) of the model, and also implicitly the amount of data used for training, and "language" means human (i.e. written, spoken) lan…

The paper you keep linking literally says they're using a large language model (search for that very string in it).

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#135

Post by zozbot234 »

pfdietz wrote: post #130
zozbot234 wrote: post #72

Earlier quoted context omitted.

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.

What I'm hoping to see is high volume automated formalization of the math literature, with the goal of formalizing (or finding flaws in) the entire thing. And once we have that formalized corpus, it's all set up as training data for moving forward.

We can't really have across-the-board formalization of the math literature without getting the basics done first (including the whole undergrad curriculum) which is what the mathlib folks are working on. It will in fact be interesting to see if AI can meaningfully speed up that work (although they seem to be bottlenecked on review and merging at the moment, not new contribs per se. So a "coding" AI workflow may be a bit of a closer fit.)

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#136

Post by gf000 »

threethirtytwo wrote: post #120
mkl wrote: post #40

Earlier quoted context omitted.

This is very narrow AI, in a subdomain where results can be automatically verified (even within mathematics that isn't currently the case for most areas).

Narrow AI? I’m not saying it’s AGI but this is not a narrow AI it’s a general AI given a narrow problem. ChatGPT.

In a very specialized setup, in tandem with a verifier.

Just because a specialized human placed in an F-16 can fly at Mach 2.0, doesn't mean humans in general can fly.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#137

Post by pfdietz »

epolanski wrote: post #42
ComplexSystems wrote: post #37

Earlier quoted context omitted.

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.

AGI in its standard definition requires matching or surpassing humans on all cognitive tasks, not just in some, especially some where only handful of humans took a stab on.

Since no human could do that, are we to conclude no human is intelligent?

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#138

Post by Legend2440 »

xorcist wrote: post #51
observationist wrote: post #2

Reconfiguring 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?

The issue with traditional logic solvers ('good old-fashioned AI') is that the search space is extremely large, or even infinite.

Logic solvers are useful, but not tractable as a general way to approach mathematics.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#139

Post by sponnath »

leggothrow wrote: post #46

This almost implies mathematicians aren’t some ungodly geniuses if something as absolutely dumb as an LLM can solve these problems via blind pattern matching. Meanwhile I can’t get Claude code to fix its own shit to save my life.

There are "ungodly geniuses" within mathematics but no one is saying every mathematician is an "ungodly genius". The quality of results you get from an LLM can vary greatly depending on the environment you place it in and the context you provide it. This isn't to say it's your fault Claude Code can't fix whatever issue you're having.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#140

Post by pfdietz »

D-Machine wrote: post #29
lwansbrough wrote: post #14

Can 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 do / have done research in building deep learning models and custom / novel attention layers, architectures, etc., and AI (ChatGPT) is tremendously helpful in facilitating (semantic) search for papers in areas where you may not quite know the magic key words / terminology for what you are looking for. It is also very good at linking you to ideas / papers that you might not have realized were related. I also found i…

Apropos your account name, I just wanted to mention that I used various Xerox D machines back in the day. They were fun.
Post reply on HN