[isabelle] on the importance of libraries related to the ABC conjecture

[José Manuel Rodriguez Caballero]

Libraries related to the subject of the ABC conjecture will be
indispensable for the development of contemporary mathematics, because of
the complexity of the candidates for new proofs. Indeed, I read in a recent
article:

Two mathematicians [Peter Scholze and Jakob Stix] have found what they say

is a hole at the heart of a proof that has convulsed the

mathematics community for nearly six years [...] Shinichi Mochizuki

maintains that his proof is not flawed despite the assertions of Jakob Stix
and Peter Scholze that they’ve discovered a “serious, unfixable gap.”

Reference (Titans of Mathematics Clash Over Epic Proof of ABC Conjecture,
by Klaus Kremmerz, Quanta Magazine):
https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/

Kind Regards,
Jose M.

[Tobias Nipkow]

Back in December 2017, Peter Scholze (for the first time, I believe) publicly
pinpoints what he believes is a flaw in Mochizuki's proof. He concludes with
this remark:

"One final point: I get very annoyed by all references to computer-verification
(that came up not on this blog, but elsewhere on the internet in discussions of
Mochizuki’s work). The computer will not be able to make sense of this step
either. The comparison to the Kepler conjecture, say, is entirely misguided: In
that case, the general strategy was clear, but it was unclear whether every
single case had been taken care of. Here, there is no case at all, just the
claim “And now the result follows”."

https://galoisrepresentations.wordpress.com/2017/12/17/the-abc-conjecture-has-still-not-been-proved/?psincomments#comment-4619

Tobias

Post by José Manuel Rodriguez Caballero
Libraries related to the subject of the ABC conjecture will be
indispensable for the development of contemporary mathematics, because of
the complexity of the candidates for new proofs. Indeed, I read in a recent
Two mathematicians [Peter Scholze and Jakob Stix] have found what they say

is a hole at the heart of a proof that has convulsed the

mathematics community for nearly six years [...] Shinichi Mochizuki

maintains that his proof is not flawed despite the assertions of Jakob Stix
and Peter Scholze that they’ve discovered a “serious, unfixable gap.”

Reference (Titans of Mathematics Clash Over Epic Proof of ABC Conjecture,
https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/
Kind Regards,
Jose M.

[José Manuel Rodriguez Caballero]

Post by Tobias Nipkow
Back in December 2017, Peter Scholze (for the first time, I believe)
publicly
pinpoints what he believes is a flaw in Mochizuki's proof. He concludes
with
"One final point: I get very annoyed by all references to
computer-verification
(that came up not on this blog, but elsewhere on the internet in
discussions of
Mochizuki’s work). The computer will not be able to make sense of this
step
either. The comparison to the Kepler conjecture, say, is entirely
misguided: In
that case, the general strategy was clear, but it was unclear whether
every
single case had been taken care of. Here, there is no case at all, just
the
claim “And now the result follows”."

Scholze's claim

"I get very annoyed by all references to computer-verification [...] The
computer will not be able to make sense of this step either"

is not the conclusion of a long theoretical research about proof-assistants
(this is not his field), but just a personal prejudice against
computer-verified mathematics. Of course, the computer will not make sense
of a mistake, making sense of a mistake is a subjective feeling. Indeed,
Voevodsky said:

"Each time when I feel myself drifting away thinking about why it is so, I
stop myself, why I not actually check what is actually true and what is
not"

Reference to Voevodsky's quotation, min 18 in the lecture:
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_4.mp4

What the computer will do is to show the first line where the mistake
occurs and that is an objective fact. Without proof assistants, the
ultimately reference for truth in mathematics is authority and I am skeptic
of scientific authority since I read the following quotation from Lord
Kelvin (who was President of the Royal Society of England): Heavier than
air flying machines are impossible. Reference to the quotation:
https://www.nasa.gov/audience/formedia/speeches/fg_kitty_hawk_12.17.03.html

Kind Regards,
Jose M.

[Tobias Nipkow]

Peter Scholze is simply very realistic wrt the pitiful state of today's proof
assitants in the face of a proof like Mochizuki's. Anybody who thinks that we
could have contributed one iota to spotting the mistake (or providing the proof,
in case there is no mistake), lives in dreamland.

Tobias

Post by José Manuel Rodriguez Caballero

Post by Tobias Nipkow
Back in December 2017, Peter Scholze (for the first time, I believe)
publicly
pinpoints what he believes is a flaw in Mochizuki's proof. He concludes
with
"One final point: I get very annoyed by all references to
computer-verification
(that came up not on this blog, but elsewhere on the internet in
discussions of
Mochizuki’s work). The computer will not be able to make sense of this
step
either. The comparison to the Kepler conjecture, say, is entirely
misguided: In
that case, the general strategy was clear, but it was unclear whether
every
single case had been taken care of. Here, there is no case at all, just
the
claim “And now the result follows”."

Scholze's claim
"I get very annoyed by all references to computer-verification [...] The
computer will not be able to make sense of this step either"
is not the conclusion of a long theoretical research about proof-assistants
(this is not his field), but just a personal prejudice against
computer-verified mathematics. Of course, the computer will not make sense
of a mistake, making sense of a mistake is a subjective feeling. Indeed,
"Each time when I feel myself drifting away thinking about why it is so, I
stop myself, why I not actually check what is actually true and what is
not"
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_4.mp4
What the computer will do is to show the first line where the mistake
occurs and that is an objective fact. Without proof assistants, the
ultimately reference for truth in mathematics is authority and I am skeptic
of scientific authority since I read the following quotation from Lord
Kelvin (who was President of the Royal Society of England): Heavier than
https://www.nasa.gov/audience/formedia/speeches/fg_kitty_hawk_12.17.03.html
Kind Regards,
Jose M.

[Ching-Tsun Chou]

You may find this article interesting:

https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/

Post by Tobias Nipkow
Peter Scholze is simply very realistic wrt the pitiful state of today's proof
assitants in the face of a proof like Mochizuki's. Anybody who thinks that we
could have contributed one iota to spotting the mistake (or providing the proof,
in case there is no mistake), lives in dreamland.
Tobias

Post by José Manuel Rodriguez Caballero

Post by Tobias Nipkow
Back in December 2017, Peter Scholze (for the first time, I believe)
publicly
pinpoints what he believes is a flaw in Mochizuki's proof. He concludes
with
"One final point: I get very annoyed by all references to
computer-verification
(that came up not on this blog, but elsewhere on the internet in
discussions of
Mochizuki’s work). The computer will not be able to make sense of this
step
either. The comparison to the Kepler conjecture, say, is entirely
misguided: In
that case, the general strategy was clear, but it was unclear whether
every
single case had been taken care of. Here, there is no case at all, just
the
claim “And now the result follows”."

Scholze's claim
"I get very annoyed by all references to computer-verification [...] The
computer will not be able to make sense of this step either"
is not the conclusion of a long theoretical research about

proof-assistants

Post by José Manuel Rodriguez Caballero
(this is not his field), but just a personal prejudice against
computer-verified mathematics. Of course, the computer will not make

sense

Post by José Manuel Rodriguez Caballero
of a mistake, making sense of a mistake is a subjective feeling. Indeed,
"Each time when I feel myself drifting away thinking about why it is so,

I

Post by José Manuel Rodriguez Caballero
stop myself, why I not actually check what is actually true and what is
not"

https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_4.mp4

Post by José Manuel Rodriguez Caballero
What the computer will do is to show the first line where the mistake
occurs and that is an objective fact. Without proof assistants, the
ultimately reference for truth in mathematics is authority and I am

skeptic

Post by José Manuel Rodriguez Caballero
of scientific authority since I read the following quotation from Lord
Kelvin (who was President of the Royal Society of England): Heavier than

https://www.nasa.gov/audience/formedia/speeches/fg_kitty_hawk_12.17.03.html

Post by José Manuel Rodriguez Caballero
Kind Regards,
Jose M.

[José Manuel Rodriguez Caballero]

Post by Tobias Nipkow
Peter Scholze is simply very realistic wrt the pitiful state of today's proof
assitants in the face of a proof like Mochizuki's. Anybody who thinks that we
could have contributed one iota to spotting the mistake (or providing the proof,
in case there is no mistake), lives in dreamland.
Tobias

Scholze’s claim gives rise to the following interesting question (I am open-minded for the three possible answers):
Is the main obstacle of today proof assistants a technological problem of the software itself, a theoretical problem related to the type theory or a lack of libraries related to this subject?

In the case of Isabelle/HOL I guess that it is the third option, although I am not an expert in the subject and I may change my opinion after learning more about it.

Kind Regards,
José M.

[Manuel Eberl]

I would like to counteract the negativity in this thread a little bit by
interjecting that theorem provers in general and Isabelle in particular
/have/ been used successfully for research mathematics, big and small.
And problems in proofs (even published and peer-reviewed ones!) have
been found in the process.

Of course, these were mostly cases where the proofs in question were
fairly straightforward to formalise and did not require too much
"non-basic" material. For instance, my BSc thesis in mathematics – which
was a formalisation of a recent small result in social choice theory –
is, of course, in no way comparable to the ABC conjecture, but it is
research mathematics nonetheless, and so I do think the situation is not
quite as hopeless as this thread may suggest.

With the ABC conjecture and things like that, I think the main problem
is, as you also suspected, the lack of "libraries". Most modern
mathematics (especially the really big results like the ABC conjecture
or Fermat's Last Theorem) build on a huge tower of other mathematics. As
a "pen-and-paper" mathematician, you can basically use any theory
developed by another person as long as it's published and not obviously
wrong. You don't have to fully understand their proof, you can just use
the result.

When you want to do the same thing In a theorem prover, in all
likelihood, you will have to formalise the entire thing yourself. And
everything it depends on. And so on. That, I think, is the biggest
problem about what makes formalising "real" modern mathematics so
difficult. Another thing is that once you formalise something, you have
to make lots of technical decisions about how to formulate it precisely
and they can all come back at you and make your life difficult. In
pen-and-paper mathematics, it is easier to argue such technical issues
away informally and focus on the essence of the proof, trusting that the
reader will still know what you mean.

Another problem (especially in the long run) is that, for the most part,
there is only one mathematics, but there are many different theorem
provers and you cannot easily exchange results between them.

In any case, something as massive as the ABC conjecture proof will
present a formidable challenge to anyone who wants to even begin to
understand it. I would guess that even writing things out on paper in
Bourbakian rigour is probably almost impossible, and that is before any
theorem-proving software even gets involved.

Manuel

Post by José Manuel Rodriguez Caballero

Post by Tobias Nipkow
Peter Scholze is simply very realistic wrt the pitiful state of today's proof
assitants in the face of a proof like Mochizuki's. Anybody who thinks that we
could have contributed one iota to spotting the mistake (or providing the proof,
in case there is no mistake), lives in dreamland.
Tobias

Is the main obstacle of today proof assistants a technological problem of the software itself, a theoretical problem related to the type theory or a lack of libraries related to this subject?
In the case of Isabelle/HOL I guess that it is the third option, although I am not an expert in the subject and I may change my opinion after learning more about it.
Kind Regards,
José M.

[Eugene W. Stark]

Mathematics is the one area of human endeavor in which the concept of an
absolute truth potentially has some meaning. Whether or not a mathematical
result is accepted as true ought not to be dependent on a clash of egos,
personalities, and reputations. It should be the responsibility of the
proposer of a theorem to address all reasonable challenges to its veracity,
not to simply argue by blatant assertion that it is fact and that those who
say otherwise have simply not managed to think deeply enough about it to see
the light. Formally checkable proofs and proof assistants hold the promise
of finally expurgating the social dynamic from mathematical truth; thereby
clearly illuminating the distinction between mathematics and the "subjective"
sciences.

[José Manuel Rodriguez Caballero]

Manuel wrote:
“As
a "pen-and-paper" mathematician, you can basically use any theory
developed by another person as long as it's published and not obviously
wrong. You don't have to fully understand their proof, you can just use
the result”

Post by José Manuel Rodriguez Caballero
"I get very annoyed by all references to computer-verification [...] The
computer will not be able to make sense of this step either"

I guess that, following the “sorry” approach, this controversy could be ended in one year, rather than the 6 years and even today we do not know the answer.

Kind Regards,
José M.

[Manuel Eberl]

I guess it's not quite that easy. It's not just the proofs, one also has
to state these theorems formally (and be extremely certain about getting
that right when a 'sorry' is involved), and one needs to define all the
required constants and concepts. That alone can be an immense amount of
work.

And even then, the ‘new’ material with this particular proof is so
immense that it is probably almost infeasible. Even if one were to find
a problem with the proof, it would then be quite unclear whether it is
an issue of the original proof or one of the formalisation, i.e. if the
person formalising it just misunderstood something.

In any case I think w.r.t. the ABC conjecture, Scholze is certainly
correct in saying that computer verification is the wrong thing to look
at at the moment. I interpret what he said as saying that no one could
possibly formalise a proof that they don't understand even informally,
and that seems to be the case with the ABC conjecture at the moment.
Mathematicians looked at it and found a step that they don't understand,
and until that is resolved and every step of the proof is
well-understood, computer verification makes no sense at all.

Of course, even when all of that is resolved, it still seems that a
verification is completely feasible simply because there is so much
material.

I guess that, following the “sorry” approach, this controversy could be ended in one year, rather than the 6 years and even today we do not know the answer.

I doubt that. I highly doubt that, even with this approach, a
formalisation of any proof of that size is feasible within a year.
Perhaps you think one should tackle this particularly controversial
aspect alone and ‘sorry’ everything before it?

Well, as I said above, if a problem /is/ found, the controversy will
then be whether it's a genuine problem or whether it can be fixed
somehow. Or if perhaps there is some mistake in the formalisation to
begin with. And if no problem is found, one will have to worry about
whether the statement that was proven is really what is required: Are
all the involved definitions correct? Are the assumptions perhaps
vacuous due to some mistake in how they were written down? And even
then, one still relies on a huge tower of sorries in front of it.

Manuel

[Dr A. Koutsoukou-Argyraki]

just adding two points supporting what Manuel just wrote:

1) In praxis, it is very easy to end up proving something wrong with a
proof assistant by assuming a false statement. One can convince
themselves of this by making up any trivial example. Now imagine how
dangerous this becomes in a much more sophisticated setting where
a very subtle mistake can go unnoticed and lead one to assume a false
statement.
That is to say, a proof assistant is not completely immune to errors by
"human" mathematicians and one should be extremely responsible and
careful with assumptions -even more so in the "sorrys" approach that
José suggests. Regarding the ABC conjecture, the level of difficulty is
such that the risk increases a lot.

2) When a step in a proof is unclear from the point of view of informal
mathematics, as is the case for the suggested proof of the ABC
conjecture, a proof assistant will not always
give a definitive answer, i.e. : If it happens that a counterexample
is found,
the step (and thus the proof) is of course wrong. If no counterexample
is found, nor a proof is given by automation, the step may or may not be
wrong.
And we cannot expect that a formal proof can necessarily be discovered
where an informal one is missing.

Best,
Angeliki

Post by Manuel Eberl

So, assuming some non-controversial theorems as true, using the key
word “sorry”, Isabelle could be used in order to do research in any
branch of mathematics. Sincerely, I do not see any other obstacle in

I guess it's not quite that easy. It's not just the proofs, one also has
to state these theorems formally (and be extremely certain about getting
that right when a 'sorry' is involved), and one needs to define all the
required constants and concepts. That alone can be an immense amount of
work.
And even then, the ‘new’ material with this particular proof is so
immense that it is probably almost infeasible. Even if one were to find
a problem with the proof, it would then be quite unclear whether it is
an issue of the original proof or one of the formalisation, i.e. if the
person formalising it just misunderstood something.
In any case I think w.r.t. the ABC conjecture, Scholze is certainly
correct in saying that computer verification is the wrong thing to look
at at the moment. I interpret what he said as saying that no one could
possibly formalise a proof that they don't understand even informally,
and that seems to be the case with the ABC conjecture at the moment.
Mathematicians looked at it and found a step that they don't
understand,
and until that is resolved and every step of the proof is
well-understood, computer verification makes no sense at all.
Of course, even when all of that is resolved, it still seems that a
verification is completely feasible simply because there is so much
material.

I guess that, following the “sorry” approach, this controversy could
be ended in one year, rather than the 6 years and even today we do not
know the answer.

I doubt that. I highly doubt that, even with this approach, a
formalisation of any proof of that size is feasible within a year.
Perhaps you think one should tackle this particularly controversial
aspect alone and ‘sorry’ everything before it?
Well, as I said above, if a problem /is/ found, the controversy will
then be whether it's a genuine problem or whether it can be fixed
somehow. Or if perhaps there is some mistake in the formalisation to
begin with. And if no problem is found, one will have to worry about
whether the statement that was proven is really what is required: Are
all the involved definitions correct? Are the assumptions perhaps
vacuous due to some mistake in how they were written down? And even
then, one still relies on a huge tower of sorries in front of it.
Manuel