Email Gateway (Aug 22 2022 at 18:23): Email Gateway (Aug 22 2022 at 18:23):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
If I am wrong in the following lines, please feel free to correct me, I am
far from being an expert in proof assistants (such a correction may help
other beginners having the same wrong ideas). My two arguments for the
"sorry" approach in actual research in mathematics are the following, which
seem to apply to both the human brains and the computers:
Argument 1 (The Tower of Babel): A library in which the types corresponding
to the statements of the theorems and their corollaries are assumed to be
inhabited rather than to be proved to be inhabited is more efficient from a
computational point of view, e.g., sledgehammer should work faster than in
the traditional approach because the search space is smaller. So, even if
we know the proof of a theorem, we may omit such a proof in order to
improve the computational efficiency of the proof assistant by eliminating
unnecessary lemmas.
Argument 2 (The Tortoise and the Hare): Informal mathematics develops
faster than formal mathematics for the same obvious reasons that it falls
apart easier. So, to do research in contemporary mathematics,
non-controversial theorems should be assumed to be true in a proof
assistant, as most mathematicians do in their brain. Few creative
contemporary mathematicians really know all the proofs of the theorems that
they used in their research, because mathematics developed in an
exponential way.
Angeliki's above-mentioned observation applies to Argument 2. Nevertheless,
using the "sorry" approach, the discussion will be no longer about validity
of logical reasoning, but about the translations from ZFC to simple type
theory. This last subject does not belong to the foundations of the
particular branch of mathematics where we are proving the theorem, e.g.,
modular forms, but to type theory and formal logic. Furthermore, it is
easier to do experiments changing the statements in Isabelle than in a
paper, because the paper does not change color after a mistake is found.
A proof assistant, with a library of types corresponding to contemporary
theorems written in Isabelle assumed to be inhabited by "sorrry" will be a
useful tool to do informal mathematics and such a practical solution should
not be confused with the systematic project of formally verifying all
mathematics. I do not say that to implement such a library of statements
without proofs is easy, but it is the only way to reach the hare.
Kind Regards,
Jose M.
Email Gateway (Aug 22 2022 at 18:23):From: Freek Wiedijk <freek@cs.ru.nl>
Dear José,
Isn't the "formal math through sorry" thing you're
proposing very close to what will be given by Tom Hales'
formal abstracts project? So isn't this happening already
in some small way?
Freek
Last updated: Apr 19 2024 at 16:20 UTC