Isabelle/HOL solutions to math contest problems

This repository contains various Isabelle/HOL formal proofs. This is mostly solutions to interesting math olympiad problems, but some higher math exercises have found their way here, too.

Apart from that, I keep some notes on the mathematical library of Isabelle. This includes situations where the structure and interaction of objects

I encourage you to explore.

Problems by tag

• number theory [8 problems]

  • BMO1 2015 Problem 2 (number theory)
  • Canada MO 2020 Problem 1 (number theory)
  • Greece MO 2007 Problem 1 (number theory)
  • Polish MO 1969 Round 1 Problem 1 (number theory, diophantine equation)
  • Polish MO 1969 Round 1 Warmup Problem A (number theory, congruences)
  • Polish MO 2020 Round 1 Problem 3 (number theory)
  • Polish MO 2020 Round 2 Problem 3 (number theory)
  • USAMO 2006 Problem 5 (number theory, combinatorics, nondeterministic process)
• combinatorics [4 problems]

  • APMO 2013 Problem 4 (combinatorics)
  • IMO 2019 Problem 5 (combinatorics)
  • Polish MO 2020 Round 2 Problem 1 (combinatorics)
  • USAMO 2006 Problem 5 (number theory, combinatorics, nondeterministic process)
• functional equation [3 problems]

  • Deltami 44M Problem 789 (functional equation)
  • IMO 2019 Problem 1 (functional equation)
  • Unknown Origin Problem 1 (functional equation)
• real analysis [3 problems]

  • IMC PoTD 15 (real analysis)
  • Polish MO 1969 Round 1 Problem 2 (real analysis)
  • Polish MO 1969 Round 1 Warmup Problem B (inequality, multiple solutions, real analysis)
• inequality [3 problems]

  • Polish MO 1969 Round 1 Problem 5 (inequality)
  • Polish MO 1969 Round 1 Warmup Problem B (inequality, multiple solutions, real analysis)
  • Polish MO 2020 Round 1 Problem 1 (inequality)
• group theory [2 problems]

  • Napkin Problem 1A (group theory)
  • Napkin Problem 1B (group theory)
• diophantine equation [1 problem]

  • Polish MO 1969 Round 1 Problem 1 (number theory, diophantine equation)
• congruences [1 problem]

  • Polish MO 1969 Round 1 Warmup Problem A (number theory, congruences)
• multiple solutions [1 problem]

  • Polish MO 1969 Round 1 Warmup Problem B (inequality, multiple solutions, real analysis)
• equation over reals [1 problem]

  • Polish MO 1969 Round 1 Warmup Problem C (equation over reals)
• metric space [1 problem]

  • Polish MO 1969 Round 1 Warmup Problem D (metric space, geometry)
• geometry [1 problem]

  • Polish MO 1969 Round 1 Warmup Problem D (metric space, geometry)
• nondeterministic process [1 problem]

  • USAMO 2006 Problem 5 (number theory, combinatorics, nondeterministic process)

Problems by origin

• Asia Pacific Math Olympiad [1 problem]

  • 2013
    • Problem 4 (combinatorics)
• British Maths Olympiad Round 1 [1 problem]

  • 2015
    • Problem 2 (number theory)
• Canada Math Olympiad [1 problem]

  • 2020
    • Problem 1 (number theory)
• Deltami 44M [1 problem]

  • Problem 789 (functional equation)
• Greece Math Olympiad [1 problem]

  • 2007
    • Problem 1 (number theory)
• Instagram Math Community [1 problem]

  • PoTD 15 (real analysis)
• International Math Olympiad [2 problems]

  • 2019
    • Problem 1 (functional equation)
    • Problem 5 (combinatorics)
• An Infinitely Large Napkin [2 problems]

  • Problem 1A (group theory)
  • Problem 1B (group theory)
• Polish Math Olympiad [11 problems]

  • 1969

    • Round 1
      • Problem 1 (number theory, diophantine equation)
      • Problem 2 (real analysis)
      • Problem 5 (inequality)
      • Warmup Problem A (number theory, congruences)
      • Warmup Problem B (inequality, multiple solutions, real analysis)
      • Warmup Problem C (equation over reals)
      • Warmup Problem D (metric space, geometry)

  • 2020

    • Round 1

      • Problem 1 (inequality)
      • Problem 3 (number theory)

    • Round 2

      • Problem 1 (combinatorics)
      • Problem 3 (number theory)
• United States of America Math Olympiad [1 problem]

  • 2006
    • Problem 5 (number theory, combinatorics, nondeterministic process)
• Unknown Origin [1 problem]

  • Problem 1 (functional equation)

Structure of this repository

Raw Isabelle .thy files are hard to look at. As can be expected for math, lots of non-ASCII characters are involved. Apart from font issues, Isabelle actually predates Unicode, so the text files are actually encoded with LaTeX-ish escape sequences.

This motivates a sophisticated CI setup (the three words you don't ever want to see next to each other). The master branch of the repository keeps the sources, while GitHub Actions render PDFs and push them onto the built-pdfs branch.