Some problems are ‘uninteresting’ in that they show results that aren’t immediately seen as useful. However, solutions may end up having ‘interesting’ connections or ideas or mathematical tools that are used elsewhere.

More broadly, I think there’s a perspective that literally just building out thousands more true statements in Lean is going to keep cementing math’s broadening knowledge framework. This is not building a giant castle a-la Wiles, it’s laying bricks in the outhouse, but someday those bricks might be useful.