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

Gemini with Deep Think achieves gold-medal standard at the IMO

deepmind.google

Post reply on HN
Print view View original

181–190 of 254 posts

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#181

Post by nicf »

mietek wrote: post #174
nicf wrote: post #148

Earlier quoted context omitted.

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

A proof written in a formal language can absolutely be illuminating to a human, but you have to pick the correct formal language and ecosystem. Writing proofs in Agda is like writing programs in a more expressive variant of Haskell. Abelson said that “programs must be written for people to read, and only incidentally for machines to execute”, and by the Curry-Howard isomorphism, proofs can be seen as programs. All th…

I certainly didn't mean to dispute that! Formal proofs have a lot in common with code, and of course reading code is illuminating to humans all the time.

I meant to be responding specifically to the case where some future theorem-proving LLM spits out a thousand-page argument which is totally impenetrable but which the proof-checker still agrees is valid. I think it's sometimes surprising to people coming at this from the CS side to hear that most mathematicians wouldn't be too enthusiastic to receive such a proof, and I was just trying to put some color on that reaction.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#182

Post by mietek »

nicf wrote: post #181
mietek wrote: post #174

Earlier quoted context omitted.

A proof written in a formal language can absolutely be illuminating to a human, but you have to pick the correct formal language and ecosystem. Writing proofs in Agda is like writing programs in a more expressive variant of Haskell. Abelson said that “programs must be written for people to read, and only incidentally for machines to execute”, and by the Curry-Howard isomorphism, proofs can be seen as programs. All th…

I certainly didn't mean to dispute that! Formal proofs have a lot in common with code, and of course reading code is illuminating to humans all the time. I meant to be responding specifically to the case where some future theorem-proving LLM spits out a thousand-page argument which is totally impenetrable but which the proof-checker still agrees is valid. I think it's sometimes surprising to people coming at this fro…

Ah, I do agree with this perspective. I think we must ensure that any such tools emit proofs that are not only valid but also readable.

On the other hand, humans do also occasionally emit unreadable proofs, and perhaps some troubles could have been avoided if a formal language had been used.

https://www.quantamagazine.org/titans-of-mathematics-clash-o...

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#183

Post by pphysch »

NitpickLawyer wrote: post #130
pphysch wrote: post #73

Earlier quoted context omitted.

This reminds me of when OpenAI made a splash (ages ago now) by beating the world's best Dota 2 teams using a RL model. ...Except they had to substantially bend the rules of the game (limiting the hero pool, completely changing/omitting certain mechanics) to pull this off. So they ended up beating some human Dota pros at a psuedo-Dota custom game, which was still impressive, but a very much watered-down result beneath…

Limiting the hero pool was fair I'd say. If you can prove RL works on one hero, it's fairly certain it would work on other heroes. All of them at once? Maybe run into problems. But anyway you'd need orders of magnitude more compute so I'd say that was fair game.

That's akin to saying it's okay to remove Knights, or castling, or en passant from chess because they have a complicated movement mechanic that the AI can't handle as well.

Hero drafting and strategy is a major aspect of competitive Dota 2.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#184

Post by dimitri-vs »

lblume wrote: post #164
fpia wrote: post #162

I'm interested in your feedback, legitimate third-party users not associated with Google: have you ever try to get anything done well with Gemini? I have, and the thing is in chains. Generate images? no can do, copyright. Evaluate available hardware for a DIY wireless camera? No can do, can't endorse surveillance. Code? WRONG. General advice? hallucinate. I swear, I currently use Perplexity, Claude, ChatGPT, i even t…

I find Gemini Pro to be much more capable than GPT-4o at reading comprehension, code writing and brainstorming.

Yes, second this, I would go as far to say I use it more than o3.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#185

Post by xdavidliu »

vouaobrasil wrote: post #128

This is making mathematics too systematic and mechanical, and it kills the joy of it....

this comment reminds me of that Feynman quote about others thinking scientific knowledge removes the beauty from a flower. of course Feynman disagreed

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#186

Post by daxfohl »

nicf wrote: post #148
kevinventullo wrote: post #91

This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions I think I have a minority opinion here, but I’m a bit disappointed they seem to be moving away from formal techniques. I think if you ever want to truly “automate” math or do it at machine scale, e.g. creating proofs that would amount to thousands of page…

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

Ideally we'd be able to get a little of both. A proof of such magnitude should likely come with new definitions that are easy to search for in the code and start to reason about independently. Even without looking at the rest of the proof, I imagine we'd be able to deduce a fair amount of the structure just by understanding the new things that are being defined, what existing theorems are being imported, and connecting the dots.

Your comment reminds me of Tao's comment on the ABC conjecture: usually with a big proof, you progressively get new tools and examples of how they can be applied to other problems. But if it's hundreds of pages of formulas that just spits out an answer at the end, that's not how math usually works. https://galoisrepresentations.org/2017/12/17/the-abc-conject...

If these provers do end up spitting out 1000-page proofs that are all calculation with no net-new concepts, I agree they'll be met with a shrug.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#187

Post by david-gpu »

nicf wrote: post #148
kevinventullo wrote: post #91

This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions I think I have a minority opinion here, but I’m a bit disappointed they seem to be moving away from formal techniques. I think if you ever want to truly “automate” math or do it at machine scale, e.g. creating proofs that would amount to thousands of page…

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

> The ultimate reason I think is that what really lights a fire under most mathematicians is the desire to know why a result is true; the explanation is really the product, much more so than just the yes-or-no answer

Of course, but a formal system like Lean doesn't merely spit out a yes-or-now answer, it gives you a fully-fledged proof. Admittedly, it may be harder to read than natural language, but that only means we could benefit from having another tool that translates Lean proofs into natural language.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#188

Post by kevinventullo »

nicf wrote: post #148
kevinventullo wrote: post #91

This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions I think I have a minority opinion here, but I’m a bit disappointed they seem to be moving away from formal techniques. I think if you ever want to truly “automate” math or do it at machine scale, e.g. creating proofs that would amount to thousands of page…

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

Thanks for the reply. I am also a no-longer-practicing mathematician :)

I completely agree that a machine-generated formal proof is not the same thing as an illuminating human-generated plain-language proof (and in fact I suspect without further guidance they will be quite different, see my other stream of thought comment). However, I do think machine-generated formal proofs would be interesting for a few reasons:

1. Sometimes the obvious thing is not true!

2. I think the existence or non-existence of a machine-generated proof of a mathematical claim is interesting in its own right. E.g. what kinds of claims are easy versus hard for machines to prove?

3. In principle, I would hope they could at least give a starting point for a proper illuminating proof. E.g. the process of refinement and clarification, which is present today even for human proofs, could become more important, and could itself be machine-assisted.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#189

Post by 7373737373 »

kevinventullo wrote: post #91

This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions I think I have a minority opinion here, but I’m a bit disappointed they seem to be moving away from formal techniques. I think if you ever want to truly “automate” math or do it at machine scale, e.g. creating proofs that would amount to thousands of page…

They aren't - they are currently collating a repository of formalized open problems: https://github.com/google-deepmind/formal-conjectures

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#190

Post by nicf »

kevinventullo wrote: post #188
nicf wrote: post #148

Earlier quoted context omitted.

I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof wit…

Thanks for the reply. I am also a no-longer-practicing mathematician :) I completely agree that a machine-generated formal proof is not the same thing as an illuminating human-generated plain-language proof (and in fact I suspect without further guidance they will be quite different, see my other stream of thought comment). However, I do think machine-generated formal proofs would be interesting for a few reasons: 1.…

Oh, I hope I didn't come off as talking down to you! As I said in another reply here, the intention behind this comment was pretty narrow --- there's a certain perspective on this stuff that I see pretty often on HN that I think is missing some insight into what makes mathematicians tick, and I may have been letting my reaction to those other people leak into my response to you. Sorry for math-splaining :).

Anyway, yeah, if this scenario does come to pass it will be interesting to see just how impenetrable the resulting formal proofs end up looking and how hard it is to turn them into something that humans can fit in their heads. I can imagine a continuum of possibilities here, with thousands of pages of inscrutable symbol-pushing on one end to beautiful explanations on the other.

Post reply on HN