Google's AI is now able to compete in Math Olympiads and rank among top three (www.mundoamerica.com)

Google DeepMind published in Nature AlphaProof, a formally verified AI system that can solve high-school–level Olympiad problems and was tested on IMO 2024. Trained with massive amounts of formalized mathematics (the team reports self-formalizing roughly 80 million statements) and built on pre-trained models plus specialist modules (it used AlphaGeometry 2 for the geometry problem), AlphaProof independently solved three of six IMO problems in algebra and number theory, producing solutions that are automatically checked step-by-step in a formal proof environment. Its performance equated roughly to a silver-medalist result, though solutions took two to three days of computation versus four hours for human contestants. The work is significant because it moves beyond humanlike natural-language proofs to machine-checkable, verifiable reasoning, closing an important trust gap for applications that need certainty. Key technical implications: success depends on huge formal corpora, specialist subsystems, and substantial compute, and the system still struggles with combinatorics and genuinely novel mathematical creativity outside seen patterns. Near-term impacts include more reliable automatic graders, exercise-generation tools, and assistants for checking routine proof steps; longer-term potential hinges on reducing compute costs and broadening the range of formalized mathematics toward open research.