Terry Tao's comment in the comments section is particularly worth pointing out, I think:
> I do not have the expertise to have an informed first-hand opinion on Mochizuki’s work, but on comparing this story with the work of Perelman and Yitang Zhang you mentioned that I am much more familiar with, one striking difference to me has been the presence of short “proof of concept” statements in the latter but not in the former, by which I mean ways in which the methods in the papers in question can be used relatively quickly to obtain new non-trivial results of interest (or even a new proof of an existing non-trivial result) in an existing field. In the case of Perelman’s work, already by the fifth page of the first paper Perelman had a novel interpretation of Ricci flow as a gradient flow which looked very promising, and by the seventh page he had used this interpretation to establish a “no breathers” theorem for the Ricci flow that, while being far short of what was needed to finish off the Poincare conjecture, was already a new and interesting result, and I think was one of the reasons why experts in the field were immediately convinced that there was lots of good stuff in these papers. Yitang Zhang’s 54 page paper spends more time on material that is standard to the experts [...] but about six pages after all the lemmas are presented, Yitang has made a non-trivial observation, which is that bounded gaps between primes would follow if one could make any improvement to the Bombieri-Vinogradov theorem for smooth moduli. [...]
> From what I have read and heard, I gather that currently, the shortest “proof of concept” of a non-trivial result in an existing (i.e. non-IUTT) field in Mochizuki’s work is the 300+ page argument needed to establish the abc conjecture. It seems to me that having a shorter proof of concept (e.g. <100 pages) would help dispel scepticism about the argument. It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever.
I am very disturbed by the unfair manner in which Yau Shing-Tung has been portrayed in the New Yorker article. I am providing my thoughts below to set the record straight. I authorize you to share this letter with the New Yorker and the public if that will be helpful to Yau.
As soon as my first paper on the Ricci Flow on three dimensional mani- folds with positive Ricci curvature was complete in the early '80's,Yau immedi- ately recognized it's importance;and although I had proved a result on which he had been working with minimal surfaces,rather than exhibit any jealosy he became my strongest supporter.He pointed out to me way back then that the Ricci Flow would form the neck pinch singularities,undoing the connected sum decomposition,and that this could lead to a proof of the Poincare conjec- ture.In 1985 he brought me to UC San Diego together with Rick Schoen and Gerhard Huisken,and we had a very exciting and productive group in Geomet - ric Analysis.Huisken was working on the Mean Curvature Flow for hypersurfaces,which closely parallels the Ricci Flow,being the most natural flows for intrinsic and extrinsic curvature respectively.Yau repeatedly urged us to study the blow-up of singularities in these parabolic equations using techniques parallel to those developed for elliptic equations like the minimal surface equation,on which Yau and Rick are experts.Without Yau's guidance and support at this early stage,there would have been no Ricci Flow program for Perelman to finish.
Yau also had some outstanding students at San Diego who had come with him from Princeton, in particular Cao Huai-Dong,Ben Chow and Shi Wan- Xiong. Yau encouraged them to work on the Ricci Flow,and all made very important contributions to the field.Cao proved existence for all time for the normalized Ricci Flow in the canonical Kaehler case ,and convergence for zero or negative Chern class.Cao's results form the basis for Perelman's excit - ing work on the Kaehler Ricci Flow,where he shows for positive Chern class that the diameter and scalar curvature are bounded. Ben Chow,in addition to excellent work on other flows,extended my work on the Ricci Flow on the two dimensional sphere to the case of curvature of varying sign.Shi Wan- Xiong pioneered the study of the Ricci Flow on complete noncompact manifolds,and in addition to many beautiful arguments he proved the local derivative estimates for the Ricci Flow.The blow-up of singularities usually produces noncompact solutions,and the proof of convergence to the blow-up limit always depends on Shi's derivative estimates; so Shi's work is central to all the limit arguments Perelman and I use.
In '82 Yau and Peter Li wrote an exceedingly important paper giving a pointwise differential inequality for linear heat equations which can be inte- grated along curves to give classic Harnack inequalities. Yau repeatedly urged me to study this paper,and based on their approach I was able to prove Har- nack inequalities for the Ricci Flow and for the Mean Curvature Flow. This Harnack inequality,generalized from Li-Yau,forms the basis for the analysis of ancient solutions which I started, and which Perelman completed and uses as the basic tool in his canonical neighborhood theorem. Cao Huai-Dong proved the Harnack estimate for the Ricci Flow in the Kahler case,and Ben Chow did the same for the Yamabe Flow and the Gauss Curvature Flow.
But there is more to this story. Perelman's most important is his noncol- lapsing result for Ricci Flow,valid in all dimensions,not just three,and thus one whose importance for the future extends well beyond the Poincare conjecture,where it is the tool for ruling out cigars,the one part of the singular- ity classification I could not do. This result has two proofs,one using an entropy for a backward scalar heat equation,and one using a path integral.The entropy estimate comes from integrating a Li-Yau type differential Harnack inequality for the adjoint heat equation,and the other is the optimal Li-Yau path integral for the same Harnack inequality; as Perelman acknowledges in 7.4 of his first paper,where he writes "an even closer reference is [L-Y],where they use "length" associated to a linear parabolic equation,which is pretty much the same as in our case".
Over the years Yau has consistently supported the Ricci Flow and the whole field of Geometric Flows,which has other important successes as well,such as the recent proof of the Penrose Conjecture by Huisken and Ilmanen,a very important result in General Relativity. I cannot think of any other prominent leader who gave nearly support to our field as Yau has.
Yau has built is an assembly of talent,not an empire of power,people attracted by his energy,his brilliant ideas,and his unflagging support for first rate mathematics, people whom Yau has brought together to work on the hard- est problems.Yau and I have spent innumerable hours over many years work- ing together on the Ricci Flow and other problems,often even late at night. He has always generously shared his suggestions with me,starting with the obser- vation of neck pinches,never asking for credit. In fact just last winter when I finally managed to prove a local version of the Harnack inequality for the Ricci Flow,a problem we had worked on together for many years,and I said I ought to add his name to the paper,he modestly declined.It is unfortunate that his character has been so badly misrepresented.He has never to my knowledge proposed any percentages of credit,nor that Perelman should share credit for the Poincare conjecture with anyone but me; which is reasonable,as indeed no one has been more generous in crediting my work than Perelman himself.Far from stealing credit for Perelman's accomplishment,he has praised Perelman's work and joined me in supporting him for the Fields Medal.And indeed no one is more responsible than Yau for creating the program on Ricci Flow which Perelman used to win this prize.
Interesting letter. I am aware that there was resistance from certain figures because of its portrayal of Yau Shing-Tung, but I had no idea Richard Hamilton sent them a letter about it (it's been 10 years since I read this article).
However, IMO the piece is still worth reading (along with the objections...) in terms of how it gave exposure to solution of the Poincare conjecture.
edit: Heh... it seems I should have followed the developments more closely. It turns out the Cao–Zhu paper was revised that same year:
> On December 3, 2006, Cao and Zhu retracted the original version of their paper, which was titled “A Complete Proof of the Poincaré and Geometrization Conjectures — Application of the Hamilton–Perelman Theory of the Ricci Flow”[2] and posted a revised version, renamed, more modestly, "Hamilton–Perelman's Proof of the Poincaré Conjecture and the Geometrization Conjecture".[21] Rather than the claim of the original abstract, "we give a complete proof", suggesting the proof is by the authors, the revised abstract states: "we give a detailed exposition of a complete proof". The authors also took out the phrase "crowning achievement" from the abstract.
In retrospect, the episode sullied the reputation of everyone involved. If Perelman were less private it likely would’ve created less space for others to fill the space. It made everyone, including medalists like Hamilton and Yau, look like publicity starved careerists. I don’t have an opinion about whether careerism or a need for publicity is bad but I can confidently say that both are viewed negatively inside the mathematics community. It was a weird situation.
If the article was that bad, how come he went through the trouble of hiring attorneys to draft letters accusing the author of defamation, threaten action, and never took it any further?
There was never any apology or retraction seeming to remove settlement an a possible result.
I have no reason to doubt the claims against the article, at first glance there are a significant number of credible sources supporting the idea the article was flawed, yet the claims were ineffective legally.
Of course it’s not easy or cheap to pursue a case of defamation, however, I think it money was the issue he could have rallied some public support. If I were asked, it’s certainly an issue I would do the due diligence on and contribute something to if it made sense.
edit: btw why is no one making a movie about this? There are so many fascinating aspects, the grand challenge, the controversy, the mathematician who declined a million dollar prize. I’d love to do even a documentary on it, or watch one if it’s been done.
In addition (not a lawyer here, but I believe this is well established territory), defamation is difficult to prove, and suing someone over an article almost always carries some negative press, regardless of the merits.
That’s the point, I mentioned the difficulty in fact. But he chose to step across that bridge and then abandon it. What else can we conclude other than, heat of the moment emotional decision, or that the merits were, if morally strong enough, not legally strong enough?
This reminds me how László Mérő, a Hungarian mathematician (and a lot other things) called certain theorems a "kitsch" if they stand alone, if they do not advance mathematics in any way. He used the well known four color graph theorem as a perhaps surprising one: you could take existing methods (discharging) and apply brute force and be done.
Mochizuki is a badass, elitist rock star of mathematics and he takes his time to roast the entire field in his papers [1].
P.115
>The adoption of strictly linear evolutionary models of progress in mathematics of the sort discussed [previously] tends to be highly attractive to many mathematicians in light of the intoxicating simplicity of such strictly linear evolutionary models, by comparison to the more complicated point of view discussed [previously]. This intoxicating simplicity also makes such strictly linear evolutionary models — together with strictly linear numerical evaluation devices such as the “number of papers published”, the “number of citations of published papers”, or other likeminded narrowly defined data formats that have been concocted for measuring progress in mathematics — highly enticing to administrators who are charged with the tasks of evaluating, hiring, or promoting mathematicians.
> Moreover, this state of affairs that regulates the collection of individuals who are granted the license and resources necessary to actively engage in mathematical research tends to have the effect, over the long term, of stifling efforts by young researchers to conduct long-term mathematical research in directions that substantially diverge from the strictly linear evolutionary models that have been adopted, thus making it exceedingly difficult for new “unanticipated” evolutionary branches in the development of mathematics to sprout.
I also recommend reading page 114 where he lists some 14 breakthroughs made in his paper, and how many years earlier they could have been made. The audacity of this guy!
This got me thinking about human cognition and the meaning of mathematical truths, or even how does one know that something is true (and I assume that probably none of this is original).
At which point would Mochizuki’s work be considered proof? If another person regarded as an authority would claim to fully understand it (but couldn't explain it better to their peers)? If only 10% of mathematicians specialising in this field could understand it? If 40%?
What if only a few percent understood the proof, but managed to "prove" to others that they understood it by using this knowledge to unlock other difficult problems?
This seems to point that even in mathematics we can never claim to know what is true. At most, we can hold a belief, an assessment based on some parameters that increases our degree of belief that something is true.
In fact, there's no need for a controversial proof to show this - it occurs with the simplest of mathematical proofs -
after all, everything we believe in is based on the ability to detect consistency or lack thereof, which in itself is based on the ability of a system (in this case, our brains) to have a memory and notice where something happening now is consistent or inconsistent with something stored in our memory. Now this is quite problematic in terms of proof, because how can we trust our memory with a 100% certainty? The answer is that we can't. We attribute a high probability that what we know is true based on the consistency of other things we remember, but we can never prove anything .
"What if only a few percent understood the proof, but managed to "prove" to others that they understood it by using this knowledge to unlock other difficult problems?"
Check the Terrence Tao comment below the post (also posted by someone else in here).
I think if those who claim to understand the proof could use the techniques to proof other things, or even to provide new proofs of known results, the level of trust would immediately go up dramatically.
While on one hand your "degrees of uncertainty" approach here is a pretty nice and valid one most of the time, I'd like to present another idea of mathematical proof.
Something cannot be proven to a collection of people, but it can be proven to an individual. You can further say that a proof is generally true if, in principle, it can be proven to any given individual under mild assumptions of their mathematical experience.
To prove something to an individual is to actually walk them through each step and show that they follow one after another. Actual mathematical proofs rarely follow such a simplified flow, but again in principle they _could_ and the missing steps are elided under the assumption that someone could in principle reconstruct them whenever they like (this time perhaps making slightly stronger assumptions about their background and skill).
So, for all people the ABC conjecture will only become a theorem when they personally have walked through the proof. It's very expensive for any person to do this for any proofs they want to own, but they should do so for core ones and should feel comfortable that they could in principle do it for any that they take faith on.
Thus, the ABC conjecture may fail to be a proof practically for at least two reasons: (1) it's just factually wrong, it does not exist as a script for making step-by-step deduction to the conclusion or (2) there is no pathway for a reasonable person to obtain confidence that they could in principle verify it.
For instance, it could fail to be a proof for reason (2) entirely because IUTT is extremely complex and totally useless for all things besides the ABC conjecture. It would never be in the best interest of any person to obtain enough familiarity with IUTT to make the conjecture available to "in principle" verification.
It seems like (2) is sort of the case as well.
So, you can again boil this down to degrees-of-uncertainty and betting odds if you want, but proof has some interesting other dynamics:
- the notion that it's about communication of an idea
- the notion that it's dependent upon each individual's verification
- the notion of "in principle" verifications
- the notion of personal expense
In particular, it creates a divide between some sort of Platonic reality and a person's belief but guards it by expense of consuming/integrating information instead of expense of gathering data.
For instance, assume a completely trusted (99.99%) third party reads the proof and commits that it is correct. Bayesian reasoning would suggest that even if the person is normally trustworthy they could still be fallible and would still lend a lot of doubt to the truth of their words.
But no number of tests could make this more "proven" to you if it's still just not worth the effort for anyone else to ever read the paper and internalize it. You'd never be able to justify the costs of those other tests because it's just so impractical as to never really reach the status of "universally accepted as true".
tl;dr
Until someone can explain the proof in something under 100s of hours, it's not considered proven. It's not useful until someone uses IUT as a tool.
It reminds me of other fields of science (like genetics) where many people have made a similar "discovery", but one person finally discovers and reports the results so clearly (e.g. Gregor Mendel) that everyone recognizes them as the discoverer... even though others came before (e.g. Imre Festetics) with similar concepts.
Mendel was a monk and high school teacher whose work (he spent a decade hybridizing pea plants in the monastery garden) was published in small regional sources and languished in obscurity for decades. Nobody at the time understood the importance of his work, and biologists continued under mistaken models of how inheritance worked. Decades later other botanists did similar experiments, and then stumbled over Mendel's papers, and credited him for first developing and experimentally validating the correct model. e.g. Correns http://www.esp.org/foundations/genetics/classical/holdings/c...
As far as I know Mendel's model was much simpler and more clearly defined than anything that came before.
Yes, exactly, he discovered it well enough that people who read his papers years later didn't need for it to be discovered again. I agree, those at the time of publishing didn't even consider it to be about inheritance, but those later did, because his careful work could be replicated... even though Imre Festetics coined the word genetic and did similar work on sheep in the same town many years before (he's mostly forgotten).
Could it be that someone, in some obscure regional mathematics journal already proved abc conjecture in 30 pages. No one took his work seriously enough, and his work would be discovered by accdent 100 years after publication?
I would sure be convinced by a Coq proof I couldn't understand. Professional mathematicians will face that kind of result eventually, if we keep progressing.
Counterexample: The Four Color Theorem (which states that any 2-dimensional map can be colored with four colors such that no two bordering countries have the same color). It is considered proven even though the proof involves a giant computer verification which certainly can't be explained in under 100s of hours.
> Counterexample: The Four Color Theorem (which states that any 2-dimensional map can be colored with four colors such that no two bordering countries have the same color). It is considered proven even though the proof involves a giant computer verification which certainly can't be explained in under 100s of hours.
There exists a proof of the Four Color Theorem by Georges Gonthier that has been verified in Coq:
This. Mathematics is not really the study of what is the case, it’s the study of why. Even if this was accompanied by a full Coq proof it would be unsatisfactory because absolutely no insight is being provided.
I don't think anything on that list was bereft of insight, even at the time. This is a context issue: the problem with Mochizuki's work is that no-one has managed to point to a single insight other than the abc conjecture. Whilst it's possible to prove certain results by brute force manipulation, it's not common. High profile results tend to be accompanied with subsidiary insights. The applicability of these insights to real world problems is, for the purposes of this discussion, beside the point.
Anyway, I'm basically repeating what people have already said. So I'll stop.
However generating a proof like that in the first place is a really tough task involving searches and codification of advanced known mathematics in Coq proof way.
In this way, semi auto prover like Isabelke are nicer fort mathematicians as they will ask about holes...
"Close" means different things to people in different roles. To a salesman, it means make the sale. To a mathematician in academia, it means publish. To a product team, it means ship.
"The primary thing when you take a sword in your hands is your intention to cut the enemy, whatever the means. Whenever you parry, hit, spring, strike or touch the enemy's cutting sword, you must cut the enemy in the same movement. It is essential to attain this. If you think only of hitting, springing, striking or touching the enemy, you will not be able actually to cut him."
"All warfare is based on closing. Hence, when we are able to attack, we must close; when using our forces, we must close; when we are near, we must close; when far away, we must close." - Sun Tsu
It sounds a little like the opposite of Fermat's famous statement about his last theorem. "I have a truly marvelous demonstration of this proposition. It only takes 300 obscure pages to explain."
I wonder why when people are talking about some math discoveries, there's always someone who'll mention that truly marvellous proof by Fermat (or at least his Last Theorem). That has become repetitive and quite often without a link strong enough to justify expressed opinion.
I have never seen a theorem prover applied to even basic 100-year-old results in Algebraic Number Theory. I think you underestimate the difficulty in translating a mathematical idea into a format a computer program can understand.
Unfortunately at this juncture, it's extremely difficult and time-consuming to place an arbitrary proof in the language of proof assistants. It's a very noble goal and much respect to those who do it, but even fully formalizing something like the four-color theorem is a major accomplishment.
> I do not have the expertise to have an informed first-hand opinion on Mochizuki’s work, but on comparing this story with the work of Perelman and Yitang Zhang you mentioned that I am much more familiar with, one striking difference to me has been the presence of short “proof of concept” statements in the latter but not in the former, by which I mean ways in which the methods in the papers in question can be used relatively quickly to obtain new non-trivial results of interest (or even a new proof of an existing non-trivial result) in an existing field. In the case of Perelman’s work, already by the fifth page of the first paper Perelman had a novel interpretation of Ricci flow as a gradient flow which looked very promising, and by the seventh page he had used this interpretation to establish a “no breathers” theorem for the Ricci flow that, while being far short of what was needed to finish off the Poincare conjecture, was already a new and interesting result, and I think was one of the reasons why experts in the field were immediately convinced that there was lots of good stuff in these papers. Yitang Zhang’s 54 page paper spends more time on material that is standard to the experts [...] but about six pages after all the lemmas are presented, Yitang has made a non-trivial observation, which is that bounded gaps between primes would follow if one could make any improvement to the Bombieri-Vinogradov theorem for smooth moduli. [...]
> From what I have read and heard, I gather that currently, the shortest “proof of concept” of a non-trivial result in an existing (i.e. non-IUTT) field in Mochizuki’s work is the 300+ page argument needed to establish the abc conjecture. It seems to me that having a shorter proof of concept (e.g. <100 pages) would help dispel scepticism about the argument. It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever.
(Comment link: https://galoisrepresentations.wordpress.com/2017/12/17/the-a... )