This blog is intended to present simple mathematical problems, where providing constructive and fully formalized solutions presents a fun challenge. My intention is that each problem should be solvable in a short amount of time with a little bit of effort and creativity. Throughout this blog, I will stick to using the proof assistant Coq.

Each problem will be presented with an explanation as well as a template Coq file providing the necessary definitions and goals. Aftera few days, I’ll submit a Coq file containing a solution along with a detailed exposition.

Feedback or problem suggestions are very much welcome.