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.
An OpenAI model has disproved a central conjecture in discrete geometry
191–200 of 1001 posts
Re: An OpenAI model has disproved a central conjecture in discrete geometry
#192Earlier 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.
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
#193As 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…
Re: An OpenAI model has disproved a central conjecture in discrete geometry
#194See 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.
Re: An OpenAI model has disproved a central conjecture in discrete geometry
#195To 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?
Re: An OpenAI model has disproved a central conjecture in discrete geometry
#196See 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.
Re: An OpenAI model has disproved a central conjecture in discrete geometry
#197Re: An OpenAI model has disproved a central conjecture in discrete geometry
#198As 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.
There's much more to being human than our "cognitive abilities"
Re: An OpenAI model has disproved a central conjecture in discrete geometry
#199Re: An OpenAI model has disproved a central conjecture in discrete geometry
#200Earlier 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.