201–210 of 254 posts
This is making mathematics too systematic and mechanical, and it kills the joy of it....
At least we can all wait tables and sell crap at convenience stores when it takes over our jobs.
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.
Solved 5 problems out of 6, scoring 35 out of 42. For comparison OpenAI scored 35/42 too, days back.
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!
>We weren't in touch with IMO. I spoke with one organizer before the post to let him know. He requested we wait until after the closing ceremony ends to respect the kids, and we did.
https://x.com/polynoamial/status/1947024171860476264?s=46
https://x.com/polynoamial/status/1947398531259523481?s=46
(I work at OpenAI, but was not part of this work)
Earlier quoted context omitted.
Accurate formalization is presumably easier than solving the problems, so you can always formalize and check after the solution is generated
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 fo…
Earlier quoted context omitted.
4.5 hours × 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
100 watts seems very low. A single Nvidia GeForce RTX 5090 is rated at ~600 watts. Probably they are using many GPUs/TPUs in parallel.
If the computer uses ~600W, let's give it 45+45 minutes and we are even :) If they want to use many GPU ...
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
Earlier quoted context omitted.
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.
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 cont…
This is not true, at least not in very long time formats like correspondence chess: https://en.chessbase.com/post/correspondence-chess-and-corre...
There's also many well known cases where even very strong engines miscalculate and can be beaten (especially in fast time controls or closed positions): https://www.chess.com/blog/SamCopeland/hikaru-nakamura-crush...
The horizon effect is still very real in engines, although it's getting harder and harder to exploit.
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 hum…
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.
apparently IMO emailed them. but then they completed the IMO eval independently.
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…
If a Language Model is capable of producing rigorous natural language proofs then getting it to produce Lean (or whatever) proofs would not be a big deal. Lean use in AlphaProof was something of a crutch (not saying this as a bad thing). Very specialized, very narrow with little use outside any other domain. On the other hand, if you can achieve the same with general RL techniques and natural language then other hard…
This is a wildly uninformed take. Even today there are plenty of basic statements which LLM’s can produce English language proofs of that have not been formalized.
Earlier quoted context omitted.
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/
Kind of disappointing that neither provider shows the unsuccessful attack on problem 6.
> We achieved this year’s result using an advanced version of Gemini Deep Think – an enhanced reasoning mode for complex problems that incorporates some of our latest research techniques, including parallel thinking. This setup enables the model to simultaneously explore and combine multiple possible solutions before giving a final answer, rather than pursuing a single, linear chain of thought. [...] We will be making a version of this Deep Think model available to a set of trusted testers, including mathematicians, before rolling it out to Google AI Ultra subscribers.