Email Gateway (Aug 22 2022 at 18:40): Email Gateway (Aug 22 2022 at 18:40):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
Just a reflexion about the interface in Isabelle. I think that there are
two to ways to prove a theorem in Isabelle:
(a) To copy the proof from a textbook (or a paper) in a linear way, i.e.,
to implement lemma by lemma in the same order as they appear in a textbook.
(b) To write the statement of the theorem. To prove it using some lemmas,
assumed to be true by means of "sorry", guaranteeing that the complexity of
each lemma is strictly inferior to the complexity of the target theorem
(this is the art of doing mathematics). To repeat the same procedure to
each lemma.
In my case, I prefer the approach (b), because one of my goals is to prove
the theorems for myself as a personal challenge, without regarding
textbooks. This is also the approach of every mathematician for doing
research. So, it would be nice to navigate the thy-file as an oriented
forest (in a graph theoretical sense): there is an arrow from lemma A to
lemma B if lemma A is used in the proof of lemma B. I guess that such a
forest is in the mind of any creative mathematician, because linear
thinking like in (a) seems to be artificial in order to make a scientific
discovery.
Reference to graph-theoretic forests:
http://mathworld.wolfram.com/Forest.html
Kind Regards,
José M.
Last updated: Apr 26 2024 at 04:17 UTC