Live data from Hacker News

An OpenAI model has disproved a central conjecture in discrete geometry

openai.com

191–200 of 1001 posts

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#191

As I have stated before, AI will win a fields medal before it can manage a McDonald's A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation. LLMs are just the beginning, we'll see more specialized math AI resembling StockFish soon.

The proof is not written in Lean, though. It’s written in English and requires validation by human experts to confirm that it’s not gibberish.

Yeah, but I wouldn't be surprised if they train the model on verification assisted by Lean

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#192

Earlier quoted context omitted.

what basis do you have for assuming an LLM is fundamentally incapable of doing this?

> what basis do you have for assuming an LLM is fundamentally incapable of doing this? because I have no basis for assuming an LLM is fundamentally capable of doing this.

Except this has been said since the 2010's and has been proven wrong again and again. Clearly the theory that LLM's can't "extrapolate" is woefully incomplete at best (and most likely simply incorrect). Before the rise of ChatGPT, the onus was on the labs to show it was plausible. At this point, I think the more epistemologically honest position is to put the burden back on the naysayers. At the least, they need to admit they were wrong and give a satisfactory explanation why their conceptual model was unable to account for the tremendous success of LLM's and why their model is still correct going forward. Realistically, progress on the "anti-LLM" side requires a more nuanced conceptual model to be developed carefully outlining and demonstrating the fundamental deficiencies of LLMs (not just deficiencies in current LLMs, but a theory of why further advancements can't solve the deficiencies).

Incidentally, similar conversations were had about ML writ large vs. classical statistics/methods, and now they've more or less completely died down since it's clear who won (I'm not saying classical methods are useless, but rather that it's obvious the naysayers were wrong). I anticipate the same trajectory here. The main difference is that because of the nature of the domain, everyone has an opinion on LLM's while the ML vs. statistics battle was mostly confined within technical/academic spaces.

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#193

As I have stated before, AI will win a fields medal before it can manage a McDonald's A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation. LLMs are just the beginning, we'll see more specialized math AI resembling StockFish soon.

> A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation. However, this was not verified in Lean. This was purely plain language in and out. I think, in many ways, this is a quite exciting demonstration of exactly the opposite of the point you're making. Verification comes in when you want to offload checking proofs to computers as well. As it s…

Yeah, but I wouldn't be surprised if they train the model on verification assisted by Lean.

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#194

See the longstanding debate on whether new math is "invented" or "discovered". Most mathematicians I knew thought it's discovered.

Math is an abstraction of reality, it had to be invented, so more inventions or discoveries could be made within it.

The test goes like ‘is our universe, or any other universe, required for the axioms to exist’ and I don’t see how ‘yes’ is a defensible answer.

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#195

To the “LLMs just interpolate their training data” crowd: Ayer, and in a different way early Wittgenstein, held that mathematical truths don’t report new facts about the world. Proofs unfold what is already implicit in axioms, definitions, symbols, and rules. I think that idea is deeply fascinating, AND have no problem that we still credit mathematicians with discoveries. So either “recombining existing material” isn…

"LLMs just interpolate their training data" Cracks me up. What exactly do we think that human brains do?

Maybe the human brain also does other things besides interpolation?

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#196

See the longstanding debate on whether new math is "invented" or "discovered". Most mathematicians I knew thought it's discovered.

Math is an abstraction of reality, it had to be invented, so more inventions or discoveries could be made within it.

What is an abstraction? It is something that arises from human thought and human thought arises from the activity of neurons which are a part of reality. You can't escape reality unless you invoke some form of dualism.

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#197
post #89

See the longstanding debate on whether new math is "invented" or "discovered". Most mathematicians I knew thought it's discovered.

...long standing indeed. It can be traced back to Plato's works.

"The European philosophical tradition consists of a series of footnotes to Plato."

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#198
post #46

As I have stated before, AI will win a fields medal before it can manage a McDonald's A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation. LLMs are just the beginning, we'll see more specialized math AI resembling StockFish soon.

I disagree. It will be able to perform work deserving if a fields medal before it is capable of running a McDonalds. I think it will be running a McDonalds well before either of those things happen, and a fields medal long after both have happened.

Not necessarily. Obviously playing Kasparov on the board requires more planning ability than managing a McDonald's but look at where chess bots are now.

There's much more to being human than our "cognitive abilities"

Re: An OpenAI model has disproved a central conjecture in discrete geometry

#200
post #61

Earlier quoted context omitted.

> I think that idea is deeply fascinating, AND have no problem that we still credit mathematicians with discoveries. Most discoveries are indeed implied from axioms, but every now and then, new mathematics is (for lack of a better word) "created"—and you have people like Descartes, Newton, Leibniz, Gauss, Euler, Ramanujan, Galois, etc. that treat math more like an art than a science. For example, many belive that to…

"new kind of math" Well I think the point is there is no "new kind of math". There's just types of math we've discovered and what we haven't. No new math is created, just found.

The map is not the territory.
Post reply on HN