Are you kidding? This is an incredible result. Stuff like this is the most important stuff happening in AI right now. Automated theorem proving? It's not too far to say the entire singular point of the technology was to get us to this.

▲ dang an hour ago | parent | next [-]

(We detached this subthread from https://news.ycombinator.com/item?id=46094763.)

▲ ares623 17 hours ago | parent | prev | next [-]

This is me being snarky and ignorant, but if it solved one problem and it is automated what’s stopping it from solving all the others? That’s what’s ultimately being sold by the tweet right.

	▲	ComplexSystems 9 hours ago \| parent \| next [-]
		Ultimately the main thing that will stop it from solving literally "all the others" are things like the impossibility of solving the halting problem, considerations like P ≠ NP, etc. But as we have just seen, despite these impossibility theorems, AI systems are still able to make substantive progress on solving important open real-world problems.
	▲	aeve890 14 hours ago \| parent \| prev [-]
		>This is me being snarky and ignorant, but if it solved one problem and it is automated what’s stopping it from solving all the others? Yeah that's the crux of the matter. How do AI did it? Using already existing math. If we need new math to prove Collatz, Goldbach or Riemman, LLMs are simply SOL. That's what's missing and hype boys always avoid to mention.

▲ BanditDefender 16 hours ago | parent | prev [-]

I think it is way too far to say that!

We've had automated theorem proving since the 60s. What we need is automated theorem discovery. Erdős discovered these theorems even if he wasn't really able to prove them. Euler and Gauss discovered a ton of stuff they couldn't prove. It is weird that nobody considers this to be intelligence. Instead intelligence is a little game AI plays with Lean.

AI researchers keep trying to reduce intelligence into something tiny and approachable, like automated theorem proving. It's easy: you write the theorem you want proven and hope you get a proof. It works or it doesn't. Nice and benchmarkable.

Automated axiom creation seems a lot harder. How is an LLM supposed to know that "between any two points there is a line" formalizes an important property of physical space? Or how to suggest an alternative to Turing machines / lambda calculus that expresses the same underlying idea?

▲ ComplexSystems 9 hours ago | parent | next [-]

> We've had automated theorem proving since the 60s.

By that logic, we've had LLMs since the 60s!

> What we need is automated theorem discovery.

I don't see any reason you couldn't train a model to do this. You'd have to focus it on generating follow-up questions to ask after reading a corpus of literature, playing around with some toy examples in Python and making a conjecture out of it. This seems much easier than training it to actually complete an entire proof.

> Erdős discovered these theorems even if he wasn't really able to prove them. Euler and Gauss discovered a ton of stuff they couldn't prove. It is weird that nobody considers this to be intelligence.

Who says they don't? I wouldn't be surprised if HarmonicMath, DeepMind, etc have also thought about this kind of thing.

> Automated axiom creation seems a lot harder. How is an LLM supposed to know that "between any two points there is a line" formalizes an important property of physical space?

That's a good question! It would be interesting to see if this is an emergent property of multimodal LLMs trained specifically on this kind of thing. You would need mathematical reasoning, visual information and language encoded into some shared embedding space where similar things are mapped right next to each other geometrically.

	▲	AdieuToLogic 39 minutes ago \| parent \| next [-]
		>> We've had automated theorem proving since the 60s. > By that logic, we've had LLMs since the 60s! From a bit earlier[0], actually: `Progressing to the 1950s and 60s We saw the development of the first language models.` Were those "large"? I'm sure at the time they were thought to be so. 0 - https://ai-researchstudies.com/history-of-large-language-mod...
	▲	BanditDefender 9 hours ago \| parent \| prev [-]
		[dead]

▲ kvemkon 14 hours ago | parent | prev [-]

> What we need is automated theorem discovery.

I've been thinking mathematicians have fun doing math, making discoveries, crafting proofs.

Does Tour de France & Co. make no sense since small, lightweight and powerful e-bicycles appeared?

Using computer as a helper like bicycles is one thing, using LLMs seems more like e-bicycle and is something another.