Math Theorem Prover

This repository contains formal proofs of 5 problems from the International Mathematical Olympiad (IMO) using the Isabelle theorem prover. Each problem is carefully proven step-by-step, showcasing the use of Isabelle for solving mathematical challenges.
It was part of the Introduction to Interactive Theorem Proving course in the final year of undergraduate studies

What is Isabelle?

• Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide.
• Download from the link

Folder structure

• problems/ - Problem formulation
• proofs/ - Problem proof in LaTeX
• problem1.thy - Problem 1 solved in Isabelle
• problem2.thy - Problem 2 solved in Isabelle
• problem3.thy - Problem 3 solved in Isabelle
• problem4.thy - Problem 4 solved in Isabelle
• problem5.thy - Problem 5 solved in Isabelle