The link: Google's blog post about the AI that performed at Silver-medal level in the latest International Mathematical Olympiad.

The obvious takeaway: That's not something that would have seemed feasible not too long ago; in many ways, it's a more impressive achievement than most "ChatGPT can do this now" news.

The not-so-obvious takeaway: It's not (only) a large language model. Most AI-driven projects nowadays focus on attempting to find the right combination of prompt chains and context to get a general-purpose language models to do something. Alpha Proof and Alpha Geometry 2, instead, leverage general-purpose language models to help formalize and take advantage of existing sets of problems leveraging the well-known Lean formal proof system, and then turn it over to versions of Alpha Zero that are specially trained to work on those formal representations. This approach isn't in itself innovative, yet the fact that the pieces are now in place to do it at this level of performance is deeply meaningful.

For all the talk about the importance of figuring out how to make the best prompt, the AIs that will dominate key markets will not be built on big foundational LLMs except as preprocessing tools to access some data regrettably locked in natural language by obsolete processes. The cognitive architecture is probably going to look like a version of what Google just did: Expressing knowledge and problems in appropriate formal representations and then solving them by pairing domain-specific processing tools with specially trained optimization and tactical engines.

Don't get too attached to the prompt-the-LLM approach to AI. It'll remain useful — language is the universal, well, language — but it's not what the economy-defining game for superhuman abilities is going to be played with.