The aim is to verify a library of algorithms for listing combinatorial objects: permutations, subsets, partitions, trees, … . There is a rich literature on the subject (see below). Part of the challenge is to find elegant functional programs instead of the universally imperative algorithms given in the literature (Nijenhuis and Wilf even give Fortran programs!). You can find a first Isabelle example here
 Nijenhuis and Wilf. Combinatorial Algorithms
 Stanton and White. Constructive Combinatorics
Prerequisites: Some familiarity with Isabelle/HOL.