Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Grothendieck's utopia was to have a mathematical system where the proof of
each theorem will be trivial. This is extremely hard to by hand.
Nevertheless, if we consider a population of theorems (with their own
proofs) and we assume that Theorem X eats Theorem Y if Theorem Y can be
obtained from theorem X in a trivial way (sledgehammer [timeout = 2000])
then, after a large battler, only the more general theorems will survive
and the theory will be a set of trivial consequences of these theorems.
Then the theory can be automatically reconstructed in such a way that the
proof of each theorem will be a trivial consequence of the set of more
general theorems (maybe there will be some non-trivial interdependence
among the more general theorems). I think that such a process can be
improved adding mutations and other features from genetic algorithms.
I do not know if such a Grothendieckization of Isabelle will have some
practical advantage.
Kind Regards,
Jose M.
Last updated: Nov 21 2024 at 12:39 UTC