cross-posted from: https://news.abolish.capital/post/41854
A Chinese artificial intelligence framework has autonomously resolved an open problem proposed more than a decade ago by a US mathematician, according to the Peking University-led team that developed it. The dual-agent framework solved the problem posed in 2014 by former University of Iowa professor Dan Anderson – who died in 2022 at the age of 73 – the researchers said in a preprint paper published on April 4. By synthesising decades of mathematical literature, the Chinese team’s AI framework…
According to the article they used formal verification, that’s an important part of automated math research (and increasingly human research too).
This is not new btw, around the new year there was a bunch of new automated / semi-automated proofs using LLMs + formal verification with Lean of some Erdos problems