Some figures about the Feit-Thompson proof

The proof is composed in 122 files. We split them in 4 groups:
  1. SSR: 61 files that are part of the SSreflect distribution
  2. MORE: 29 files that propose some extensions to the SSreflect distribution
  3. BG: 18 files that compose the Bender and Glauberman formalisation
  4. PF: 14 files that compose the Peterfalvi formalisation
In the following ALL refers to all the files

Definitions, theorems

We first give some basic facts of the proof: number of lines with its percentage with respect to the total number of lines, number of definitions with its respective percentage, number of theorems with its respective percentage and finally the ratio between theorems and definitions

SSR

Number of lines Number of definitions Number of theorems Ratio
87427 (55%) 3122 (74%) 9663 (73%) 3.1

MORE

Number of lines Number of definitions Number of theorems Ratio
30239 (19%) 871 (21%) 2412 (18%) 2.8

BG

Number of lines Number of definitions Number of theorems Ratio
20953 (13%) 96 (2%) 685 (5%) 7.1

PF

Number of lines Number of definitions Number of theorems Ratio
19741 (13%) 127 (3%) 485 (4%) 3.8

ALL

Number of lines Number of definitions Number of theorems Ratio
158360 (100%) 4216 (100%) 13245 (100%) 3.1

Proof length distribution

SSR

There are 9316 proofs. The largest proof has 227 lines. The medium length is 3.8. The standard deviation of 7.2. Here is the distribution as a table

1 2 3 4 5 6 7 8 9 10-19 20-29 30-39 40-49 50-59 60-69 70-79 80-89 90-99 100-199 200-300
5295 2 563 1366 678 353 254 154 99 370 85 34 17 9 10 6 3 3 14 1

or as a chart

MORE

There are 2363 proofs. The largest proof has 210 lines. The medium length is 6.5. The standard deviation of 11.3. Here is the distribution as a table

1 3 4 5 6 7 8 9 10-19 20-29 30-39 40-49 50-59 60-69 70-79 90-99 100-199 200-299
976 123 410 156 149 81 66 43 213 65 29 17 8 9 7 2 7 2

or as a chart

BG

There are 589 proofs. The largest proof has 684 lines. The medium length is 27.9. The standard deviation of 55.2. Here is the distribution as a table

1 3 4 5 6 7 8 9 10-19 20-29 30-39 40-49 50-59 60-69 70-79 80-89 90-99 100-199 200-299 300-399 500-599 600-699
141 17 61 38 29 17 17 9 85 33 35 21 10 9 10 7 8 29 9 2 1 1

or as a chart

PF

There are 635 proofs. The largest proof has 1047 lines. The medium length is 22.9. The standard deviation of 64.6. Here is the distribution as a table

1 3 4 5 6 7 8 9 10-19 20-29 30-39 40-49 50-59 60-69 70-79 80-89 90-99 100-199 200-299 300-399 400-499 700-799 1000-1999
189 21 81 43 34 34 16 8 63 45 12 14 15 13 6 4 2 26 3 2 2 1 1

or as a chart

ALL

Altogether, there are 12903 proofs. The largest proof has 1047 lines. The medium length is 6.3. The standard deviation of 21.43. Here is the distribution as a table

1 2 3 4 5 6 7 8 9 10-19 20-29 30-39 40-49 50-59 60-69 70-79 80-89 90-99 100-199 200-299 300-399 400-499 500-599 600-699 700-799 1000-1999
6601 2 724 1918 915 565 386 253 159 731 228 110 69 42 41 29 14 15 76 15 4 2 1 1 1 1

or as a chart

Number of tactics per line

For each set of files, we give the number of proof lines that have a given number of tactics

SSR

Total 1 2 3 4 5 6 7
27006 13142 (49%) 9974 (37%) 3325 (12%) 512 (2%) 48 (< 1%) 4 (< 1%) 1(< 1%)

MORE

Total 1 2 3 4 5 6 7
12597 6868 (55%)) 4228 (34%) 1240 (10%) 228 (2%) 27 (< 1%) 4 (< 1%) 2 (< 1%)

BG

Total 1 2 3 4 5
15546 10816 (70%) 3763 (24%) 847 (5%) 114 (< 1%) 6 (< 1%)

PF

Total 1 2 3 4 5
13675 9659 (71%) 3358 (24%) 580 (4%) 71 (< 1%) 7 (< 1%)

ALL

Total 1 2 3 4 5 6 7
68824 40485 (59%)) 21323 (31%) 5992 (9%) 925 (1%) 88 (< 1%) 8 (< 1%) 3 (< 1%)

Branching depth

For each set of files we give the number of proof lines at a given branching depth. As in Ssreflect we use identation to indicate the branching depth, a proof with deep branching would have a proof script drifting to the right.

SSR

Level 0 Level 1 Level 2 Level 3 Level 4
20297 (76%) 5494 (20%) 910 (3 %) 103 (< 1%) 5 (< 1%)

MORE

Level 0 Level 1 Level 2 Level 3 Level 4 Level 5
7737 (63%) 3573 (29%) 830 (7%) 78 (< 1%) 8 (< 1%) 1 (< 1%)

BG

Level 0 Level 1 Level 2 Level 3 Level 4 Level 5
6361 (41%) 6438 (42%) 2207 (14%) 344 (2%) 48 (< 1%) 10 (< 1%)

PF

Level 0 Level 1 Level 2 Level 3 Level 4 Level 5
5122 (38%) 5132 (38%) 2282 (17%) 678 (5%) 168 (1%) 21 (< 1%)

ALL

Level 0 Level 1 Level 2 Level 3 Level 4 Level 5
39517 (58%) 20641 (30%) 6629 (9%) 1203 (2%) 229 (< 1%) 32 (< 1%)

Tacticals and Tactics

For each set of files we give the number of applications of some specific tacticals and tactics and their percentage with respect to the number of maximal tactics that do not contain sequences _ ; _.

SSR

Total _ ; _ _ ; [_ | _] _ ; first _ _ ; last _ _ => _ by _ rewrite _ apply: _ elim : _ admit. have : _ suff : _ have _ := _ wlog : _
45208 18378 (41%) 191 (< 1%) 1057 (2%) 868 (2%) 13085 (29%) 13852 (31%) 18989 (42%) 3060 (7%) 731 (2%) 0 (0%) 2301 (5%) 233 (< 1%) 1659 (4%) 63 (< 1%)

MORE

Total _ ; _ _ ; [_ | _] _ ; first _ _ ; last _ _ => _ by _ rewrite _ apply: _ elim : _ admit. have : _ suff : _ have _ := _ wlog : _
19795 7532 (38%) 69 (< 1%) 502 (3%) 448 (2%) 5570 (28%) 5374 (27%) 8407 (42%) 1369 (7%) 239 (1%) 0 (0%) 1178 (6%) 152 (< 1%) 988 (5%) 56 (< 1%)

BG

Total _ ; _ _ ; [_ | _] _ ; first _ _ ; last _ _ => _ by _ rewrite _ apply: _ elim : _ admit. have : _ suff : _ have _ := _ wlog : _
21238 5823 (27%) 27 (< 1%) 242 (1%) 364 (2%) 3305 (17%) 4820 (24%) 8123 (41%) 1559 (8%) 45 (< 1%) 0 (0%) 3725 (19%) 184 (1%) 3296 (17%) 58 (< 1%)

PF

Total _ ; _ _ ; [_ | _] _ ; first _ _ ; last _ _ => _ by _ rewrite _ apply: _ elim : _ admit. have : _ suff : _ have _ := _ wlog : _
18207 4759 (26%) 36 (< 1%) 230 (1%) 506 (3%) 3214 (18%) 4455 (24%) 7977 (44%) 2253 (12%) 32 (< 1%) 0 (0%) 2603 (24%) 184 (1%) 2108 (12%) 58 (< 1%)

ALL

Total _ ; _ _ ; [_ | _] _ ; first _ _ ; last _ _ => _ by _ rewrite _ apply: _ elim : _ admit. have : _ suff : _ have _ := _ wlog : _
104448 36492 (35%) 323 (< 1%) 2031 (2%) 2186 (2%) 25174 (24%) 28522 (27%) 43499 (42%) 14654 (14%) 1339 (1%) 0 (0%) 9807 (9%) 778 (< 1%) 8051 (8%) 220 (< 1%)