231–240 of 254 posts
That's some big news. I'm a little sad about how this genuine effort - coordinated with and judged by IMO - is "front ran" by a few random tweets of OpenAI, though. Says a lot about the current situation of this industry.
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 s…
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.
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.
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!
Sounds like no one requested that OpenAI wait a week: >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.
>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.
I use o3, openAI API and Claude Code. Genuinely curious what about Gemini 2.5 is so far behind?
Earlier quoted context omitted.
I'm aware the Nakamura example is old, but the core issue (the horizon effect) is still there in any alpha/beta pruning engine, including the newest SF. But I will certainly grant you that it has become much harder to execute since then. MCTS engines (like Lc0) are far more immune to the horizon effect, but can instead suffer from missing very shallow tactics, especially in very fast time controls, as Andrew Tang sho…
There's a beautiful game between SF and Lc0 (a few months ago) where Stockfish thinks it's winning, while Lc0 has a lock on a draw. Lc0 then proceeds to sack 4 pieces and draw, but SF (with NNUE) only "sees" the draw 2 moves into the position.
Indeed a good showcase of the horizon effect between an a/b and a MCTS engine, thanks for sharing!
This is making mathematics too systematic and mechanical, and it kills the joy of it....
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
@tao I think there is a broader problem wherein competitions (math, programming, games, whatever) are meant to measure something difficult for humans, but tools work so fundamentally differently from us that success for a tool isn't even necessarily meaningful. AI companies have long viewed the IMO Grand Challenge as a sign of achieving "AGI," but no matter what set of rules a machine follows, there's no reason to believe success for a machine will correlate with broader mathematical or "reasoning" abilities in the way it does for human participants.
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!
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…