Mathematicians and AI in behind-the-scenes battle over what's true

AI models are solving mathematics problems with increasing pace, and a technique called formalisation is key to demonstrating that their claimed solutions are indeed correct. But can we trust the formalisation process?

AI has made staggering progress in mathematics in recent months, unearthing solutions to thorny puzzles that evaded humans for decades. Key to technology companies being able to announce these complex new findings, confident in their correctness, is a niche field called formalisation.

But recently, the developers behind formalisation tools have realised that the AI models have the potential to cheat their way to success. Now, the battle is on to tighten up the tools and prevent that from happening.

Formalising mathematical theorems essentially turns them into code that allows computers to grapple with them directly, methodically working through the logic and exposing any flaws. The process is so thorough that if a theorem comes through intact, it is considered to have been proved correct beyond all reasonable doubt.