The newest models are solving some of the hardest Math Olympiad problems [1]. This is in the top 1% of the top 1% math students out of high school.

The math performance, even for VERY hard problems, is already getting extremely good and progress is still high year-on-year.

What OpenAI (and everyone else, less publicly) seem to be doing, is to integrate these kinds of abilities into multi-modal models.

https://deepmind.google/discover/blog/ai-solves-imo-problems...

It seems misleading to lump AlphaGeometry in with this: that system works by having an LLM generate hundreds of Lean programs and trying to find the one that works. Frankly the project is pointless and borderline dishonest: it is a hideously expensive way to solve useless Olympiad problems, but it won't work at all for actual mathematical research since we wouldn't have nearly enough training data. It does not represent even the slightest advancement at AI performing mathematics, it's pure gimmickry. I suspect the entire point of AlphaGeometry is to generate comments like yours, "AI is now an Olympian-level mathematician."

The real AI math advancement will be a computer which is as smart as a pigeon and innately understands what a number is, which means it is able to solve simple counting problems without training. AlphaGeometry or Strawberry aren't even close to that, and I suspect none of us will live to see such a sophisticated AI.

Yeah sure, but AlphaProof is "cheating", because they are using an external system to do the hard work and the LLM is just there for translation and semantic information retrieval.

As impressive as it is, it makes LLMs look like they are just a fancy UI. Like, you can tell the computer to press the upvote button in English using your voice instead of using your mouse.

It's the same with AlphaProof. The LLM is just taking a problem specification in natural language and then acting as the UI of the theorem prover.

The moment you talk about using LLMs to solve decidable problems, people whip you with the idea that you should let the LLM generate python code. Aka, the LLM is just a fancy UI for specifying python programs in English.

Cool, but also somewhat hollow. It's no different than having a translator from one language to another.

What percentage of work being done daily requires solving harder than "high-school" problems? Single digits? Low double digits? If it actually becomes capable of doing this we might move on into it actually being deployable to real world jobs.

It is already being deployed to real-world jobs.

Let me rephrase, to a *much* higher percentage of real-world jobs that require solving harder than "high-school" problems. Right now the lack of real determinism and trust means that you can't really leave it unsupervised 100% of the time.

"They showed it to the feds" means "Competition has more than caught up and is beating us, so we'll now sell to the most clueless buyer: one that has unlimited budget".

When General Paul M. Nakasone, who until just recently was near the top of the chain for Cyber Command in the US Armed Forces, joined the OpenAI board, it could be seen in multiple ways.

My take is that this wasn't something OpenAI did as a PR stunt, but rather that the military started seeing this tech as being critical to national security, and basically forced OpenAI to take him on the board.

That's not necessarily good for stock prices. If AI beyond some capability are labelled as strategic military assets, then the Nvidia export restrictions may end up a pale foreshadowing of what AI companies could be facing soon.

Compare to the Microsoft HoloLens project, which peddles VR goggles to the U.S. Army:

https://www.cnbc.com/2021/03/31/microsoft-wins-contract-to-m...

I am sure it will be a raging success among the troops on the ground.