Re: [isabelle] New in the AFP: Intersecting Chords Theorem



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.