I know this is a bit of a white whale and there is a lot of mathematics to formalize before this is even in reach. But when the formal math community (taken as a whole) is at 99 out of 100 of the Top 100 list, of course it is easy to focus on the one.
Anyway the news is that there was a recent talk on formalizing local field class theory which apparently is one of the things that will be needed. https://mathstodon.xyz/@tao/109877480759530521 -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/801A5DE1-7B74-4059-9430-9EED5A938689%40panix.com.
