Some other statistics

The CCL project started in 1996. The CCL-book contains 334 pages divided into 8 chapters covering a total of 715 items. Of these, 254 items are examples and exercises which we did not plan to cover. By the end of April 2002, the formalization covered 231 items which is slightly more than 50% of the work originally planned. (A caveat is in place: items differ substantially in their weights and many of the remaining items seem to be more difficult to formalize as their proofs are diagram based.)

Table IV: CCL articles over the years

year	1996	1997	1998	1999	2000	2001	Total
YELLOW	8	1	5	3	1	4	22
WAYBEL	10	6	8	4	5	2	35
All	18	7	13	7	6	6	57

Table V: Some article statistics

	MML	WAYBEL	YELLOW	W and Y	Percentage
Articles	717	35	22	57	7.95%
Theorems	31,741	1,512	1,018	2,530	7.97%
Average	44.3	43.2	46.3	44.4
Min	0	18	14	14
Median	37	41	49	43
Max	194	90	72	90
Definitions	6,093	271	138	409	6.7%
Average	8.5	7.7	6.3	7.2
Min	0	0	0	0
Median	6	5	5	5
Max	49	40	26	40
Tokens (,000)	16,219	787	471	1259	7.76%
Average	22,589	22,498	21,431	22,086
Min	50	10699	8,762	8,762
Median	18,704	22,045	17,622	20,591
Max	248,314	33,217	55,567	55,567
Size (kB)	52,184	3,027	1,671	4,699	9%
Average	72.8	86.5	75.9	82.4
Min	0.9	41.1	29.9	29.9
Median	62.2	86.5	66.9	77.4
Max	640.0	121.4	166.3	166.3

Table VI: External references

External references	Count	Avg	Min	Med	Max	% MML	% W&Y
		over relevant articles
MML	371,795	518.5	0	392	6,024	100.00
MML to W&Y	13,168	18.4	0	0	1,017	3.54
Out W&Y to W&Y	859	1.3	0	0	149	0.23
Out W&Y to out W&Y	340,791	516.4	0	380	6,024	91.66
W&Y to MML	30,145	528.9	143	476	2,076	8.11	100
W&Y to W&Y	12,309	215.9	0	201	1,017	3.31	40.83
W&Y to out W&Y	17,836	312.9	39	266	1,059	4.80	59.17

Table  summarizes the number of articles submitted to MML from this project. The YELLOW series constitutes 38.6% of the articles, much less than originally anticipated. However, this may change in the near future as we are approaching the part of the CCL-book which is poorly covered in MML.

Table  presents the size of the project in terms of theorems, definitions, and sheer bytes. The last column is the percentage of this project's contribution to the entire MML. Average numbers of theorems, definitions, tokens, and kilobytes show that articles in the project are close to the MML average. Note the smaller average number of definitions which may indicate that the theory is explored more intensively.

The interaction between the CCL project and the rest of the MML, may be measured by the number of references between the project articles and other MML articles as presented in Table . The percentage of all external references from the YELLOW and WAYBEL articles to the rest of MML is 59.17%. This indicates that MML contained a substantial quantity of definitions and facts needed for our project.