In this post, I will try to explain what my Ph.D. is going to be about – of course, you can just read my proposal, but I assume that’s not really accessible to a lay-person. The broad topic is knowledge management across formal libraries, specifically libraries of formal mathematics obtained from (mostly) various computer-supported theorem…