Two paragraphs that highlight the potential source of the problem in the sublinked article:
> Despite mathematics being a universal language, culture clash could be getting in the way, says Kim. “In Japan people are pretty used to long, technical discussions by the lecturer that require a lot of concentration,” he says. “In America or England we expect much more interaction, pointed questions coming from the audience, at least some level of heated debate.”
> There is a growing consensus that Mochizuki has over-engineered his work, contributing to the confusion. “Most of the large theories that he builds are not essential. He could have written things in a much more streamlined way,” says Voloch.
This is a problem in a lot of technical fields but also in writing in general. It's always easier to write 1000 words to say something than 100 to say it well.
The article didn't explain the abc conjecture in much detail ("The original proof is of the long-standing ABC conjecture that explores the deep nature of numbers, centred on the simple equation a + b = c."). That's unfortunate, because even though the proof is inscrutable, the conjecture itself isn't very complicated:
If three numbers a, b, and c are coprime and two numbers a and b have large prime factors, then their sum c generally does not.
To make that a little more formal, it means that the radical (product of distinct prime factors) of their product abc is usually less than the sum c, up to some exponent 1+eps:
rad(abc)^(1+eps) < c
... for some eps. That eps is important! There are infinitely many numbers a, b, c where this isn't true for some eps (and there are ways to construct those), but the conjecture states that for any given eps, there are finitely many.
To find maximal counterexamples (which, because mathematics consistently uses intuitive terminology, are said to be "high-quality") you typically look for numbers that are smooth (small prime factors) but not powersmooth (larger prime-factors-raised-to-a-power). Typically you'll also fix a to be really small, to limit the search space somewhat. [MM14] describes other methods for finding triples.
Here's a simple example of a high-quality triple:
a = 1
b = 2*3^7 = 4374
c = 5^4*7 = 4375
Because all factors are unique, rad(abc) = rad(a) rad(b) rad(c).
This is a great example, because the exponent (sometimes called q) is about 1.57, which is extraordinarily high. In the first billion c's, there are only 34 with q > 1.4. This is the fifth best such triple we know of. [triples]
Consider a trivial case where all three numbers are prime; a = 2, b = 3, c = 5. Primes are their own radical, so:
Some bitter conflict is referenced in footnote 1 of the 300 page summary.
"""
The author hears that a mathematician (I. F.), who pretends to understand inter-universal Teichm¨uller
theory, suggests in a literature that the author began to study inter-universal Teichm¨uller theory “by his
encouragement”. But, this differs from the fact that the author began it by his own will. The same person,
in other context as well, modified the author’s email with quotation symbol “>” and fabricated an email,
seemingly with ill-intention, as though the author had written it. The author would like to record these facts
here for avoiding misunderstandings or misdirections, arising from these kinds of cheats, of the comtemporary
and future people.
"""
I wonder if "I.F." is referring to the same "I.F." quoted in the original article.
I've personally modified thousands of e-mails with the ">" symbol; it's called replying. That, per se, has nothing to do with fabricating an e-mail; why mention it?
Of course > symbols are fairly likely to be used in a forged e-mail, possibly next to fake quoted text; but that then is not simply an alteration of genuine text by the addition of those symbols.
>"If nobody understands a mathematical proof, does it count?"
Just wait until general AI really kicks off, then all of new math will be like that. It's not that humans are bad at logical thinking, our weakness is memory. That won't be the case for an artificial agent with instantaneous perfect recall of everything it has ever seen.
I'm not a mathematician, so I don't know the significance of the ABC conjecture, but for those that are laymen like me, here's a quick introduction to the ABC conjecture:
I know there has been a lot of work in automated theorem proving.
I'm curious if anyone here is able to describe the state of the art in that. Is it really just a toy for basic things right now, or how realistic is it that we'd ever get to a point where the author of a paper like this could use a formal language to show that their proof is indeed valid and complete?
It is realistic in the sense that it has already been done! But it's still laborious in the extreme.
Kepler conjecture was stated in 1611 and had been unsolved since. Thomas Hales started a project to attack it in 1992. After six years of work, he announced the proof in 1998, in the form of 250 pages of argument and 3 gigabytes of computer calculation. He submitted it to Annals of Mathematics, one of the most prestigious math journal, for review. Reviewers and the author tried valiantly for five years, gave up, and published it in 2003 with a warning that while reviewers were 99% certain, it couldn't be completely reviewed.
Soon after getting this both rejection and acceptance, Thomas Hales announced the plan to formalize his proof to remove any uncertainty. It was enthusiastically received by automated theorem proving community. For a while Thomas Hales "shopped" for the prover tool to use and basically leaders of every significant provers tried to "sell" it to him. He decided on HOL Light, wrote the detailed plan for formalization, and estimated it would take 20 years. He actually carried out this plan, announced the completion in 2014, wrote the paper on formalization, and submitted the formalization paper, with 21 collaborators, in 2015. The formalization paper was published in 2017.
So there's that. The formal proof of Kepler conjecture is at the moment the most significant corpus of formalized mathematics in existence.
I am not an expert, but I recently took a course on formal systems, which included theorem proving. It was more focused on proving properties for code since this is the focus of my professor, but I was really surprised how well it was working. I also recently tried out Liquid-Haskell, which adds an SMT solver (i think...) to Haskell. In my opinion, theorem proving has come a long way and I think the challenge is now equal in theorem-proving and programming language. We have to get the ergonomics right, deriving properties for imperative code is awful. We need a super elegant, easy to use and not too restrictive language that can be verified automatically. The overhead of using it must be minimal.
By the way, if anyone is interested in getting a feel of the difference between these types of systems but is more just generally interested and doesn't necessarily have anything they want/need to prove themselves this: http://www.cs.ru.nl/~freek/comparison/comparison.pdf is a good document to skim through/jump around.
It's still a significant order of magnitude more time consuming to write a formal proof as you can't gloss over any details. Proof automation helps somewhat but the search space is so enormous it's not going to be feasible any time soon that you can avoid doing the difficult parts yourself. The formal proof for the Kepler conjecture involved around 15 people and was estimated to take around 20 years of work I think. If the summary for this proof is 300 pages, the formal proof would probably be 3K pages at least.
So, there are two main areas of development in the automation of theorem proving.
The first one is proof assistants, such as Isabelle/HOL, HOL Light, HOL4, Coq, PVS, Lean, TLApm (and others). These are typically languages to be used directly by a human, and share many common features with programming languages. In a sense, you "program" your proof. There are some large developments in such languages, as pointed out in other comments, including the Kepler conjecture (in HOL Light), the 4 colors theorem and Feit-Thompson theorem (in Coq), a fully verified micro-kernel (SEL4, in Isabelle/HOL), etc. It's an active research area with multiple teams around the world, but the provers are still difficult to use for non-experts. Isabelle/HOL has some nice features and good documentation that make it a bit more approachable to newcomers, afaik, and Lean has promising design decisions, but clearly right now it's a lot of effort to formalize anything consequent in proof assistants.
The second area is fully automatic provers — an endeavour started very early (50s, 60s?). Such provers accept a logic formula as input, and try to compute if it's a theorem or not. They typically accept more restricted fragments of logic (because it's a super hard problem!). Even first-order logic, which is less expressive (and convenient) than the higher-order logic usual in proof assistants, is semi-decidable only because of Gödel's incompleteness theorem. This means a prover for this logic will never terminate on some inputs that are not theorems. There still are interesting provers for FOL, e.g. [E](https://eprover.org). More restricted fragments that tools can effectively deal with are SAT (purely propositional logic, solvers are very good nowadays) and SMT (SAT + theories such as arithmetic) which is very useful in software verification (e.g. liquid haskell's type system, why3, boogie, F*, etc.).
There are people trying to join both domains of research by developing so-called "hammers", that make automatic provers available in proof assistants to make small proof steps entirely automatic.
question: if a reviewer is given a proof to verify, then is it possible to simply step through each transformation and verify it, without really understanding the entirety? Or in cases such as this are there steps that are new or obtuse enough that there isn't a way to verify them without understanding the whole thing. Or, are there individual steps that require so much work that it is impractical to verify them?
In practice, a proof contains many steps that are highly non-obvious unless you have a deep understanding of the subject. This is done not just for the sake of brevity, but also clarity. In a proof, there are a few key ideas you want to show. Around that, you need glue to convince the reader that your key ideas work, and save them from some the tedium and hard work of verifying that stuff.
A 1/4 page proof, when made as simple as you suggested, could easily bloom to 2 pages. At this point, your reader can no longer find those few key ideas, and is instead lost in the rigor.
If you write a proof in sufficient detail (which nobody does but is manifestly possible), it can be verified with no understanding at all. Indeed, it can be verified by ~300 lines of Python: http://us.metamath.org/downloads/mmverify.py
This process is very similar to analyzing the plot of a novel to the utmost detail: it depends not only on the "facts" but very much on the writing style (compare f.i. Joyce and H. James).
This sheds an interesting light on the referee process in that referees are given an inordinate amount of power in the scientific process.
Suppose I am a referee, then I am a mathematician and I generally want new and interesting work released having to do with my subject area because I want more students interested in those topics validating my general area of research. If I dont plan to personally build on this work (because maybe its too confusing or doesn't shed light on what I am working on), then in a case like this where the paper is so confounding, whats to keep me from simply saying "I understand this and its correct" even if that is not the case? Its not like if you referee and approve a paper that is later proven wrong (especially in a case like this) you are run out of the mathematical community. Do they need to provide detailed explanations as to why they think its right?
What would stop a referee from simply going along with it and approving this paper, especially when the community is confounded by it and doesn't want to do the work itself.
Does the rigor of scientific process ultimately just come down to unrigorous consensus?
That can occasionally happen with much less important papers; e.g. someone is asked to referee something, and doesn't really feel like actually reading it but would still like to see it published. If they are not conscientious they might only briefly skim the proof and write a hasty referee report.
But ABC is a major claim. The community will not be nearly so quick to reach a consensus. In particular, from what I can tell now there are a handful of mathematicians other than Mochizuki vouching for the proof, but even that is still not enough: overall, the community has yet to come to a consensus that this is enough.
> What's to keep me from simply saying "I understand this and its correct" even if that is not the case?
Then you should be able to have intelligent discussions about the paper and answer questions that come up. If you're pretending to understand it, a quick 5-minute discussion with a mathematician would reveal that this is not the case.
The proof apparently rests on an entirely new (not yet vetted) branch of number theory developed by the proof's author, "Inter-universal Teichmüller Theory". 45-page overview linked:
[+] [-] dmix|8 years ago|reply
> Despite mathematics being a universal language, culture clash could be getting in the way, says Kim. “In Japan people are pretty used to long, technical discussions by the lecturer that require a lot of concentration,” he says. “In America or England we expect much more interaction, pointed questions coming from the audience, at least some level of heated debate.”
> There is a growing consensus that Mochizuki has over-engineered his work, contributing to the confusion. “Most of the large theories that he builds are not essential. He could have written things in a much more streamlined way,” says Voloch.
This is a problem in a lot of technical fields but also in writing in general. It's always easier to write 1000 words to say something than 100 to say it well.
[+] [-] ghgr|8 years ago|reply
As (probably) Pascal said: "If I had more time, I would have written a shorter letter".
https://quoteinvestigator.com/2012/04/28/shorter-letter/
[+] [-] sebcat|8 years ago|reply
[+] [-] KGIII|8 years ago|reply
[+] [-] lvh|8 years ago|reply
If three numbers a, b, and c are coprime and two numbers a and b have large prime factors, then their sum c generally does not.
To make that a little more formal, it means that the radical (product of distinct prime factors) of their product abc is usually less than the sum c, up to some exponent 1+eps:
... for some eps. That eps is important! There are infinitely many numbers a, b, c where this isn't true for some eps (and there are ways to construct those), but the conjecture states that for any given eps, there are finitely many.To find maximal counterexamples (which, because mathematics consistently uses intuitive terminology, are said to be "high-quality") you typically look for numbers that are smooth (small prime factors) but not powersmooth (larger prime-factors-raised-to-a-power). Typically you'll also fix a to be really small, to limit the search space somewhat. [MM14] describes other methods for finding triples.
Here's a simple example of a high-quality triple:
Because all factors are unique, rad(abc) = rad(a) rad(b) rad(c). This is a great example, because the exponent (sometimes called q) is about 1.57, which is extraordinarily high. In the first billion c's, there are only 34 with q > 1.4. This is the fifth best such triple we know of. [triples]Consider a trivial case where all three numbers are prime; a = 2, b = 3, c = 5. Primes are their own radical, so:
This is the edge case.[triples]: https://www.math.leidenuniv.nl/~desmit/abc/index.php?set=2
[MM14]: https://arxiv.org/pdf/1409.2974.pdf
[+] [-] lvh|8 years ago|reply
[+] [-] Koshkin|8 years ago|reply
[+] [-] math_and_stuff|8 years ago|reply
""" The author hears that a mathematician (I. F.), who pretends to understand inter-universal Teichm¨uller theory, suggests in a literature that the author began to study inter-universal Teichm¨uller theory “by his encouragement”. But, this differs from the fact that the author began it by his own will. The same person, in other context as well, modified the author’s email with quotation symbol “>” and fabricated an email, seemingly with ill-intention, as though the author had written it. The author would like to record these facts here for avoiding misunderstandings or misdirections, arising from these kinds of cheats, of the comtemporary and future people. """
I wonder if "I.F." is referring to the same "I.F." quoted in the original article.
[1] http://www.kurims.kyoto-u.ac.jp/~gokun/DOCUMENTS/abc_ver6.pd...
[2] https://www.maths.nottingham.ac.uk/personal/ibf/activity.htm...
[+] [-] kazinator|8 years ago|reply
Of course > symbols are fairly likely to be used in a forged e-mail, possibly next to fake quoted text; but that then is not simply an alteration of genuine text by the addition of those symbols.
[+] [-] mrkgnao|8 years ago|reply
http://inference-review.com/article/fukugen
[+] [-] sanxiyn|8 years ago|reply
[+] [-] svisser|8 years ago|reply
The abc conjecture may be solved today but only when a sufficient number of people understand and accept the proof as a proof.
[+] [-] pacala|8 years ago|reply
[+] [-] MikkoFinell|8 years ago|reply
Just wait until general AI really kicks off, then all of new math will be like that. It's not that humans are bad at logical thinking, our weakness is memory. That won't be the case for an artificial agent with instantaneous perfect recall of everything it has ever seen.
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] tobhahn|8 years ago|reply
[deleted]
[+] [-] ZenoArrow|8 years ago|reply
https://m.youtube.com/watch?v=RkBl7WKzzRw
[+] [-] Joe-Z|8 years ago|reply
Also, the second-highest comment in this thread right now is one explaining this conjecture.
[+] [-] Koshkin|8 years ago|reply
[+] [-] crazygringo|8 years ago|reply
I'm curious if anyone here is able to describe the state of the art in that. Is it really just a toy for basic things right now, or how realistic is it that we'd ever get to a point where the author of a paper like this could use a formal language to show that their proof is indeed valid and complete?
[+] [-] sanxiyn|8 years ago|reply
Kepler conjecture was stated in 1611 and had been unsolved since. Thomas Hales started a project to attack it in 1992. After six years of work, he announced the proof in 1998, in the form of 250 pages of argument and 3 gigabytes of computer calculation. He submitted it to Annals of Mathematics, one of the most prestigious math journal, for review. Reviewers and the author tried valiantly for five years, gave up, and published it in 2003 with a warning that while reviewers were 99% certain, it couldn't be completely reviewed.
Soon after getting this both rejection and acceptance, Thomas Hales announced the plan to formalize his proof to remove any uncertainty. It was enthusiastically received by automated theorem proving community. For a while Thomas Hales "shopped" for the prover tool to use and basically leaders of every significant provers tried to "sell" it to him. He decided on HOL Light, wrote the detailed plan for formalization, and estimated it would take 20 years. He actually carried out this plan, announced the completion in 2014, wrote the paper on formalization, and submitted the formalization paper, with 21 collaborators, in 2015. The formalization paper was published in 2017.
So there's that. The formal proof of Kepler conjecture is at the moment the most significant corpus of formalized mathematics in existence.
[+] [-] LeanderK|8 years ago|reply
[+] [-] anewhnaccount2|8 years ago|reply
[+] [-] seanwilson|8 years ago|reply
[+] [-] c-cube|8 years ago|reply
The first one is proof assistants, such as Isabelle/HOL, HOL Light, HOL4, Coq, PVS, Lean, TLApm (and others). These are typically languages to be used directly by a human, and share many common features with programming languages. In a sense, you "program" your proof. There are some large developments in such languages, as pointed out in other comments, including the Kepler conjecture (in HOL Light), the 4 colors theorem and Feit-Thompson theorem (in Coq), a fully verified micro-kernel (SEL4, in Isabelle/HOL), etc. It's an active research area with multiple teams around the world, but the provers are still difficult to use for non-experts. Isabelle/HOL has some nice features and good documentation that make it a bit more approachable to newcomers, afaik, and Lean has promising design decisions, but clearly right now it's a lot of effort to formalize anything consequent in proof assistants.
The second area is fully automatic provers — an endeavour started very early (50s, 60s?). Such provers accept a logic formula as input, and try to compute if it's a theorem or not. They typically accept more restricted fragments of logic (because it's a super hard problem!). Even first-order logic, which is less expressive (and convenient) than the higher-order logic usual in proof assistants, is semi-decidable only because of Gödel's incompleteness theorem. This means a prover for this logic will never terminate on some inputs that are not theorems. There still are interesting provers for FOL, e.g. [E](https://eprover.org). More restricted fragments that tools can effectively deal with are SAT (purely propositional logic, solvers are very good nowadays) and SMT (SAT + theories such as arithmetic) which is very useful in software verification (e.g. liquid haskell's type system, why3, boogie, F*, etc.).
There are people trying to join both domains of research by developing so-called "hammers", that make automatic provers available in proof assistants to make small proof steps entirely automatic.
[+] [-] dmh2000|8 years ago|reply
[+] [-] rocqua|8 years ago|reply
A 1/4 page proof, when made as simple as you suggested, could easily bloom to 2 pages. At this point, your reader can no longer find those few key ideas, and is instead lost in the rigor.
[+] [-] sanxiyn|8 years ago|reply
[+] [-] pfortuny|8 years ago|reply
[+] [-] nautilus12|8 years ago|reply
Suppose I am a referee, then I am a mathematician and I generally want new and interesting work released having to do with my subject area because I want more students interested in those topics validating my general area of research. If I dont plan to personally build on this work (because maybe its too confusing or doesn't shed light on what I am working on), then in a case like this where the paper is so confounding, whats to keep me from simply saying "I understand this and its correct" even if that is not the case? Its not like if you referee and approve a paper that is later proven wrong (especially in a case like this) you are run out of the mathematical community. Do they need to provide detailed explanations as to why they think its right?
What would stop a referee from simply going along with it and approving this paper, especially when the community is confounded by it and doesn't want to do the work itself.
Does the rigor of scientific process ultimately just come down to unrigorous consensus?
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] impendia|8 years ago|reply
That can occasionally happen with much less important papers; e.g. someone is asked to referee something, and doesn't really feel like actually reading it but would still like to see it published. If they are not conscientious they might only briefly skim the proof and write a hasty referee report.
But ABC is a major claim. The community will not be nearly so quick to reach a consensus. In particular, from what I can tell now there are a handful of mathematicians other than Mochizuki vouching for the proof, but even that is still not enough: overall, the community has yet to come to a consensus that this is enough.
[+] [-] luckyt|8 years ago|reply
Then you should be able to have intelligent discussions about the paper and answer questions that come up. If you're pretending to understand it, a quick 5-minute discussion with a mathematician would reveal that this is not the case.
[+] [-] TimTheTinker|8 years ago|reply
http://www.kurims.kyoto-u.ac.jp/%7Emotizuki/Panoramic%20Over...
[+] [-] rusanu|8 years ago|reply
So is not really a summary, is more of a reformulation, an easier to read rewrite.
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] unknown|8 years ago|reply
[deleted]
[+] [-] shad0wca7|8 years ago|reply
[+] [-] Phosphenes|8 years ago|reply
[+] [-] unknown|8 years ago|reply
[deleted]