How much of the ATLAS of finite groups is independently checked and/or computer verified?

Unlike Dima, I am inclined to agree with Serre on this point. Although most of the facts recorded in the ATLAS have been proved elsewhere or, in the case of all of the character tables except for those of the very large groups like the Monster, can be easily recomputed in GAP or Magma using standard algorithms for finite groups, it can be very difficult in some cases to track down alternative proofs.

I have recently completed a book (co-authored with John Bray and Colva Roney-Dougal) calculating complete lists of maximal subgroups of almost simple classical groups in dimensions up to $12$, and we were confronted with this problem. Although we cited the ATLAS many times, we tried hard to provide alternative citations or, for facts that could be easily checked by computer, we provided code to do this. In fact nearly all of the facts we required were either about maximal subgroups of groups in the ATLAS or involved entries in character tables. For the sporadic groups there were virtually always alternative papers to cite, which were generally also cited in the ATLAS.

We had more difficulties with things like maximal subgroups of almost simple extensions of some of the more complicated classical groups in the ATLAS, like $U_4(3)$. For these we could not always find alternative sources that gave precise enough information, and we were told informally that some of the information had been originally calculated by unidentified research students or PostDocs. So we tried hard to re-prove these facts.

Having said that, we found remarkably few errors in the ATLAS. I think there might have been one or two very small and minor inaccuracies in some of the structure descriptions, which we reported to the authors, and I think they might have known about them already. I see that there is an "ATLAS 30 Years On" conference coming up in Princeton in November 2015, so perhaps this will lead to more discusssion of these questions.

I should also reinforce the point made by David Roberts that one needs to be very cautious when using Computer Algebra Systems, such as GAP and Magma, to verify facts contained in sources like the ATLAS, because it is possible that the code used is itself relying on these sources. For example $\mathtt{ MaximalSubgroups}$ in Magma will generally look up the maximal subgroups of the group's composition factors in a database, which will have been constructed using the ATLAS. However, a default use of $\mathtt{CharacterTable}$ on a finite group will use a general purpose algorithm (such as Dixon-Schneider), which does not rely on properties of specific (simple) groups.

The Atlas was a work of scholarship, not research. Our aim in those days was to collect information together for convenience, and the large character tables, and all the other data, was all proved. The fact that there were so many errors is down to human error - both in our sources and our own work.

Nevertheless it would be possible to re-compute much of it now fairly easily, and in particular computing the character tables of explicitly given matrices or permutations would be less heroic now than 30 years ago. The result would be that there exists a group with the proven properties. If anyone wants to have a go at that, I'd love to help.

The "uniqueness" part is more difficult. There is much published work on properties of simple groups, and the definition of the group studied would need to be somehow be connected to the (re)computed data. This would require further work. For example one would need to show for the first Conway group that the 24x24 matrices used to define the group fix an even unimodular lattice in 24 dimensions with minimum norm 4 and that there is an involution centralizer of the form 2.1+8.O8+(2) and so on.

There is no doubt that the project is feasible, and I had a short discussion with Serre on the subject. Let's hope someone cares enough to actually do it!

It may also worth to look at the paper

T. Breuer, G. Malle, and E. A. O'Brien, Reliability and reproducibility of Atlas information, Contemporary Mathematics 694 (2017) pp 21–31, doi:10.1090/conm/694/13960, arXiv:1603.08650

in which is discussed the reliability and reproducibility of much of the information contained in the Atlas of Finite Groups.