*To*: Johannes Waldmann <johannes.waldmann at htwk-leipzig.de>*Subject*: Re: [isabelle] New in the AFP: Intersecting Chords Theorem*From*: Lukas Bulwahn <lukas.bulwahn at gmail.com>*Date*: Thu, 13 Oct 2016 19:45:26 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <a698e11d-80b4-82c8-04cf-149399376cc5@htwk-leipzig.de>*References*: <a698e11d-80b4-82c8-04cf-149399376cc5@htwk-leipzig.de>

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

**References**:**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Johannes Waldmann

- Previous by Date: Re: [isabelle] finishing a proof
- Next by Date: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Previous by Thread: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Next by Thread: [isabelle] TABLEAUX 2017 - First Call for Papers
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list