Automated formal solution of 5 out of 6 IMO 2025 problems is achieved by Harmonic AI using their current Aristotle system. No claims of satisfying formal conditions for gold are made (neither in terms of runtime, nor (I think) in terms of unassisted autoformalization of problem statements). Fully automated solution synthesis is achieved after formal statements of problems are given. The system automatically annotates proofs with comments in key places. Formalization is in Lean.
Automated formal solution of 5 out of 6 IMO 2025 problems is achieved by Harmonic AI using their current Aristotle system. No claims of satisfying formal conditions for gold are made (neither in terms of runtime, nor (I think) in terms of unassisted autoformalization of problem statements). Fully automated solution synthesis is achieved after formal statements of problems are given. The system automatically annotates proofs with comments in key places. Formalization is in Lean.
Despite the limitations above, this is a very impressive result. The proofs are published: https://github.com/harmonic-ai/IMO2025. The livestream recording is here: https://x.com/HarmonicMath/status/1949951004482441362
They have just opened their waitlist for their first public form factor for Aristotle, an iOS app: https://aristotle.harmonic.fun/
My request for access has been approved very quickly (I don’t know them, but my background and my aims are a reasonable fit).