8 ms·
The ABC conjecture has still not been proved
- rconti 9y agoI posit that there are, in fact, times that one should be doing things other than closing.
- taneq 9y ago"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.
- leoc 9y ago"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." https://en.wikiquote.org/wiki/Miyamoto_Musashi#The_Water_Book https://en.wikiquote.org/wiki/Miyamoto_Musashi#The_Water_Boo...
- taneq 9y ago"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
- adamnemecek 9y agoIf only we had automated proof assistants that could check the proof quickly. Oh wait.
- monochromatic 9y agoUnfortunately, coq can’t parse just anything.
- dogecoinbase 9y agoThis comment does nothing other than demonstrate your own ignorance of research mathematics.
- adamnemecek 9y agoPlease keep going.
- deleted 9y ago[deleted]
- reallydude 9y agoWhy bother?
- qmalzp 9y agoI 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.
- dang 9y agoPlease don't post snarky dismissals to Hacker News. I'm dismayed to see this from you here.
- bo1024 9y agoUnfortunately 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.
- kurthr 9y agotl;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.
- jacobolus 9y agoMendel 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/cc-00.pdf 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.
- kurthr 9y agoYes, 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).
- hamilyon2 9y agoCould 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?
- 9y ago
- Sniffnoy 9y agoTerry 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. (Comment link: https://galoisrepresentations.wordpress.com/2017/12/17/the-abc-conjecture-has-still-not-been-proved/#comment-4563 https://galoisrepresentations.wordpress.com/2017/12/17/the-a... )
- chx 9y agoThis 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.
- moomin 9y agoThis. 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.
- AstralStorm 9y agoThose proofs can be cleaned up and analysed. 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...
- ilitirit 9y agoThings that provide no insight now may have theoretical or even practical applications in the future. https://mathoverflow.net/questions/116627/useless-math-that-became-useful/ https://mathoverflow.net/questions/116627/useless-math-that-... I'm not saying that this is the same of Mochizuki's work, but I would not dismiss it solely on the basis that it's "useles".
- moomin 9y agoI 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.
- placebo 9y agoThis 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 .
- Certhas 9y ago"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.
- deleted 9y ago[deleted]
- tel 9y agoWhile 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".
- mherrmann 9y agoIt 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."
- enedil 9y agoI 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.
- jonsen 9y agoIn this case it's not just mentioning. It's a twist of thought. This kind of comments can promote thinking outside conventional borders.
- vog 9y agoI like that story, too, but note that the actual quote was: "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." https://upload.wikimedia.org/wikipedia/commons/2/24/Diophantus-II-8.jpg https://upload.wikimedia.org/wikipedia/commons/2/24/Diophant... https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Fermat%27s_conjecture https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Fermat...
- vog 9y agoWow, being downvoted for correcting a misquote. That's HN at its best.
- williamdclt 9y agoThis was not a quote
- hardlianotion 9y agoThe vote was very harsh, but parent was laying out some kind of opposite to the quote, not misquoting
- tontonius 9y agoMochizuki 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! [1] ALIEN COPIES, GAUSSIANS, & INTER-UNIVERSAL TEICHMULLER THEORY (http://www.kurims.kyoto-u.ac.jp/~motizuki/Alien%20Copies,%20Gaussians,%20and%20Inter-universal%20Teichmuller%20Theory.pdf http://www.kurims.kyoto-u.ac.jp/~motizuki/Alien%20Copies,%20...)
- nautilus12 9y agoSounds like a way of justifying the fact that his results are totally silo'd off from the rest of the mathematical cannon
- robinhouston 9y agoIt’s worth revisiting this very nice article (2013) by Caroline Chen, which gives a vivid impression of the situation at that time. http://projectwordsworth.com/the-paradox-of-the-proof/ http://projectwordsworth.com/the-paradox-of-the-proof/ In a way, the only “news” since then is that the mathematical community hasn’t made any real progress with understanding Mochizuki’s theory.
- deleted 9y ago[deleted]
- muizelaar 9y agoHere's an article on IUT that shows that progress is being made: http://inference-review.com/article/fukugen http://inference-review.com/article/fukugen
- DaggerSpaces 9y agoComments now by Terry Tao and Peter Scholze (PS). That's some heavy fire power.
- woopwoop 9y agoScholze's comment is particularly interesting.