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

241–250 of 254 posts

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

#241

Post by scotty79 »

earthicus wrote: post #132
scotty79 wrote: post #47

Earlier quoted context omitted.

Some of the critique is valid but some of it sounds like, "but the rules of the contest are that participants must use less than x joules of energy obtained from cellular respiration and have a singular consciousness" I don't think anybody thinks AI was competing fair and within the rules that apply to humans. But if the humans were competing on the terms that AI solved those problems on, near-unlimited access to ene…

I don't think that characterization is fair at all. It's certainly true that you, me, and most humans can't solve these problems with any amount of time or energy. But the problems are specifically written to be at the limit of what the actual high school students who participate can solve in four hours . Letting the actual students taking the test have four days instead of four hours would make a massive difference…

> you haven't accurately told us what the machines can do today

It told us that using probably unreasonable compute they can solve few math problems that are very hard to solve for high-schools students in 4 hours. That's all the rules. No need to state them ahead of time or at all because they are obvious from the context.

It was just a fun thing to check and good meme for the media. Obviously the machines can do a lot more in some aspects and a lot less in others.

If we at least maintain the current pace in few years instead of machines solving 5 problems almost all high-schools students are incapable of solving in 4 hours they are gonna solve a problem Terence Tao is not capable of solving in one lifetime. Hopefully.

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

#242

Post by sigmoid10 »

nicce wrote: post #235
aerhardt wrote: post #95

Earlier quoted context omitted.

I use o3, openAI API and Claude Code. Genuinely curious what about Gemini 2.5 is so far behind?

I don’t think it is behind in anything. It is just harder to make obey and redefine the default system command. It is very verbose model by default.

It's not just much more verbose in general, it easily gets lost in verbosity. As in often trying to solve issues that aren't there. And when you try to make it focus, it doesn't get the issue at all.

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

#243

Post by machiaweliczny »

daxfohl wrote: post #151
modeless wrote: post #45

> AlphaGeometry and AlphaProof required experts to first translate problems from natural language into domain-specific languages, such as Lean, and vice-versa for the proofs. It also took two to three days of computation. This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions So, the problem wasn't translated…

I'd also be curious as to why not use Lean. Is it that Lean use at this point makes the problems too easy to brute force? Or is it that Lean at this point just gets in the way of things?

I think because you want to input mathematical proof intuition (heuristic) into models so they can grasp our reality better than just use tools without much clue.

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

#244

Post by machiaweliczny »

asdfologist wrote: post #159
ted_dunning wrote: post #147

Earlier quoted context omitted.

It didn't kill chess

It did partially, which is why top players are nowadays playing Freestyle (chess 960) more and more.

Every game becomes boring once figured out. I personally like to explore "meta" on my own. Once I know it I leave game to others as it's usually boring to me.

I think meta is basically experimentally determined constrains that limit reasoning tree and make problems computable/easy. LLMs/AI needs to start figuring something like this out on their own to make progress. RL kinda does it but maybe there's a better way.

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

#245

Post by machiaweliczny »

machiaweliczny wrote: post #244
asdfologist wrote: post #159

Earlier quoted context omitted.

It did partially, which is why top players are nowadays playing Freestyle (chess 960) more and more.

Every game becomes boring once figured out. I personally like to explore "meta" on my own. Once I know it I leave game to others as it's usually boring to me. I think meta is basically experimentally determined constrains that limit reasoning tree and make problems computable/easy. LLMs/AI needs to start figuring something like this out on their own to make progress. RL kinda does it but maybe there's a better way.

To add to this. Scientific progress seems to slow when some of these constraints are incorrectly defined leading or blocking valid search trees, which suggest that humanity determines then but also wrong sometimes. Thus we need to really on formal proofs that are 100% reliable as well and revisit these constraints from time to time.

It applies to science as to law etc.

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

#246

Post by edanm »

simonw wrote: post #157
jonahx wrote: post #137

Earlier quoted context omitted.

As a side question, do you think using tools like Lean will become a staple of these "deep reasoning" LLM flavors? It seems that LLMs excel (relative to other paradigms) in the kind of "loose" creative thinking humans do, but are also prone to the same kinds of mistakes humans make (hallucinations, etc). Just as Lean and other formal systems can help humans find subtle errors in their own thinking, they could do the…

I was surprised to see them not using tools for it, that feels like a more reliable way to get useful results for this kind of thing. I get the impression not using tools is as part of the point though - to help demonstrate how much mathematical "reasoning" you can get out of just a model on its own.

Yes, I'm similarly surprised. Intuitively I'd think that it's much better to train on using Lean, since it's much easier to do RL on it (Lean gives you an objective metric on whether you achieved your objective). It also seems more useful in some ways.

But all the model providers are putting emphasis on the "this is only using natural language" angle, which I think is interesting both from a "this is easier for humans to actually use" perspective, but also comes from a place of "look how general the model is".

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

#247

Post by blinding-streak »

thewebguyd wrote: post #17
jeffbee wrote: post #6

Advanced Gemini, not Gemini Advanced. Thanks, Google. Maybe they should have named it MathBard.

Google and Microsoft continuing to prove that the hardest problem in programming is naming things.

ChatGPT is also a terrible name for a product. OpenAI's branding for their models is awful.

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

#248

Post by bwfan123 »

This paper [1] shows that gemini pro 2.5 without data-contamination and some minimal prompting (llm orchestration) can solve problems 1-5 on imo 2025.

[1] https://arxiv.org/pdf/2507.15855

For problems with 2 page solutions, the search space of solutions is likely limited, and hence could be brute-forced by a search. Combinatorics is likely the hold-out since there are no set approaches one could take ie training data wont cover the space of techniques - which could explain why problem 6 stumped the llms.

Also, in the future the minimal diligence IMO problem setters could do is to test against these LLMs to ensure that they cant solve them. Further, one could expect these tools to become available to contestents just like calculators are allowed in tests these days.

Still, it is impressive for the LLMs to be able to craft watertight arguments in math at the IMO level without the use of provers.

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

#249

Post by qbit42 »

tough wrote: post #108
dist-epoch wrote: post #92

Earlier quoted context omitted.

The bitter lesson.

well lean systems might be still useful for other stuff than max benching my point being transformers and llms have all the tailwind of all the infra+lateral discoveries/improvements being put into them. does that mean they're the one tool to unlock machine intelligence? I dunno

I think formal systems like Lean are still extremely interesting. And I would imagine that, if these machines get good at standard "informal" proofs, that the overhead of formalization would be a lot less painful for them than humans (it is pretty tedious these days but even for humans the friction is decreasing).

Verified proofs allow you to collaborate with much less trust (for humans or machines), at least in the phase where you are trying to figure out what is true. They don't guarantee that a proof is insightful for "why" a result is true, but that is much easier to put together once you have a valid proof.

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

#250

Post by jug »

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, I'd say GPT-4o is more on the order of Gemini Flash.
Post reply on HN