Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Grothendieck's utopia and genetic algorithms


view this post on Zulip 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: Mar 28 2024 at 08:18 UTC