A methodical attack on the "Project Euler" programming challenges.
Project Euler is a well known collection of math-based programming challenges. There are currently over 600 problems, and new ones are added every few weeks. They range in difficulty from fizz-buzz level problems to extremely difficult and intricate puzzles even a professional computer scientist would find challenging. The problems can be found at: https://projecteuler.net. Once you think you've found an answer, you can enter it to see if you're right. (Submitting answers requires an account; making one is free and does not require any information other than a username and password.)
I figures Idris is a rather appropriate language for attacking math-based programming puzzles, considering its relationship to mathematical logic (see Curry-Howard isomorphism) and seeing as one can actually prove programs correct.