Timeline for Known and fixed gaps in the proof of the CFSG
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 25, 2021 at 20:15 | comment | added | Carl-Fredrik Nyberg Brodda | @PaulTaylor Here are two relevant questions. See Ben Steinberg's answer to the first. I think the answer to your question boils down to: the statement of the CFSG is not even yet formalised, let alone the proof. (But I say this as an outsider both to CFSG and proof assistants). | |
| Sep 25, 2021 at 13:38 | comment | added | Richard Lyons | The Odd order theorem has been verified. Beyond that I am the wrong person to ask. | |
| Sep 25, 2021 at 8:56 | comment | added | Paul Taylor | How much of this proof has been verified so far using proof assistant programs? Is anyone working on that actively? (I ask as an outsider, but I was a grad student in Cambridge when the Atlas was published.) | |
| Sep 23, 2021 at 19:05 | comment | added | Carl-Fredrik Nyberg Brodda | Though it's unfortunate (for this question) that no log was kept, this is still an excellent answer. Thank you! (When you mentioned it, I now recall seeing the order $5$ vs $25$ issue mentioned in an erratum paper). | |
| Sep 23, 2021 at 19:02 | vote | accept | Carl-Fredrik Nyberg Brodda | ||
| Sep 23, 2021 at 17:10 | history | answered | Richard Lyons | CC BY-SA 4.0 |