THEOREMS TOP 50

End of 2002
(i)
(ii)
(iii)
1.
 AXIOMS:22
8042
2.0266%
2.
 TARSKI:def 1
6547
1.6499%
3.
 XBOOLE_0:def 3
5523
1.3918%
4.
 FUNCT_1:def 5
4676
1.1784%
5.
 NAT_1:38
4659
1.1741%
6.
 XBOOLE_0:def 2
4345
1.0950%
7.
 FUNCT_2:def 1
3811
0.9604%
8.
 FINSEQ_1:def 3
3525
0.8883%
9.
 XBOOLE_1:1
3325
0.8379%
10.
 AXIOMS:13
3108
0.7832%
11.
 FINSEQ_3:27
2610
0.6577%
12.
 STRUCT_0:def 2
2449
0.6172%
13.
 XBOOLE_0:def 4
2279
0.5743%
14.
 REAL_1:def 5
2171
0.5471%
15.
 TARSKI:def 2
1992
0.5020%
16.
 FINSEQ_4:def 4
1955
0.4927%
17.
 FINSEQ_1:3
1947
0.4907%
18.
 REAL_1:30
1842
0.4642%
19.
 TARSKI:def 4
1840
0.4637%
20.
 NAT_1:29
1787
0.4503%
21.
 STRUCT_0:def 3
1728
0.4355%
22.
 SQUARE_1:6
1681
0.4236%
23.
 TARSKI:def 3
1637
0.4125%
24.
 AXIOMS:21
1624
0.4093%
25.
 PBOOLE:def 3
1548
0.3901%
26.
 ZFMISC_1:106
1547
0.3899%
27.
 XBOOLE_0:def 10
1498
0.3775%
28.
 EUCLID:56
1355
0.3415%
29.
 FUNCT_1:72
1318
0.3321%
 REAL_1:def 3
1318
0.3321%
31.
 AXIOMS:24
1312
0.3306%
32.
 AXIOMS:18
1307
0.3294%
33.
 BINOP_1:def 1
1297
0.3269%
34.
 AXIOMS:16
1281
0.3228%
35.
 PRE_TOPC:12
1233
0.3107%
36.
 REAL_1:53
1199
0.3022%
37.
 XBOOLE_0:3
1175
0.2961%
38.
 XBOOLE_0:def 7
1150
0.2898%
39.
 MCART_1:7
1075
0.2709%
40.
 AMI_1:def 15
1068
0.2691%
 REAL_1:55
1068
0.2691%
42.
 GRFUNC_1:8
1016
0.2560%
43.
 AMI_1:def 19
1011
0.2548%
44.
 FUNCT_1:9
1006
0.2535%
45.
 REAL_1:49
989
0.2492%
46.
 FUNCT_4:42
962
0.2424%
 REAL_1:84
962
0.2424%
48.
 FUNCT_1:23
937
0.2361%
49.
 NAT_1:18
929
0.2341%
50.
 ZFMISC_1:33
924
0.2329%
Explanations:
    (i) - Number of theorem and its ranking.
   (ii) - Number of references.
  (iii) - Percentage of all references.
Previous year