[HN Gopher] Gemini with Deep Think achieves gold-medal standard ...
___________________________________________________________________
Gemini with Deep Think achieves gold-medal standard at the IMO
Author : meetpateltech
Score : 402 points
Date : 2025-07-21 16:36 UTC (6 hours ago)
(HTM) web link (deepmind.google)
(TXT) w3m dump (deepmind.google)
| lufenialif2 wrote:
| Still no information on the amount of compute needed; would be
| interested to see a breakdown from Google or OpenAI on what it
| took to achieve this feat.
|
| Something that was hotly debated in the thread with OpenAI's
| results:
|
| "We also provided Gemini with access to a curated corpus of high-
| quality solutions to mathematics problems, and added some general
| hints and tips on how to approach IMO problems to its
| instructions."
|
| it seems that the answer to whether or not a general model could
| perform such a feat is that the models were trained specifically
| on IMO problems, which is what a number of folks expected.
|
| Doesn't diminish the result, but doesn't seem too different from
| classical ML techniques if quality of data in = quality of data
| out.
| vonneumannstan wrote:
| >it seems that the answer to whether or not a general model
| could perform such a feat is that the models were trained
| specifically on IMO problems, which is what a number of folks
| expected.
|
| Not sure thats exactly what that means. Its already likely the
| case that these models contained IMO problems and solutions
| from pretraining. It's possible this means they were present in
| the system prompt or something similar.
| sottol wrote:
| Or that they did significant retraining to boost IMO
| performance creating a more specialized model at the cost of
| general-purpose performance.
| AlotOfReading wrote:
| Does the IMO reuse problems? My understanding is that new
| problems are submitted each year and 6 are selected for each
| competition. The submitted problems are then published
| _after_ the IMO has concluded. How would the training data
| contain unpublished, newly submitted problems?
|
| Obviously the training data contained similar problems,
| because that's what every IMO participant already studies. It
| seems unlikely that they had access to the same problems
| though.
| AlanYx wrote:
| IMO doesn't reuse problems, but Terence Tao has a Mastodon
| post where he explains that the first five (of six)
| problems are generally ones where existing techniques can
| be leveraged to get to the answer. The sixth problem
| requires considerable originality. Notably, both Gemini and
| OpenAI's model didn't get the sixth problem. Still quite an
| achievement though.
| Davidzheng wrote:
| strange statement--it's not true in general for sure (3&6
| typically hardest but they certainly aren't fundamentally
| of a different nature to other questions) this year P6
| seemed to be by far the hardest though but this posthoc
| statement should be read cautiously
| apayan wrote:
| Do you have another source for that? I checked his
| Mastodon feed and don't see any mention about the source
| of the questions from the IMO.
|
| https://mathstodon.xyz/@tao
| vonneumannstan wrote:
| >How would the training data contain unpublished, newly
| submitted problems?
|
| I don't think I or op suggested it did.
| dvh wrote:
| Ok but when reported by mass media, which never used SI units
| and instead uses units like libraries of Congress, or
| elephants, what kind of unit should media use to compare
| computational energy of ai vs children?
| dortlick wrote:
| Kilocalories. A unit of energy that equals 4184 Joules.
| lufenialif2 wrote:
| Convert libraries, elephants, etc into SI of course!
| Otherwise, they aren't really comparable...
| thrance wrote:
| If the models that got a gold medal are anything like those
| used on ARC-AGI, then you can bet they wrote an insane amount
| of text trying to reason their ways through these problems.
| Like, several bookshelves worth of writings.
|
| So funnily enough, "the AI wrote x times the library of
| Congress to get there" is good enough of a comparison.
| rfurmani wrote:
| Dollars of compute at market rate is what I'd like to see, to
| check whether calling this tool would cost $100 or $100,000
| gus_massa wrote:
| 4.5 hours x 2 "days", 100 Wats including support system.
|
| I'm not sure how to implement the "no calculator" rule :) but
| for this kind of problems it's not critical.
|
| Total = 900Wh = 3.24MJ
| nicce wrote:
| Some unofficial comparison with costs of public models
| (performing worse): https://matharena.ai/imo/
|
| So the real cost is something much more.
| pfortuny wrote:
| They can train it n "Crux Mathematicorum" and similar journals,
| which are collections of "interesting" problems and their
| solutions.
|
| https://cms.math.ca/publications/crux
| gjm11 wrote:
| Human IMO contestants are also trained specifically on IMO
| problems.
| jeffbee wrote:
| Advanced Gemini, not Gemini Advanced. Thanks, Google. Maybe they
| should have named it MathBard.
| sahila wrote:
| Can't wait for Advanced Gemini Advance.
| throwawayoldie wrote:
| Advanced Gemini Advance Enterprise Advanced Edition (feat.
| Pitbull)
| lufenialif2 wrote:
| Advanced Gemini Advance Enterprise Boy Advanced Edition 3
| (feat. Pitbull) & Knuckles
| rao-v wrote:
| Don't give them ideas
| thewebguyd wrote:
| Google and Microsoft continuing to prove that the hardest
| problem in programming is naming things.
| nashashmi wrote:
| There are only so many words in the modern English language
| to hint at "next upgrade": pro, plus, ultra, new, advanced,
| magna, X, Z, and Ultimate. Even fewer words to explain
| miniaturized: mini, lite, and zero. And marketers are trying
| to seesaw on known words without creating new ones to explain
| new tech. This is why we have Bard and Gemini and Chat and
| Copilot.
|
| Taking a step back, it is overused exaggeration to the point
| where words run out quick and newer tech needs to fight with
| existing words for dominance. Copilot should be the name of
| an AI agent. Bard should have been just a text generator.
| Gemini is the name of a liar. Chat is probably the iphone of
| naming but the GPT suffix says Creativity had not come to
| work that day.
| SirMaster wrote:
| Good thing we have a system called numbers that can easily
| designate an infinite range of greater and greater things.
| NitpickLawyer wrote:
| Heh, you'd still get confusing stuff. Wait, is gemini
| 2.5.3.1 the math one or the erotica lit one?
| antonvs wrote:
| There are two different versions of that hard problem: the
| computer science version, and the marketing version. The
| marketing one has more nebulous acceptance criteria though.
| seydor wrote:
| They will have to rename gemini anyway, since it's doubtful
| they will ever be able to buy gemini.com. Gemini turboflex plus
| pro SE plaid interstellar 4.0
| catigula wrote:
| What makes you think google can't buy that domain?
| esafak wrote:
| ... for a reasonable cost.
| joaogui1 wrote:
| It's not a new product/model with that name, they're just
| saying it's an advanced version of Gemini that's not public atm
| nomad_horse wrote:
| Do I understand it correctly that OpenAI self-proclaimed that
| they got their gold, without the official IMO judges grading
| their solutions?
| ipsum2 wrote:
| Yes
| jacquesm wrote:
| Why am I not surprised?
| danjl wrote:
| Childish. And, of course they must have known there was an
| official LLM cohort taking the real test, and they probably
| even knew that Gemini got a gold medal, and _may_ have even
| known that Google planned a press release for today.
| cma wrote:
| I think maybe all Altman companies have used tactics like
| this.
|
| > We were trying to get a big client for weeks, and they said
| no and went with a competitor. The competitor already had a
| terms sheet from the company were we trying to sign up. It
| was real serious.
|
| > We were devastated, but we decided to fly down and sit in
| their lobby until they would meet with us. So they finally
| let us talk to them after most of the day.
|
| > We then had a few more meetings, and the company wanted to
| come visit our offices so they could make sure we were a
| 'real' company. At that time, we were only 5 guys. So we
| hired a bunch of our college friends to 'work' for us for the
| day so we could look larger than we actually were. It worked,
| and we got the contract.
|
| > I think the reason why PG respects Sam so much is he is
| charismatic, resourceful, and just overall seems like a
| genuine person.
|
| https://news.ycombinator.com/item?id=3048944
| pishpash wrote:
| So, a more charismatic version of Zuck is Zucking, what a
| surprise. Company culture starts at its origin. Despite
| Google's corruption, its origin is in academia and it shows
| even now.
| gowld wrote:
| For a long time, the YC application asked founders for an
| example of how they "hacked" (cheated) a system.
| tough wrote:
| I think pg was into it way before sama was a baby lol
| https://www.paulgraham.com/gh.html
| tough wrote:
| >> > I think the reason why PG respects Sam so much is he
| is charismatic, resourceful, and just overall seems like a
| genuine person.
|
| does he? wasn't sama ousted of YC in some muddy ways after
| he tried to co-opt in into an OpenAI investment arm, was
| funny to find the YC Open Research project landing page on
| yc's website now defunct and pointing how he misrepresented
| it as a YC project when it was his own
|
| maybe he fears him, but I doubt pg respects him, unless he
| respects evil, lol
| cma wrote:
| The post was from 14 years ago, before that.
| gametorch wrote:
| (deleted because I was mistaken)
| nomad_horse wrote:
| isn't he an IOI medalist? and even if he was an IMO medalist,
| isn't there a bit of a conflict of interests?
| cbsmith wrote:
| Just a wee bit.
| cbsmith wrote:
| I'm pretty sure when they got the gold medal they weren't
| allowed to judge themselves.
| NitpickLawyer wrote:
| Well, I don't doubt that they did get those results, but it is
| clear now that it was not an official collaboration. It was
| heavily implied in a statement by IMO's president a few days
| ago (the one where they said they'd prefer AI companies wait a
| week before announcing, so that the focus is first on the human
| competitors).
|
| Goog had an official colab with IMO, and we can be sure they
| got those results under the imposed constraints (last year they
| allocated ~48h for silver IIRC) and an official grading by the
| IMO graders.
| Tadpole9181 wrote:
| So from 48 hours for silver down to 4.5 hours for gold in one
| year? And all reasoning generated is clear and easy to
| follow? That's one hell of an improvement.
| tshadley wrote:
| Yes, OpenAI:
|
| https://x.com/alexwei_/status/1946477754372985146
|
| > 6/N In our evaluation, the model solved 5 of the 6 problems
| on the 2025 IMO. For each problem, three former IMO medalists
| independently graded the model's submitted proof, with scores
| finalized after unanimous consensus. The model earned 35/42
| points in total, enough for gold!
|
| That means Google Deepmind is the first OFFICIAL IMO Gold.
|
| https://x.com/demishassabis/status/1947337620226240803
|
| > We've now been given permission to share our results and are
| pleased to have been part of the inaugural cohort to have our
| model results officially graded and certified by IMO
| coordinators and experts, receiving the first official gold-
| level performance grading for an AI system!
| nomad_horse wrote:
| Do you know if OpenAI used the same grading criteria as
| official judges?
| tshadley wrote:
| As IMO medalists they would be expected to I'm sure.
|
| But this can be verified because the results are public:
|
| https://github.com/aw31/openai-imo-2025-proofs/
| lvl155 wrote:
| Seems OpenAI knew this is forthcoming so they front ran the news?
| I was really high on Gemini 2.5 Pro after release but I kept
| going back to o3 for anything I cared about.
| sigmoid10 wrote:
| >I was really high on Gemini 2.5 Pro after release but I kept
| going back to o3 for anything I cared about
|
| Same here. I was impressed by their benchmarks and topping most
| leaderboards, but in day to day use they still feel so far
| behind.
| danjl wrote:
| I think that's most likely just your view, and not really
| based on evidence.
| aerhardt wrote:
| I use o3, openAI API and Claude Code. Genuinely curious what
| about Gemini 2.5 is so far behind?
| erichocean wrote:
| I regularly have the opposite experience: o3 is almost
| unusable, and Gemini 2.5 Pro is reliably great. Claude Opus 4
| is a close second.
|
| o3 is so bad it makes me wonder if I'm being served a different
| model? My o3 responses are so truncated and simplified as to be
| useless. Maybe my problems aren't a good fit, but whatever it
| is: o3 output isn't useful.
| Davidzheng wrote:
| I have this distinctive feeling that o3 tries to trick me
| intentionally when it can't solve a problem by cleverly
| hiding its mistakes. But I could be imagining it
| int_19h wrote:
| It's certainly the "laziest" model, in the sense that it
| seems to be the likeliest to avoid doing the actual work
| and generate "TBD" stubs instead.
| helloplanets wrote:
| Are you using a tool other than ChatGPT? If so, check the
| full prompt that's being sent. It can sometimes kneecap the
| model.
|
| Tools having slightly unsuitable built in prompts/context
| sometimes lead to the models saying weird stuff out of the
| blue, instead of it actually being a 'baked in' behavior of
| the model itself. Seen this happen for both Gemini 2.5 Pro
| and o3.
| square_usual wrote:
| Are you using o3 on the official ChatGPT app or via API? I
| use it on the app and it performs very well, it's my go-to
| model for general purpose LLM use.
| erichocean wrote:
| official ChatGPT app
| deanCommie wrote:
| From Terence Tao, via mastodon [0]:
|
| > It is tempting to view the capability of current AI technology
| as a singular quantity: either a given task X is within the
| ability of current tools, or it is not. However, there is in fact
| a very wide spread in capability (several orders of magnitude)
| depending on what resources and assistance gives the tool, and
| how one reports their results.
|
| > One can illustrate this with a human metaphor. I will use the
| recently concluded International Mathematical Olympiad (IMO) as
| an example. Here, the format is that each country fields a team
| of six human contestants (high school students), led by a team
| leader (often a professional mathematician). Over the course of
| two days, each contestant is given four and a half hours on each
| day to solve three difficult mathematical problems, given only
| pen and paper. No communication between contestants (or with the
| team leader) during this period is permitted, although the
| contestants can ask the invigilators for clarification on the
| wording of the problems. The team leader advocates for the
| students in front of the IMO jury during the grading process, but
| is not involved in the IMO examination directly.
|
| > The IMO is widely regarded as a highly selective measure of
| mathematical achievement for a high school student to be able to
| score well enough to receive a medal, particularly a gold medal
| or a perfect score; this year the threshold for the gold was
| 35/42, which corresponds to answering five of the six questions
| perfectly. Even answering one question perfectly merits an
| "honorable mention".
|
| > But consider what happens to the difficulty level of the
| Olympiad if we alter the format in various ways:
|
| * One gives the students several days to complete each question,
| rather than four and half hours for three questions. (To stretch
| the metaphor somewhat, consider a sci-fi scenario in the student
| is still only given four and a half hours, but the team leader
| places the students in some sort of expensive and energy-
| intensive time acceleration machine in which months or even years
| of time pass for the students during this period.)
|
| * Before the exam starts, the team leader rewrites the questions
| in a format that the students find easier to work with.
|
| * The team leader gives the students unlimited access to
| calculators, computer algebra packages, formal proof assistants,
| textbooks, or the ability to search the internet.
|
| * The team leader has the six student team work on the same
| problem simultaneously, communicating with each other on their
| partial progress and reported dead ends.
|
| * The team leader gives the students prompts in the direction of
| favorable approaches, and intervenes if one of the students is
| spending too much time on a direction that they know to be
| unlikely to succeed.
|
| * Each of the six students on the team submit solutions, but the
| team leader selects only the "best" solution to submit to the
| competition, discarding the rest.
|
| * If none of the students on the team obtains a satisfactory
| solution, the team leader does not submit any solution at all,
| and silently withdraws from the competition without their
| participation ever being noted.
|
| > In each of these formats, the submitted solutions are still
| technically generated by the high school contestants, rather than
| the team leader. However, the reported success rate of the
| students on the competition can be dramatically affected by such
| changes of format; a student or team of students who might not
| even reach bronze medal performance if taking the competition
| under standard test conditions might instead reach gold medal
| performance under some of the modified formats indicated above.
|
| > So, in the absence of a controlled test methodology that was
| not self-selected by the competing teams, one should be wary of
| making apples-to-apples comparisons between the performance of
| various AI models on competitions such as the IMO, or between
| such models and the human contestants.
|
| > Related to this, I will not be commenting on any self-reported
| AI competition performance results for which the methodology was
| not disclosed in advance of the competition. EDIT: In particular,
| the above comments are not specific to any single result of this
| nature.
|
| [0] https://mathstodon.xyz/@tao/114881418225852441
| Mond_ wrote:
| Unlike OpenAI, Deepmind at least signed up for the competition
| ahead of time.
|
| Agree with Tao though, I am skeptical of any result of this
| type unless there's a lot of transparency, ideally ahead of
| time. If not ahead of time, then at least the entire prompt and
| fine-tune data that was used.
| ferguess_k wrote:
| This is a fair reply, but TBH I don't think it's going to
| change much. The upper echelon of the human society has decided
| to move AI forward rapidly regardless of any consequences. The
| rest of us can only hold and pray.
| justanotherjoe wrote:
| You are watching american money hard at work, my friend. It's
| either glorious or reckless, hard to tell for now.
| ferguess_k wrote:
| Could be both, but one for different group of people.
| scotty79 wrote:
| 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 energy, raw compute and data, still very
| few humans could solve those problems within a reasonable
| timeframe. It would take me probably months or years to educate
| myself sufficiently to even have a chance.
| earthicus wrote:
| 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 in their ability to solve them.
|
| Said differently, the students, difficulty of the problems,
| and time limit are specifically coordinated together, so the
| amount of joules of energy used to produce a solution is not
| arbitrary. In the grand scheme of how the tech will improve
| over time, it seems likely that doesn't matter and the
| computers will win by any metric soon enough, but Tao is
| completely correct to point out that you haven't accurately
| told us what the machines can do today, in July 2025, without
| telling us ahead of time exactly what rules you are
| modifying.
| dang wrote:
| Discussed here:
|
| _A human metaphor for evaluating AI capability_ -
| https://news.ycombinator.com/item?id=44622973 - July 2025 (30
| comments)
| be7a wrote:
| Super interesting that they moved away from their specialized,
| Lean-based system from last year to a more general-purpose LLM +
| RL approach. I would suspect this likely leads to improved
| performance even outside of math competitions. It'll be
| fascinating to see how much further this frontier can go.
|
| The article also suggests that the system used isn't too far
| ahead of their upcoming general "DeepThink" model / feature,
| which is they announced for this summer.
| gundmc wrote:
| I assume that an "advanced version" of Gemini Deepthink means it
| was a different model or had significantly more test time compute
| than the upcoming Deepthink in the Gemini Ultra subscription.
| Still cool to see OpenAI and Google neck and neck.
| sxp wrote:
| Related news:
|
| - OpenAI claims gold-medal performance at IMO 2025
| https://news.ycombinator.com/item?id=44613840
|
| - "According to a friend, the IMO asked AI companies not to steal
| the spotlight from kids and to wait a week after the closing
| ceremony to announce results. OpenAI announced the results BEFORE
| the closing ceremony.
|
| According to a Coordinator on Problem 6, the one problem OpenAI
| couldn't solve, "the general sense of the IMO Jury and
| Coordinators is that it was rude and inappropriate" for OpenAI to
| do this.
|
| OpenAI wasn't one of the AI companies that cooperated with the
| IMO on testing their models, so unlike the likely upcoming Google
| DeepMind results, we can't even be sure OpenAI's "gold medal" is
| legit. Still, the IMO organizers directly asked OpenAI not to
| announce their results immediately after the olympiad.
|
| Sadly, OpenAI desires hype and clout a lot more than it cares
| about letting these incredibly smart kids celebrate their
| achievement, and so they announced the results yesterday."
| https://x.com/mihonarium/status/1946880931723194389
| KaoruAoiShiho wrote:
| OpenAI announced their results after the closing ceremony as
| was requested.
| https://x.com/polynoamial/status/1947024171860476264?s=46
| nicce wrote:
| > as was requested.
|
| They requested week after?
| modeless wrote:
| He claims nobody made that request to OpenAI. It was a
| request made to Google and others who were being judged by
| the actual contest judges, which OpenAI was not.
| gowld wrote:
| IMO agreed to cancel the embargo after OpenAI announced.
| mike_d wrote:
| Proposed question for next IMO: "Show a proof that 'after the
| closing ceremony' and 'one week later' are not the same unit
| of time"
| ml-anon wrote:
| This is weasily bullshit from Brown.
| sherburt3 wrote:
| What a great metaphor for AI. Taking an event that is a
| celebration of high school kids' knowledge and abilities and
| turning it into a marketing stunt for their frankenstein
| monster that they are building to make all the kids' hard work
| worth nothing.
| echelon wrote:
| Google did the correct and respectful thing.
|
| It appears that OpenAI didn't officially enter (whereas
| Google did), that they knew Google was going to gold medal,
| and that they released their news ahead of time
| (disrespecting the kids and organizers) so they could scoop
| Google.
|
| Really scummy on OpenAI's part.
|
| The IMO closing ceremony was July 19. OpenAI announced on the
| same day.
|
| IMO requested the tech companies to wait until the following
| week.
| ml-anon wrote:
| Not only, by not officially entering they had no obligation
| to announce their result so if they didn't achieve a gold
| medal score they presumably wouldn't have made any
| announcement and no-one would have been the wiser.
|
| This cowardly bullshit followed by the grandstanding on
| Twitter is high-school bully behaviour.
| gowld wrote:
| If they failed and remained quiet, then everyone would know
| that the other companies performed well and they didn't
| even qualify.
| tough wrote:
| If they failed while not participating officially, they
| would have never competed at the eyes public if they
| didnt disclose it (doubtful, given prior decisions to
| prioritise hype vs transparency)
| tough wrote:
| also did they self-rate themselves?
| ekojs wrote:
| > Btw as an aside, we didn't announce on Friday because we
| respected the IMO Board's original request that all AI labs share
| their results only after the official results had been verified
| by independent experts & the students had rightly received the
| acclamation they deserved
|
| > We've now been given permission to share our results and are
| pleased to have been part of the inaugural cohort to have our
| model results officially graded and certified by IMO coordinators
| and experts, receiving the first official gold-level performance
| grading for an AI system!
|
| From https://x.com/demishassabis/status/1947337620226240803
|
| Was OpenAI simply not coordinating with the IMO Board then?
| dmitrygr wrote:
| > Was OpenAI simply not coordinating with the IMO Board then?
|
| You are still surprised by sama@'s asinineness? You must be new
| here.
| antonvs wrote:
| When your goal is to control as much of the world's money as
| possible, preferably all of it, then everyone is your enemy,
| including high school students.
| dmitrygr wrote:
| How dare those high school students use their brains to
| compete with ChatGPT and deny the shareholders their value?
| MisterPea wrote:
| I am still surprised many people trust him. The board's
| (justified) decision to fire him was so awfully executed that
| it lead to him having even more slack
| thegeomaster wrote:
| Yes, there have been multiple (very big) hints dropped by
| various people that they had no official cooperation.
| pphysch wrote:
| 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 the
| marketing hype.
|
| It does seem like Money+Attention outweigh Science+Transparency
| at OpenAI, and this has always been the case.
| NitpickLawyer wrote:
| 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.
| npinsker wrote:
| It's not even close to the same game as Dota. Limiting the
| hero (and item) pool so drastically locks off many
| strategies and counters. It's a bit hard to explain if you
| haven't played, but full Dota has many more tools and much
| more creativity than the reduced version on display. The
| behavior does not evidently "scale up", in the same way
| that the current SotA of AI art and writing won't evidently
| replace top-level humans.
|
| I'd never say it's impossible, but the job wasn't finished
| yet.
| pphysch wrote:
| 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.
| osti wrote:
| I think this is them not being confident enough before the
| event, so they don't wanna be shown a worse result than
| competitors. By being private they can obviously not publish
| anything if it didn't work out.
| ml-anon wrote:
| As not-so-subtly hinted at by Terry Tao.
|
| Its a great way to do PR but its a garbage way to to science.
| osti wrote:
| True, but openai definitely isn't trying to do public
| research on science, they are all about money now.
| ml-anon wrote:
| Thats not a contentious statement. Its still a pathetic
| way to behave at a kids competition no less.
| esafak wrote:
| They shot themselves in the foot by not showing the
| confidence that Google did.
| tornikeo wrote:
| I think we are having a Deep Blue vs. Kasparov moment in
| Competitive Math right now. This is a large progress from just a
| few years ago and yet I think we still are really far away from
| even a semi-respectable AI mathematician. What an exciting time
| to be alive!
| NitpickLawyer wrote:
| Terrence Tao, in a recent podcast, said that he's very
| interested in "working along side these tools". He sees the
| best use in the near future as "explorers of human set vision"
| in a way. (i.e. set some ideas/parameters and let the LLMs
| explore and do parallel search / proof / etc)
|
| Your comparison with chess engines is pretty spot-on, that's
| how the best of the best chess players do prep nowadays. Gone
| are the multi person expert teams that analysed positions and
| offered advice. They now have analysts that use supercomputers
| to search through bajillions of positions and extract the best
| ideas, and distill them to their players.
| tough wrote:
| > They now have analysts that use supercomputers to search
| through bajillions of positions and extract the best ideas,
| and distill
|
| I was recently researching AI's for this, seems it would be a
| huge unlock for some parts of science where this is the case
| too like chess
| 7373737373 wrote:
| He created a Youtube channel showcasing working alongside
| these tools: https://youtube.com/@TerenceTao27
| j2kun wrote:
| He also had some interesting things to say about these IMO
| results: https://mathstodon.xyz/@tao/114881418225852441
| ars wrote:
| Similar to https://en.wikipedia.org/wiki/Advanced_chess
|
| The Wikipedia doesn't have much info on the results, but from
| other reading I got the impression that the combination
| produced results stronger than any individual human or
| computer player.
| gjm11 wrote:
| My understanding is that they _did_ , but don't any more;
| it's no longer true that humans understand enough things
| about chess better than computers for the human/computer
| collaboration to contribute anything over just using the
| computer.
|
| I don't think the interval between "computers are almost as
| strong as humans" and "computers are so much stronger than
| humans that there's no way for even the strongest humans to
| contribute anything that improves the computer's play" was
| very long. We'll see whether mathematics is any
| different...
| drexlspivey wrote:
| More like Deep Blue vs Child prodigy. In the IMO the
| contestants are high school students not the greatest
| mathematicians in the world.
| bbconn wrote:
| Of course contest math is not research math but the active
| IMO kids are pretty much the best in the world at math
| contests.
| aldousd666 wrote:
| The difference here is that no amount of brute force can
| produce the winning score in the timeframe. This is more of a
| legitimate technical milestone and less of a moral 'in
| principle' one that we saw with deep blue
| modeless wrote:
| > 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 to Lean first. But did the
| model use Lean, or internet search, or a calculator or Python or
| any other tool during its internal thinking process? OpenAI said
| theirs didn't, and I'm not sure if this is exactly the same
| claim. More clarity on this point would be nice.
|
| I would also love to know the rough order of magnitude of the
| amount of computation used by both systems, measured in dollars.
| Being able to do it at all is of course impressive, but not
| useful yet if the price is outrageous. In the absence of
| disclosure I'm going to assume the price is, in fact, outrageous.
|
| Edit: "No tool use, no internet access" confirmed:
| https://x.com/FredZhang0/status/1947364744412758305
| rfurmani wrote:
| Sounds like it did not:
|
| > This year, our advanced Gemini model operated end-to-end in
| natural language, producing rigorous mathematical proofs
| directly from the official problem descriptions - all within
| the 4.5-hour competition time limit
| modeless wrote:
| Yes, that quote is contained in my comment. But I don't think
| it unambiguously excludes tool use in the internal chain of
| thought.
|
| I don't think tool use would detract from the achievement,
| necessarily. I'm just interested to know.
| KoolKat23 wrote:
| End to end in natural language would imply no tool use, I'd
| imagine. Unless it called another tool which converted it
| but that would be a real stretch (smoke and mirrors).
| simonw wrote:
| I interpreted that bit as meaning they did not manually alter
| the problem statement before feeding it to the model - they
| gave it the exact problem text issued by IMO.
|
| It is not clear to me from that paragraph if the model was
| allowed to call tools on its own or not.
| jonahx wrote:
| 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 same for LLMs.
| simonw wrote:
| 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.
| getnormality wrote:
| We're told that formal verification tools like Lean are not
| used to solve the actual IMO problems, but are they used in
| training the model to solve the problems?
|
| We know from Google's 2024 IMO work that they have a way to
| translate natural language proofs to formally verifiable ones.
| It seems like a natural next step would be to leverage this for
| RLVR in training/fine-tuning. During training, any piece of
| reasoning generated by the math LLM could be translated,
| verified, and assigned an appropriate reward, making the reward
| signal much denser.
|
| Reward for a fully correct proof of a given IMO problem would
| still be hard to come by, but you could at least discourage the
| model from doing wrong or indecipherable things. That plus tons
| of compute might be enough to solve IMO problems.
|
| In fact it probably would be, right? We already know from
| AlphaProof that by translating LLM output back and forth
| between formal Lean proofs, you can search the space of
| reasoning moves efficiently enough to solve IMO-class problems.
| Maybe you can cut out the middleman by teaching the LLM via
| RLVR to mimic formal reasoning, and that gets you roughly the
| same efficiency and ability to solve hard problems.
| modeless wrote:
| It seems very likely from the description in the link that
| formal verification tools for mathematical proofs were used
| in part of the RL training for this model. On the other hand,
| OpenAI claims "We reach this capability level not via narrow,
| task-specific methodology, but by breaking new ground in
| general-purpose reinforcement learning and test-time compute
| scaling." Which might suggest that they don't specifically
| use e.g. Lean in their training process. But it's not
| explicitly stated. All we can really do is speculate unless
| they publish more detail.
| getnormality wrote:
| The OpenAI proofs are so brutally, inhumanly spartan that I
| can't imagine how the AI came up with them, except by RLVR
| against some crudely translated formal language.
| daxfohl wrote:
| 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?
| wbhart wrote:
| Lean is an interactive prover, not an automated prover. Last
| year a lot of human effort was required to formalise the
| problems in Lean before the machines could get to work. This
| year you get natural language input and output, and much
| faster.
|
| The advantage of Lean is that the system checks the
| solutions, so hallucination is impossible. Of course, one
| still relies on the problems and solutions being translated
| to natural language correctly.
|
| Some people prefer difficult to read formally checked
| solutions over informal but readable solutions. The two
| approaches are just solving different problems.
|
| But there is another important reason to want to do this
| reliably in natural language: you can't use Lean for other
| domains (with a few limited exceptions). They want to train
| their RL pipelines for general intelligence and make them
| reliable for long horizon problems. If a tool is needed as a
| crutch, then it more or less demonstrates that LLMs will not
| be enough in any domain, and we'll have to wait for
| traditional AI to catch up for every domain.
| daxfohl wrote:
| Oh, I didn't realize that last year the problem
| formalization was a human effort; I assumed the provers
| themselves took the problem and created the formalization.
| Is this step actually harder to automate than solving the
| problem once it's formalized?
|
| Anyway mainly I was curious whether using an interactive
| prover like Lean would have provided any advantage, or
| whether that is no longer really the case. My initial take
| would be that, yes, it should provide a huge advantage.
| Like in chess and go, it'd allow it to look algorithmically
| through a huge search space and check which approaches get
| it closer to resolving, where the AI is "only" responsible
| for determining what approaches to try.
|
| OTOH, maybe not. Maybe the search space is so big that
| trying to go through it linearly is a waste of CPU. In
| which case, plausibly the translation to Lean offers no
| benefit. And now that I think about it, I could imagine
| that. When doing problems like these, you kind of have to
| figure out the overall approach end to end first, fill in
| any gaps in your logic, and the formalization/writing step
| is kind of the last thing you do. So I could see where
| starting on formalization from the start could end up being
| the wrong approach for IMO-level problems. It'd just be
| nice to have that confirmed.
|
| The cool thing is that if true, it implies this is
| something completely different from the chess/go engines
| that rely on sheer computational power. Not so much of a
| "deep blue" moment, but more of an existential one.
| jay_kyburz wrote:
| I wonder if "not tool use, no internet access" means it can run
| without google inf, and offline. Meaning it could be deployed
| locally for people that need that.
| brokensegue wrote:
| based on the score looks like they also couldn't answer question
| 6? has that been confirmed?
| liuliu wrote:
| https://storage.googleapis.com/deepmind-media/gemini/IMO_202...
| brokensegue wrote:
| i saw that but it doesn't answer my question since it doesn't
| have associated marks? i'm not about to check their answer to
| a question i can't answer
| simonw wrote:
| That PDF lists solutions for problems 1 through 5 but does
| not mention problem 6 at all.
| brokensegue wrote:
| Ah thanks that does answer it. You should start a blog
| tough wrote:
| Simon's a prolific writer on AI
|
| http://simonw.substack.com https://simonwillison.net
| brokensegue wrote:
| cool! glad he took my advice
| tough wrote:
| oracle!!
| osti wrote:
| The proofs also seem more human reable than openai's?
| b8 wrote:
| Surprising since Reid Barton was working on a lean system.
| dist-epoch wrote:
| The bitter lesson.
| tough wrote:
| 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
| shiandow wrote:
| Comparing the answers between Openai and Gemini the writing style
| of Gemini is a lot clearer. It could be presented a bit better
| but it's easy enough to follow the proof. This also makes it a
| lot shorter than the answer given by OpenAI and it uses proper
| prose.
| cubefox wrote:
| I found the proofs you were referring to:
|
| Google https://storage.googleapis.com/deepmind-
| media/gemini/IMO_202...
|
| OpenAI https://github.com/aw31/openai-imo-2025-proofs/
| sweezyjeezy wrote:
| Gemini is clearer but MY GOD is it verbose. e.g. look at
| problem 1, section _2. Analysis of the Core Problem_ - there
| 's nothing at all deep here, but it seems the model wants to
| spell out every single tiny logical step. I wonder if this is
| a stylistic choice or something that actually helps the model
| get to the end.
| shiandow wrote:
| Section 2 is a case by case analysis. Those are never
| pretty but perfectly normal given the problem.
|
| With OpenAI that part takes up about 2/3 if the proof even
| with its fragmented prose. I don't think it does much
| better.
| sweezyjeezy wrote:
| It's not it being case by case that's my issue. I used do
| olympiads and e.g. for the k>=3 case I wouldn't write
| much more than:
|
| "Since there are 3k - 3 points on the perimeter of the
| triangle to be covered, and any sunny line can pass
| through at most two of them, it follows that 3k - 3 <=
| 2k, i.e. k <= 3."
|
| Gemini writes:
|
| _Let Tk be the convex hull of Pk. Tk is the triangle
| with vertices V1 = (1, 1), V2 = (1, k), V3 = (k, 1). The
| edges of Tk lie on the lines x = 1 (V), y = 1 (H), and x
| + y = k + 1 (D). These lines are shady._
|
| _Let Bk be the set of points in Pk lying on the boundary
| of Tk. Each edge contains k points. Since the vertices
| are distinct (as k >= 2), the total number of points on
| the boundary is |Bk| = 3k - 3._
|
| _Suppose Pk is covered by k sunny lines Lk. These lines
| must cover Bk. Let L [?] Lk. Since L is sunny, it does
| not coincide with the lines containing the edges of Tk. A
| line that does not contain an edge of a convex polygon
| intersects the boundary of the polygon at most at two
| points. Thus, |L [?] Bk| <= 2. The total coverage of Bk
| by Lk is at most 2k. We must have |Bk| <= 2k. 3k - 3 <=
| 2k, which implies k <= 3._
| vessenes wrote:
| They actually do help - in that they give the model more
| computation time and also allow realtime management of the
| input context by the model. You can see this same behavior
| in the excessive comment writing some coding models engage
| in; Anthropic interviews said these do actually help the
| model.
| guluarte wrote:
| Looks like models can solve slightly modified problems and
| extrapolate from their training data, amazing! /s
|
| I will be surprised when a model with only the knowledge of a
| college student can solve these problems.
| akomtu wrote:
| Those who keep their identity in their intelligence are heading
| into the rough seas once the proto-AI becomes real-AI in the
| coming years. What's the value of your smart thoughts if AI on
| your smartwatch can do it better, faster and cheaper?
|
| Also, how is AI going to change a society ruled by
| competitiveness, where the winner takes all? You may not want to
| replace your thinking with AI, but your colleagues will. Their
| smartwatches or smartglasses will outcompete you with ease and
| your boss will tell you one day that the company doesn't need you
| anymore.
|
| Think of it again. Today advertisers fight each other with their
| ad budgets: those who spend more, get more attention and win.
| Tomorrow everyone will need a monthly subscription to AI for it
| will be the price of staying competitive, relevant and employed.
| kevinventullo wrote:
| _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 pages of writing, there is simply no way forward but
| to formalize. Otherwise, one cannot get past the bottleneck of
| needing a human reviewer to understand and validate the proof.
| kevinventullo wrote:
| (Stream of consciousness aside:
|
| That said, letting machines go wild in the depths of the
| consequences of some axiomatic system like ZFC may reveal a
| method of proof mathematicians would find to be monstrous. So
| like, if ZFC is inconsistent, then anything can be proven. But
| short of that, maybe the machines will find extremely powerful
| techniques which "almost" prove inconsistency that nevertheless
| somehow lead to logical proofs of the desired claim. I'm
| thinking by analogy here about how speedrunning seems to often
| devolve into exploiting an ACE glitch as early as possible,
| thus meeting the logical requirements of finishing the game
| while violating the spirit. Maybe we'd have to figure out what
| "glitchless ZFC" should mean. Maybe this is what logicians have
| already been doing heh).
| modeless wrote:
| These problems are designed to be solvable by humans without
| tools. No reason we can't give tools to the models when they go
| after harder problems. I think it's good to at least reproduce
| human-level skill without tools first.
| kevinventullo wrote:
| Oh so to be clear, I view formal methods as less of a useful
| tool, and more as enforcing a higher standard of proof. E.g.
| it's not clear to me that having access to Lean would
| actually help a human in the IMO; certainly most professional
| mathematicians are not yet getting a positive ROI from
| formalization. But I'm sort of an armchair expert here; I
| could be wrong!
| nicf wrote:
| 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 without some way to verify it
| formally. But I also don 't think we really want them all that
| much!
|
| 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. For example, I was never a
| number theorist, but I think most people who are informed
| enough to have an opinion think that the Riemann Hypothesis is
| probably true, and I know that they 're not actually waiting
| around to find out. There are lots of papers that get published
| whose results take the form "If the Riemann Hypothesis is true
| then [my new theorem]."
|
| The reason they'd still be excited by a proof is the hope,
| informed by experience with proofs of earlier long-standing
| open problems, that the proof would involve some exciting new
| method or perspective that would give us a deeper understanding
| of number theory. A proof in a formal language that Lean says
| is true but which no human being has any hope of getting
| anything from doesn't accomplish that.
| lblume wrote:
| I have always wondered about what could be recovered if the
| antecedent (i.e. in this case the Riemann hypothesis) does
| actually turn out to be false. Are the theorems completely
| useless? Can we still infer some knowledge or use some
| techniques? Same applies to SETH and fine-grained complexity
| theory.
| nicf wrote:
| I don't know enough about the RH examples to say what the
| answer is in that case. I'd be very interested in a
| perspective from someone who knows more than me!
|
| In general, though, the answer to this question would
| depend on the specifics of the argument in question.
| Sometimes you might be able to salvage something; maybe
| there's some other setting where same methods work, or
| where some hypothesis analogous to the false one ends up
| holding, or something like that. But of course from a
| purely logical perspective, if I prove that P implies Q and
| P turns out to be false, I've learned nothing about Q.
| mietek wrote:
| 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 the lessons of software
| engineering can and indeed should be applied to making proofs
| easier for humans to read.
|
| For a quick example, check out my mechanization of Martin-
| Lof's 2006 paper on the axiom of choice:
|
| https://research.mietek.io/mi.MartinLof2006.html
|
| Recent HN discussion:
|
| https://news.ycombinator.com/item?id=44269002
| nicf wrote:
| 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.
| mietek wrote:
| 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...
| daxfohl wrote:
| 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.
| david-gpu wrote:
| _> 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.
| kevinventullo wrote:
| 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.
| nicf wrote:
| 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.
| kurtis_reed wrote:
| Accurate formalization is presumably easier than solving the
| problems, so you can always formalize and check after the
| solution is generated
| lacker wrote:
| Typically formalization is actually harder than solving a
| problem. You almost always solve before formalizing. And it
| can be surprisingly hard to formalize problems that are easy
| to solve.
|
| For example, is there a polygon of area 100 that you can fit
| 99 circles of area 1 inside it, without overlapping? Yes,
| obviously, it's very easy to prove this informally. Now try
| formalizing it! You will find it takes a while to formalize a
| number of fairly obvious geometric statements.
| 7373737373 wrote:
| They aren't - they are currently collating a repository of
| formalized open problems: https://github.com/google-
| deepmind/formal-conjectures
| habibur wrote:
| Solved 5 problems out of 6, scoring 35 out of 42. For comparison
| OpenAI scored 35/42 too, days back.
| caconym_ wrote:
| I wouldn't read too much into the timelines, as it seems that
| OpenAI simply broke an embargo that the other players were up
| to that point respecting:
| https://arstechnica.com/ai/2025/07/openai-jumps-gun-on-inter...
|
| Very in character for them!
| neom wrote:
| How much of a big deal is this stuff? I was blessed with
| dyscalculia so I can hardly add two numbers together, don't pay
| much attention to the mathematics word, but my reading indicates
| this is extremely difficult/humans cannot do this?
|
| What comes next for this particular exercise? Thank you.
| danie123 wrote:
| Humans certainly can get gold at IMO: the threshold is chosen
| each year such that around 8% of students get it. So about 50
| students (worldwide) per year are awarded it. Also note that
| the competition is only for students who are still in school.
|
| Getting a gold is considered very impressive, but there are
| certainly plenty of humans in the world who can solve problems
| at that level, and even more so if you relax the time
| constraints of it being a competition environment. If you
| include people who are too old to be eligible for IMO, then
| there are maybe around 1,000-100,000 people in the world who
| could get a gold at IMO (the large range is because I think
| this quantity is quite hard to estimate).
|
| Another important thing to bear in mind is that research
| mathematics is quite different to competition mathematics, so
| it is quite tricky to tell how good these AIs will be at
| research maths.
| lblume wrote:
| There does seem to be a fairly strong correlation between
| excelling at competition and research mathematics
| respectively. The question remains whether this correlation
| generalizes to nonhuman cognition.
| jtlicardo wrote:
| At this point, I wonder how long software engineers will keep
| convincing themselves they're irreplaceable
| gyrovagueGeist wrote:
| Useful and interesting but likely still dangerous in production
| without connecting to formal verification tools.
|
| I know o3 is far from state of the art these days but it's great
| at finding relevant literature and suggesting inequalities to
| consider but in actual proofs it can produce convincing looking
| statements that are false if you follow the details, or even just
| the algebra, carefully. Subtle errors like these might become
| harder to detect as the models get better.
| sweezyjeezy wrote:
| 100% o3 has a strong bias towards "write something that looks
| like a formal argument that appears to answer the question"
| over writing something sound.
|
| I gave it a bunch of recent, answered MathOverflow questions -
| graduate level maths queries. Sometimes it would get
| demonstrably the wrong answer, but it not be easy to see where
| it had gone wrong (e.g. some mistake in a morass of algebra). A
| wrong but convincing argument is the last thing you want!
| Workaccount2 wrote:
| If nothing else, I'd imagine these tools will allow
| mathematicians to automate a lot of busy work that exists between
| ideas and validation.
| vouaobrasil wrote:
| This is making mathematics too systematic and mechanical, and it
| kills the joy of it....
| ted_dunning wrote:
| It didn't kill chess
| asdfologist wrote:
| It did partially, which is why top players are nowadays
| playing Freestyle (chess 960) more and more.
| xdavidliu wrote:
| this comment reminds me of that Feynman quote about others
| thinking scientific knowledge removes the beauty from a flower.
| of course Feynman disagreed
| irthomasthomas wrote:
| Woah they used parallel reasoning. An idea I opensourced about a
| month before GDMs first paper on it. Very cool.
| https://x.com/GoogleDeepMind/status/1947333836594946337 So you
| might be able to achieve similar performance at home today using
| llm-consortium https://github.com/irthomasthomas/llm-consortium
| Sol- wrote:
| > all within the 4.5-hour competition time limit
|
| Both OpenAI and Google pointed this out, but does that matter a
| lot? They could have spun up a million parallel reasoning
| processes to search for a proof that checks out - though of
| course some large amount of computation would have to be reserved
| for some kind of evaluator model to rank the proofs and decide
| which one to submit. Perhaps it was hundreds of years of GPU
| time.
|
| Though of course it remains remarkable that this kind of process
| finds solutions at all and is even parallelizable to this degree,
| perhaps that is what they meant. And I also don't want to
| diminish the significance of the result, since in the end it
| doesn't matter if we get AGI with overwhelming compute or not.
| The human brain doesn't scale as nicely, even if it's more energy
| efficient.
| lblume wrote:
| > They could have spun up a million parallel reasoning
| processes
|
| But alas, they did not, and in fact nobody did (yet).
| Enumerating proofs is notoriously hard for deterministic
| systems. I strongly recommend reading Aaronson's paper about
| the intersection of philosophy and complexity theory that
| touches these points in more detail: [1]
|
| [1]: https://www.scottaaronson.com/papers/philos.pdf
| foota wrote:
| Let's throw these deep learning models at the classification of
| simple finite groups and see if they can come up with something
| shorter than 1000 pages.
| Dzugaru wrote:
| Most critical piece of information I couldn't find is - how many
| shot was this?
|
| Could it understand the solution is correct by itself (one-shot)?
| Or did it have just great math intuition and knowledge? How the
| solutions were validated if it was 10-100 shot?
| aldousd666 wrote:
| The solutions were evaluated on their submitted output. You're
| allowed to use multiple 'shots' to produce the output, but just
| one submission per question. People are allowed this same
| affordance.
| sanjitb wrote:
| Why do they brag about not using a theorem prover? To me,
| whatever tool helps the model perform, go for it.
|
| Besides, they still specialized Gemini for the IMO in other ways:
|
| > we additionally trained this version of Gemini on novel
| reinforcement learning techniques that can leverage more multi-
| step reasoning, problem-solving and theorem-proving data. We also
| provided Gemini with access to a curated corpus of high-quality
| solutions to mathematics problems, and added some general hints
| and tips on how to approach IMO problems to its instructions.
| alephnerd wrote:
| > Why do they brag about not using a theorem prover
|
| Because this highlights that Gemini actually reasoned
| independently of other tools. That is a massive quantum leap in
| AI/ML. Abstract reasoning is arguably the basis of cognition.
| fpia wrote:
| 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
| tried DeepSeek (which has its own share of obstacles). But
| Gemini? never again.
| lblume wrote:
| I find Gemini Pro to be much more capable than GPT-4o at
| reading comprehension, code writing and brainstorming.
| dimitri-vs wrote:
| Yes, second this, I would go as far to say I use it more than
| o3.
___________________________________________________________________
(page generated 2025-07-21 23:00 UTC)