AI已能攻克研究级数学难题

Artificial intelligence can now solve research problems in mathematics and verify the answers Jeremy Avigad1 and Matthew Ballard2 Every year, at the International Mathematical Olympiad (IMO), precollege students from around the world compete to solve difficult mathematical problems. In 2019, a team of researchers proposed the IMO Grand Challenge, which encouraged researchers to build artificial intelligence (AI) systems to solve IMO problems at the level of a gold medalist. The challenge required the systems to produce proofs that can be checked by a computational proof assistant such as Lean. In 2024, Google DeepMind’s AI system, AlphaProof, provided Lean with proofs of three of the competition’s problems. A year later, four AI systems performed at the level of a gold medalist. …