harmonic-ai/IMO2025

Lean

4 commits

updated Jul 30, 2025

README

Harmonic's IMO 2025 Results

Harmonic's model Aristotle achieved gold medal performance, solving 5 problems. This repository contains the lean statement files and proofs for Problems 1-5.

Contributors

lawrence-harmonic

2 commits

m-harmonic

2 commits

Similar repos

aw31/openai-imo-2025-proofs

481

google-deepmind/superhuman

803

Goedel-LM/MathOlympiadBench

Dataset

This repository contains the MathOlympiadBench dataset, which is introduced in the paper…

AxiomMath/IMO2026

102

ByteDance-Seed/Seed-Prover

443

AxiomMath/Putnam2025

Our solutions to Putnam 2025.

113

ArjunPanickssery/ai-math-debate

AI debate on math problems

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

Languages

Lean

100.0%

harmonic-ai/IMO2025

Lean

4 commits

updated Jul 30, 2025

See the code

README

Harmonic's IMO 2025 Results

Harmonic's model Aristotle achieved gold medal performance, solving 5 problems. This repository contains the lean statement files and proofs for Problems 1-5.

Similar repos

aw31/openai-imo-2025-proofs

481

google-deepmind/superhuman

803

Goedel-LM/MathOlympiadBench

Dataset

This repository contains the MathOlympiadBench dataset, which is introduced in the paper…

AxiomMath/IMO2026

102

ByteDance-Seed/Seed-Prover

443

AxiomMath/Putnam2025

Our solutions to Putnam 2025.

113

ArjunPanickssery/ai-math-debate

AI debate on math problems

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

Contributors

lawrence-harmonic

2 commits

m-harmonic

2 commits

Languages

Lean

100.0%