All Questions

While people are steaming ahead on finessing the proof of the classification of finite simple groups (CFSG), we have a formal proof in Coq of one of the first major components: the Feit-Thompson odd-...

I probably don't have the appropriate background to even ask this question. I know next to nothing about formal or computer-aided proof, and very little even about group theory. And this question is ...