[FOM] Proof assistants and conjectures

[Vaughan Pratt]

Roger Bishop Jones wrote:
> There is a list of "The Hundred greatest theorems" at:
> http://personal.stevens.edu/~nkahl/Top100Theorems.html

Taking this list at face value (how come that remarkable and 
fundamentally useful theorem, that every vector space is free, is bumped 
in favor of the birthday problem, Cramer's rule, the Buffon needle 
problem, etc?), and assigning half a dozen of the undated candidates at 
least to centuries, leaving about 10 unassigned, the following table 
bins the remaining 90 theorems by century.

BC
18th 1
5th  2
4th  1
3rd  10

AD
1st  1
2nd  1
14th 2
16th 3
17th 9
18th 17
19th 32
20th 11

Despite a growing population of research mathematicians, the 20th 
century has barely stayed ahead of the 17th, and even more narrowly just 
edged out the third century B.C.

The question then arises, how will our descendants a century hence view 
the 20th century?  Will they continue to assess the 19th century as the 
peak of mathematical discovery, much like that century's great gold 
rushes, or will the standards have changed by then to acknowledge a 
great many contributions of the 20th century whose greatness we have 
simply been unable to see at such close range?

It may be just a brand recognition issue.  The apparent productivity of 
19th century mathematics might have more to do with how the 20th century 
has marketed the 19th than with which century has advanced the subject 
further.

Vaughan Pratt