Email Gateway (Aug 22 2022 at 18:38): Email Gateway (Aug 22 2022 at 18:38):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Dear Freek, as I already pointed out, I am just a beginner in the world of
proof assistants. So, I cannot give official references to the state of art
of the ideas in this field, just because of lack of knowledge (maybe in the
future that will be possible). I did not study Tom Hales' work, although I
know that he contributed to the proof of Kepler's conjecture. When I
propose some idea to other peoples, it is because I hope that other people,
with more experience than myself, will develop it: it is like to deliver a
baby to an orphanage. If Tom Hales' had the idea first, good for him,
less responsability for myself.
In my own mathematical research I do not use the "sorry" approach, because
everything that I need was already implemented in Isabelle/HOL. Indeed, in
my last publication in Journal of Number Theory (Elsevier)
https://authors.elsevier.com/a/1XqPC,WUAvIul
I just used elementary mathematics and even a good high school student can
understand my result and its proof (maybe someday this theorem will be
proposed as an exercise for an Olympiad of Mathematics at high school
level). In my paper, there are some theorems which are assumed to be true
without providing the details (it is the informal equivalent of "sorry"),
e.g., in Corollary 7 I wrote "it follows in a straight-forward way that".
After the publication of the paper, I filled the gap in Corollary 7 using
Isabelle without "sorry":
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/blob/master/PeriPythTriang.thy
Nevertheless, other mathematicians, working in new branches of mathematics,
may lack libraries.
Kind Regards,
José M.
Last updated: Nov 21 2024 at 12:39 UTC