Axiom Math, IMO 2026 여섯 문제 Lean 4 증명 공개

Axiom Math가 GitHub에 공개한 자료에 따르면 자율 다중 에이전트 정리증명기 ‘AxiomProver’는 국제수학올림피아드(IMO) 2026의 여섯 문제를 Lean 4 형식 증명으로 풀었다. 회사는 이를 42점 만점에 해당하는 결과라고 평가했으며, 문제별 형식화와 전체 증명 코드를 공개 저장소에 올렸다.

저장소는 각 문제를 Q1부터 Q6까지 나누고, 자연어 문제를 Lean 정리로 옮긴 problem.lean 파일과 증명을 담은 solution.lean 파일을 함께 제공한다. 풀이 코드는 Mathlib 4.31.0을 기준으로 작성됐다. Axiom Math는 각 문제와 풀이의 호환성을 확인하는 검증 스크립트도 공개했다.

회사 자료에 기록된 문제별 처리 시간은 24분에서 869분 사이다. Q1은 24분, Q2는 360분, Q3은 869분, Q4는 39분, Q5는 65분, Q6은 139분으로 제시됐다. 가장 긴 Q3 풀이 코드는 4,229줄이며, 여섯 풀이를 합치면 7,722줄이다. 다만 병렬 실행 여부와 사용한 연산 자원 등 비교에 필요한 세부 조건은 저장소에 공개되지 않았다.

형식 증명은 풀이가 선언된 공리와 규칙을 따라 결론에 도달하는지 기계적으로 검사할 수 있다는 점에서 자연어 답안과 다르다. 공개된 solution.lean 파일에서는 미완성 증명에 쓰이는 sorry나 admit 표현이 확인되지 않는다. 저장소의 verify.py는 Axiom Math의 Axle 검증 서비스를 호출해 여섯 문제의 문제·풀이 쌍을 확인하도록 구성됐다.

IMO 공식 사이트는 2026년 대회 문제 여섯 개를 공개하고 있다. 대회는 중국 상하이에서 7월 10일부터 21일까지 열리며, Axiom Math 저장소는 공식 문제 페이지를 원문 출처로 연결했다. 공개 시점은 여섯 문제가 모두 출제된 뒤다.

다만 이번 결과는 IMO 조직위원회가 채점하거나 인증한 참가 성적이 아니다. ‘42/42’는 Axiom Math가 형식 증명 완성을 IMO 배점에 대응해 표현한 자체 평가다. 자연어 문제를 Lean 정리로 옮긴 형식화가 원문의 의미를 정확히 보존했는지에 대해서도 별도의 수학적 검토가 필요하다.

이번 공개는 수학 추론 모델의 성능을 정답률만으로 제시하는 대신, 제3자가 내려받아 검사할 수 있는 증명 코드로 내놓았다는 점에서 의미가 있다. 앞으로의 평가는 증명 완성 여부뿐 아니라 형식화 정확성, 연산 자원, 실행 시간, 재현 절차를 함께 공개하는 방향으로 더 엄격해질 것으로 보인다.

출처: Axiom Math GitHub https://github.com/AxiomMath/IMO2026
출처: 국제수학올림피아드 공식 사이트 https://www.imo-official.org/problems/2026/