All Questions

In a recent talk Finite groups, yesterday and today Serre made some comments about proofs that rely on the classification of finite simple groups (CFSG) and on the ATLAS of Finite Groups. Namely, he ...

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 ...