But then inevitably I find myself wondering whether a proof assistant, or even a formal system, can make the distinction between “technical” and “fundamental” questions. There seems to be no logical distinction. The formalist answer might involve algorithmic complexity, but I don’t think that sheds any useful light on the question. The materialist answer (often? usually?) amounts to just-so stories involving Darwin, and lions on the savannah, and maybe an elephant, or at least a mammoth. I don’t find these very satisfying either and would prefer to find something in between, and I would feel vindicated if it could be proved (in I don’t know what formal system) that the capacity to make such a distinction entails appreciation of music.
Peirce proposed a distinction between corollarial and theorematic reasoning in mathematics that strikes me as similar to the distinction that Michael Harris seeks between technical and fundamental questions.
I can’t say I have a lot of insight into how the line might be drawn, but I recall a number of traditions pointing to the etymology of theorem as having to do with the observation of objects and practices whose depth of detail always escapes full accounting by any number of partial views.
On the subject of music, all I have is this incidental —
Perhaps it takes a number theorist to appreciate it …