@andrejbauer@mathstodon.xyz @tao@mathstodon.xyz Only combinatorics. I still maintain that it would be an extremely long project to even *state* the main theorems in any of the recent papers written by Toby Gee or Ana Caraiani, two other number theorists in my department. And proving them would be completely inaccessible -- even proving FLT is a gigantic project and this is from the 90s. There are still lots of problems in the way of making formalisation of all modern mathematics easy.