CoChat
Sign Up
Cited by 4Logic, programming, and type systemsMathematics, Computing, and Information ProcessingFormal Methods in Verification

The DOI matches its Crossref record.

Formalizing IMO Problems and Solutions in Isabelle/HOL

Open access
Marić, Filip, Stojanović-Đurđević, Sana·2020·Electronic Proceedings in Theoretical Computer Science
DOI 10.4204/eptcs.328.3
Open this paper in CoChat — free account

Abstract

The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires to build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public repository of mechanically checked solutions of IMO Problems in the interactive theorem prover Isabelle/HOL. This repository is actively maintained by students of the Faculty of Mathematics, University of Belgrade, Serbia within the course "Introduction to Interactive Theorem Proving".

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.4204/eptcs.328.3

Cites

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

No references could be resolved yet.

Research works printed but not linked: 8

  1. Djuki\'c, 2011, The IMO compendium, 10.1007/978-1-4419-9854-5 · DOI
  2. Eberl, 2019, Selected Problems from the International Mathematical Olympiad 2019, Archive of Formal Proofs
  3. Génevaux, 2011, Formalization of Wu's Simple Method in Coq, 71, 10.1007/978-3-642-25379-9_8 · DOI
  4. Janiči\'c, 2012, The Area Method: a Recapitulation, Journal of Automated Reasoning, 48, 489, 10.1007/s10817-010-9209-7 · DOI
  5. Nipkow, 2020 (accessed Jun 20, 2020), Programming and Proving in Isabelle/HOL
  6. Pham, 2011, A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry, 368, 10.1007/978-3-642-21898-9_32 · DOI
  7. Stojanovi\'c-\begingroupłet [Pleaseinsert\PrerenderUnicodeÐintopreamble]ur\IeCđ evi\'c, 2019, From informal to formal proofs in Euclidean geometry, Annals of Mathematics and Artificial Intelligence, 85, 10.1007/s10472-018-9597-7 · DOI
  8. Wiedijk, 2006, The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence), 10.1007/s11225-007-9093-2 · DOI

Cited by

Sorted by citations

See all 4

Metadata

Authors
Marić, F., & Stojanović-Đurđević, S.
Affiliations
University of Belgrade (RS)
Venue
Electronic Proceedings in Theoretical Computer Science
Publisher
Open Publishing Association
Published
2020-10-30
Volume
328
Pages
35-55
ISSN
2075-2180 (ISSN-L)
DOI
10.4204/eptcs.328.3
OpenAlex
W3095074845
Cited by
4
References
0
Citations by year
2026: 1 · 2024: 2 · 2021: 1
FWCI
0.29
Type
journal article
Language
en
Open access
Licence
cc-by-nc-nd
Locations
  • Electronic Proceedings in Theoretical Computer Science (publishedVersion, cc-by-nc-nd)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Mathematics, Computing, and Information Processing
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
International Mathematical Olympiad, interactive theorem proving, Isabelle/HOL

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review

How to cite

Cite CoChat for the checks on this page, and the paper for its own findings.

This page
CoChat. (2026). Citation check: Formalizing IMO Problems and Solutions in Isabelle/HOL. https://app.cochat.ai/papers/10.4204/eptcs.328.3
The paper
Marić, F., & Stojanović-Đurđević, S. (2020). Formalizing IMO Problems and Solutions in Isabelle/HOL. Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/eptcs.328.3