Dear Johannes,

to large parts I agree with Manuel's opinion, but nevertheless here

are some thoughts from my side:

as author of the AFP entry "Intersecting Chords Theorem" and some

other entries on the Top 100, I can give a little personal insight

about the reasons that some theorems are formalized and some are not.

Please remember that this is really a very subjective personal

opinion.

First of all, already Freek Wiedijk, who maintains the recordings of

the formalized Top 100 Theorems list, noted that the list is actually

quite arbitrary and does not really provide a proper measure of the

state of formalizations in the different theorem provers. So, this

list is actually really more `for the fun of it` than a proper

measurement of contributions.

This brings me directly to the reason for my contributions. I enjoy

using Isabelle to challenge my brain with logical puzzles and there

are still some theorems in the Top 100 theorems list that are just in

reach with a few free-time sessions. Although the list is largely

arbitrary as proper measure, the theorems actually point to historical

interesting and sometimes surprising discoveries, and while

researching and formalizing those you often also learn a bit on the

history of mathematics.

Another reason that some theorems on the list have lately been

formalized is that some of them are just challenging enough to give as

final challenge to students after an introductory course on Isabelle.

But also, many proved theorems on the list are more or less basics

that are today available in all larger formalized mathematical

collections of theorem provers.

To your remark that some of the open proofs could be proved

automatically with the right automation points actually in an

interesting direction that Amine Chaieb suggested a few years ago:

Whereas it is more or less obvious that these historic proofs can be

formalized by humans later on with some effort, the real challenge

(and measure of research progress) is to provide automation on whole

theories that make it possible that these facts can today be proved by

automatic methods without any further human interaction. So, we should

not measure which have been formalized, but instead which can be

proved automatic from some base theory and powerful automation. But

improving on this measure takes wise guidance and some work from PhD

students to be completed.

Now, here are the reasons why some theorems are not formalized:

Most of the theorems have an historic importance, but no one would

today expect these historic proofs to be possibly flawed or consider

some specific proof step difficult to argue. Some past research

projects on formalizing mathematics, such as the formalization of the

four-color-theorem and the proof of Kepler's conjecture, focussed on

increasing the confidence of proofs that could be possibly flawed. For

example, the two mentioned proofs had specific proof steps that were

impossible to validate or verify by sheer human reasoning capacity.

Other research activities focus on formalizing mathematics, so that

certain classes of computer programs or systems can be verified. So

these formalizations are driven by mathematic fields which are applied

in systems that must be dependable (i.e., safe, secure, reliable,

available...). However, these substantial research contributions do

not necessarily come across the very specific theorems on the Top 100

list.

Lukas