Email Gateway (Aug 22 2022 at 14:14): Email Gateway (Aug 22 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
We now have a small but elegant entry from Lukas Bulwahn:
This entry provides a geometric proof of the intersecting chords theorem. The theorem states that when two chords intersect each other inside a circle, the products of their segments are equal. After a short review of existing proofs in the literature, I decided to use a proof approach that employs reasoning about lengths of line segments, the orthogonality of two lines and the Pythagoras Law. Hence, one can understand the formalized proof easily with the knowledge of a few general geometric facts that are commonly taught in high-school. This theorem is the 55th theorem of the Top 100 Theorems list.
https://www.isa-afp.org/entries/Chord_Segments.shtml
Many thanks, and keep them coming! Incidentally, we are also getting entries to the Development branch of the AFP. These can take advantage of the latest development version of Isabelle but unfortunately will not become visible on the AFP website until after the next release. That is expected by the end of 2016.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:15):From: Johannes Waldmann <johannes.waldmann@htwk-leipzig.de>
... the intersecting chords theorem.
Yes, geometry is nice.
This theorem is the 55th theorem of the Top 100 Theorems list.
So - what Isabelle formulations are missing - and why?
Ok, I can compute the diff of http://www.cs.ru.nl/~freek/100/
and http://www.cse.unsw.edu.au/~kleing/top100/
but I'd be interested to know about the "why".
Is it mostly "too easy" or "too tedious" -
or is there something else, like "fundamentally hard"?
The lowest-numbered items where Isabelle is missing,
but other systems have a formalisation, are
13 : Polyhedron Formula
28 : Pascal's Hexagon Theorem
29 : Feuerbach's Theorem
I'm pretty sure 28 and 29 (and 61 - Ceva, 84 - Morley, 87 - Desargues)
can be proved automatically using computer algebra (with Gröbner bases)
(cf. http://dx.doi.org/10.1016/S0747-7171(86)80006-2 )
Of course, Isabelle is not a computer algebra system.
But you have https://www.isa-afp.org/entries/Groebner_Bases.shtml
so something could be done here. Well, I guess it's "why bother".
Email Gateway (Aug 22 2022 at 14:15):From: Manuel Eberl <eberlm@in.tum.de>
As someone who has done quite a few of the Top 100 theorems in Isabelle,
I would say that the remaining ones fall mostly into three categories:
or some linear combination thereof. I for one know very little about all
these geometric problems and have never really felt the appeal of
formalising them in Isabelle.
Still, there has been a pretty continuous trickle of problems of this
list being done in Isabelle in the past few years, and I am fairly
confident that this will continue.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:15):From: Manuel Eberl <eberlm@in.tum.de>
I should probably add: there are also some problems (like "e is
transcendental", "π is transcendental") that are perfectly within reach
for a small side project for someone. The main reason why I haven't
attacked them yet is that the proofs for those are a bit ‘ad-hoc’. There
are much stronger results like the very nice Lindemann–Weierstraß
theorem, which I'd very much like to see in Isabelle, but that is a bit
more tricky to prove and I haven't found a nicely written-up version of
it so far.
As for the Gröbner bases, I know very little about these things. We have
some ML code doing something with Gröbner basis, and we have the
theoretical formalisation of them by Alexander Maletzky in the AFP. I
don't know what would be required to use either of these to prove
theorems like the ones you mentioned – that certainly sounds like an
interesting idea though. Maybe one of our Gröbner basis experts could
comment on this?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:16):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
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
Email Gateway (Aug 22 2022 at 14:16):From: Tobias Nipkow <nipkow@in.tum.de>
All of the ones that Johannes says can be proved by Gröbner bases have been
proved in HOL Light, which has well-developed Gröbner basis algorithms. It would
be interesting to see if the proofs make use of them.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:16):From: Lawrence Paulson <lp15@cam.ac.uk>
I haven’t come across any. The most distinctive feature of HOL Light is its suite of “without loss of generality” tactics, which however seldom seem to lead to shorter or more readable proofs.
Larry
Last updated: Apr 20 2024 at 04:19 UTC