The International Mathematical Olympiad (IMO), held annually since 1959, is the premier competition for young mathematicians, with participants solving six challenging problems across various fields. Top performers receive medals, with around 8% earning gold. Recently, AI systems like Google DeepMind's AlphaProof and AlphaGeometry 2 have aimed to reach human elite levels, achieving a silver medal by solving four problems. This progress shows AI is nearing advanced human mathematical reasoning. This year, our team joined an inaugural group using formal languages to further explore and enhance AI's capabilities in mathematical problem-solving and reasoning.

本专栏通过快照技术转载，仅保留核心内容

内容中包含的图片若涉及版权问题，请及时与我们联系删除