Google developed AI models that achieved on this year’s IMO questions a silver-medal (with only one point away from a gold-medal). You can read more about it in this blog post of Google: link.
The for me most interesting thing in this news is not that it achieves a silver-medal, but how the system works, namely that it incorporates LEAN. Let me cite a sentence from the above mentioned blog post: When presented with a problem, AlphaProof generates solution candidates and then proves or disproves them by searching over possible proof steps in Lean.
So the system basically works like a human mathematician: One first comes up with an idea of how to solve a problem or how to prove a statement, and then tries to verify it thoroughly by trying to write down a full proof in all details.
For this particular attempt on the IMO, the problems where first translated by hand into formal statements to feed them into the AI. But as they write at the end of the blog post, they also tried to automate this by feeding the problems as they are into a natural language model first.
I am excited about this development, since the AI formally verifying its own proposed solution in LEAN complete solves the problem with hallucination (at least in math) and therefore the system becomes much more reliable.