Some statistics

The project started in 1996. The compendium contains 334 pages and the theory formalized by the end of February 2000 covers about 180 pages of it (about 54% without taking into account the articles currently under development).

The following summarizes the number of articles from this project submitted to MML:

year	1996	1997	1998	1999	2000	1996-2000
YELLOW	8	1	5	3	0	17
WAYBEL	10	6	8	4	4	32
All	18	7	13	7	4	49
Y$\div$All %	44%	14%	38%	42%	0%	35%

The last line gives percentage of YELLOW series. This percentage is less than we expected.

	MML	WAYBEL	YELLOW	W&Y	Percentage
Articles	633	32	17	49	7.74%
Theorems	29,514	1,391	834	2225	7.54%
ave per art	46.6	43.5	49.1	45.4	-
Definitions	5,389	246	105	351	6.51%
ave per art	8.5	7.7	6.2	7.2	-
Size (kB)	46,966	2,867	1,273	4,140	8.82%
ave per art	74.2	89.6	74.9	84.5	-

The last column gives percentage of this project in the entire MML. Average numbers of theorems, definitions, and kilobytes show that the project is 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 project and the rest of the MML may be measured by the number of references between them. Each reference to the theorem coming from another article is called an external reference.

External references	Count	Percentage
All	317427	100.00%
All to Y&W	11677	3.68%
Outside of Y&W to Y&W	349	0.11%
In Y&W	26747	100.00%
In Y&W to Y&W	11328	42.35%

57.65% of all external references from the YELLOW and WAYBEL articles is to the rest of the MML. This indicates that the MML contained a substantial quantity of definitions and facts needed for our project.

There is, unfortunatly, no statistics concerning the quantity of work needed to formalize this material. However, we may state that it vary on authors and WAYBEL series needed much more work per line than YELLOW series.