In the Proof Olympiad, answers must incorporate a proof of correctness that is verifiable by computer. Participants prepare their proofs in an interactive theorem-proving system, such as Lean, [Isabelle, or Coq.]
There are two problem categories: (1) Queries, where you must provide an answer, like a traditional math contest, and then provide a proof that it is correct, and (2) Theorems, where you are presented with the statement of a theorem and must provide a proof.
The competition is open to the public, including high school, undergraduate, and graduate students, and also to experienced professionals, with winners announced in those four groups. Olympiad questions will incorporate a range of difficulty, with the easiest accessible to beginners and with the hardest challenging to experts.
To get ready, review the background materials and the sample questions and try submitting answers to the sample questions to our automatic grading system. Answers will be accepted in the Lean, Isabelle, and Coq formats--get started by choosing one. A quick way to get started is by playing the Natural Number Game lean. Be forewarned--developing formal proofs can be challenging even on easy questions, so practice as much as you can.
The Proof Olympiad will run for two weeks, during July 6 at 12 am (EST) to July 20 at 12 am (EST). You are free to consult online and offline information sources, but not other individuals. You may not post your solutions or consult solutions shared by others.