13 ms·
Mathematician's anger over his unread 500-page proof
- hoopism 12y agoDon't feel bad. I can't get coworkers to read 2 page approach docs.
- ableal 12y agoI not too sure about emails with ten lines.
- nabla9 12y agoHopefully someday, model checkers and proof assistants can help mathematicians to put these monster proofs into format that can be verified with computer.
- kodis 12y agoYes, assuming that there remain any proofs which the model checkers and proof assistants haven't already discovered!
- marcosdumay 12y agoThe space of proofs is enormous. Model checkers and proof assistants will probably become user friendly much sooner than they'll get good enough heuristics to navigate such spaces.
- deepsun 12y agoWhen I was a student, I started making such a system. It would also be very beneficial for students for explaining complex proofs. The main problem is not in model checker (there are plenty of them already), but to automatically convert between a model checker syntax (that looks rather like a programming language), and regular math paper syntax (which is free-form English, so you need general AI for reading that). I was already quite experienced programmer at that time, but realized the UI/UX problem is too big for me alone, even if I'm going to parse some simplified English. But with simplified English, the problem is definitely solvable, someone just needs to put their time/money in that. Once UX is good enough for mathematicians, professors or students, it will lift off and be the Wikipedia for Mathematics.
- cskau 12y agohttps://coq.inria.fr/ https://coq.inria.fr/
- fibo 12y agoOften happens that after an hard proof there are less t'han 10 People that can understand it. Also happened for Fermat Conjecture proved in 1997, after 5k years! Also with shorter proofs can be tricky. I studied at University a proof of Stoker Theorem by Poincaré that fits in one page, but, trust me that it is really diabolic.
- pfortuny 12y agoYou probably mean 5C=D years but the logic is the same... :-)
- rando3826 12y agoWhat are C=D years?
- noblethrasher 12y agoC and D are the Roman numerals corresponding to 100 and 500 respectively. Hence, 5C = D. But, the larger point was that took 500 (5C) rather than 5000 (5K) years to prove Fermat's Last Theorem.
- deleted 12y ago[deleted]
- Someone 12y agoI = 1 V = 5 X = 10 L = 50 C = 100 D = 500 M = 1000 => D = 5C or, equivalently, 5C=D It's more like 8L years ago, though.
- gecko 12y agoHe did the entire 500-page paper in isolation and refuses to lecture on it in any capacity anywhere other than his own university. He may be right, and he may not be, but his failure to get an answer from the community is his fault, not theirs.
- jblow 12y agoMath is supposed to be about pursuit of truth, not how congenial you are.
- lomnakkus 12y agoLike it or not, but math these days is a kind of social activity.
- deleted 12y ago[deleted]
- pavel_lishin 12y agoMy friends and I occasionally joke that the worse a professor's/programmer's/scientist's personal university webpage, the better they are at their actual profession.
- pekk 12y agoNobody asked you how good he was as a web designer.
- deleted 12y ago[deleted]
- Goronmon 12y agoIt's really not though. It's basically a sign that he's an academic, and again, not a web developer.
- robbrulinski 12y agoThis man invented bitcoin.
- taternuts 12y agoI thought he looked familiar... I definitely remember his photo making the rounds as "Potential Satoshi"'s when that was the media craze of the week
- bengali3 12y agoyup, i recognized the photo as well http://chartgirl.com/wordpress/wp-content/uploads/2013/05/SATOSHI_large.jpg http://chartgirl.com/wordpress/wp-content/uploads/2013/05/SA...
- psychometry 12y agoDo you people not understand most of that infographic is a joke?
- mietek 12y ago> Grigori Perelman, another mathematician who refused to engage with the mathematical community That’s not quite it. http://www.newyorker.com/magazine/2006/08/28/manifold-destiny http://www.newyorker.com/magazine/2006/08/28/manifold-destin...
- wetmore 12y agoThat article isn't quite it either: http://en.wikipedia.org/wiki/Manifold_Destiny#Controversy http://en.wikipedia.org/wiki/Manifold_Destiny#Controversy
- udev 12y agoI feel for the guy. At the same time one can argue that if len ( Proof1 ) < len ( Proof2 ), where Proof1 and Proof2 are of the same theorem, then Proof1 imposes less cost, and hence is more valuable, since it will be easier to teach, use. etc.
- trhway 12y agoa frequent situation is that the first proof is really long and convoluted. Later, after building up of much of a theory construction blocks around, the proof becomes "simpler" (i.e. simpler combination of well established in that area "blocks") and that is what frequently taught later to students and to "outsiders". For such first long proofs among the best approaches is to throw it to the pack of hungry wolves ... err ... students and first years PhD-s and let them gnaw on it (with presenting their progress on weekly department seminars - thus saving time to more valuable members of the department and providing the students with real-life experience of a mathematician) Well, at least this is how it was done back then at our University (in Russia :).
- wetmore 12y agoThis would be relevant if there was another proof of the ABC conjecture available.
- udev 12y agojust take len ( Proof2 ) = infinity
- placebo 12y agoNo doubt the guy's exceptionally brilliant, and perhaps one day a mathematician with enough motivation to do it will spend a very long time trying to understand and decipher what he constructed, but my take on it is that anyone that wants to communicate a message, no matter how brilliant, should also go to the trouble of making it as legible as possible to others.
- therobot24 12y agoThis is actually a major gripe of mine when reading papers - not enough effort to communicate the math so it's readable. It's really frustrating to decipher a paper when there's a lot of hand waving. It's 10x worse when buzzwords or unimportant relationships are also included.
- RBerenguel 12y agoIf you've gone through paper-publishing, editors ask for pretty large reductions. A 29 page paper can easily be a 50-60 pages paper with "decent details" or a 150 pages paper with clear explanations of all details.
- raverbashing 12y agoSure, publish the reduced paper in the journal, then have the "Scenic Guide" in your webpage or ArXiv, or wherever Or, I dunno, just create a subreddit or a StackOverflow page for it
- arjunnarayan 12y agoThe best, most readable version is often the author's dissertation, although this obviously only applies for the works of graduate students.
- RBerenguel 12y agoThis assumes infinite time to add all minutiae to LaTeX. Not everyone works directly on that, almost everyone thinks on paper, develops ideas on paper and then TeXifies it. In my case, most of the "it is clear that" never made it into any version of the final file.
- dzdt 12y agoThere is a really good article here :http://projectwordsworth.com/the-paradox-of-the-proof/ http://projectwordsworth.com/the-paradox-of-the-proof/. That is from May 2013; the situation is basically unchanged since.
- dang 12y agohttps://news.ycombinator.com/item?id=5685166 https://news.ycombinator.com/item?id=5685166
- briantakita 12y agoI have a similar issue with a philosophy that I'm creating. There are some barriers. Off the top of my head... 1. The reader has to care enough to expend time & energy to understand the concepts 2. The reader comes in with an Existential Context that may have to be suspended or expanded. This is tricky because Existence is a fractal of nuance and it's difficult to know when there's a misunderstanding. Conversations & isolating examples help. 3. The reader has to be willing to adopt the new Existential Context while reading the works. 4. The more ridged & complex the context, the more the reader has to deny self.
- sosuke 12y agoHe will be doing a workshop: RIMS Joint Research Workshop: On the verification and further development of inter-universal Teichmuller theory (in Japanese) http://www.kurims.kyoto-u.ac.jp/~motizuki/2015-03%20IUTeich%20Program%20(English).pdf http://www.kurims.kyoto-u.ac.jp/~motizuki/2015-03%20IUTeich%... March 9-20 2015
- DMac87 12y agoThis and many comments seem to miss the facts, at least as presented on the ABC conjecture's wikipedia page http://en.wikipedia.org/wiki/Abc_conjecture http://en.wikipedia.org/wiki/Abc_conjecture: - An error was found in 2012 and was just recently (Nov 2014) corrected - He's re-released his notes & lectures on the subject - A workshop will be held on the topic in March That doesn't seem to be unusual / isolationist behavior, though it's obviously a complicated topic and since Fermat's Last Theorem has been deemed 'solved' already, the fact that it makes a FLT proof easier isn't much appreciated by the press / community.
- lotsofmangos 12y agoHey, it's New Scientist - http://www.wired.com/images_blogs/beyond_the_beyond/2009/07/020709.jpg http://www.wired.com/images_blogs/beyond_the_beyond/2009/07/... The angry isolated maths geek sells better. This happened to Scientific American though and I stopped buying it. On a long enough timeline, it seems all popular science magazines may turn into Focus.
- deleted 12y ago[deleted]
- MicroBerto 12y agoWhat real-world purpose does this conjecture hold, and why is its proof of any importance?
- bengali3 12y agosee http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Monetary_prizes http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Monetar...
- tedunangst 12y ago? The Fermat prize money has already been collected. If the real world purpose of this conjecture is to collect prize money, it won't be that prize.
- 1stop 12y agoAndrew Wiles already solved that...
- jackmaney 12y agohttp://ars.userfriendly.org/cartoons/?id=20070105 http://ars.userfriendly.org/cartoons/?id=20070105
- hiou 12y ago> This sense of stubbornness, dignity and pride is a part of what gives him the personality necessary to embark on a project like this It is always interesting to me, as I see it often in the software world, that people expect extraordinary people to behave like ordinary people.
- rando3826 12y agoFuck you (I'm extraordinary)
- mhomde 12y agoI'm kinda amazed that no one has been able to write a proof solving AI yet. While a human AI is a very daunting task in order to capture "humaness" and large problem-set it would seem to me that an AI working solely as a domain expert within maths should be much more feasible. Shouldn't you be able to build a database of all current proofs and have a computer be able to cross-reference and extrapolate from that? Sure it would be far from trivial but it seems doable. Mathematica/Wolfram for instance should be half way there. Here's the golden chance for a programmer to win x amount of Nobel prizes! :)
- DMac87 12y agoThis is an area of research: http://en.wikipedia.org/wiki/Automated_theorem_proving http://en.wikipedia.org/wiki/Automated_theorem_proving
- TTPrograms 12y agoAutomated proof checking software has been around for a while, and they don't really require any capacity I'd describe as 'AI' as they simply verify logic: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking The trouble is that writing a proof in a format amenable to this verification is harder and much more tedious than writing it for a paper
- mhomde 12y agoyes, that's why I think something different than Automated proof checking for solving advanced theorems, you need to have an AI that can take "creative leaps" and break down proofs down to something humans can understand, and not just verify existing rules
- deepsun 12y agoSome time ago I started designing a system that would convert between automated checkers syntax and some simplified human-readable English. But failed, once realized the problem is bigger than me. Here I just want to encourage anyone who thinks he's a good programmer to develop such a system. It would be extremely useful for education as well: students would get a tool that explains complex proofs, and professors would give assignments to put a theorem into the system (if student is able to enter the theorem into the system, then he/she definitely understands it up to the very foundations). The main problem to solve is good UX, not the math. They who manage to make the system, the new verified Wikipedia for Math, would have their names inscribed for eternity, because Math is eternal.
- lambdasgr 12y agoHe probably should try to use Coq proof assistant. If Coq proves his proof, then mostly like it's correct. Of course, it's easier to say than to do, not a trivial work, and he's the only one who can do it, since he's the only one who can understand the proof. But if he indeed able to write the entire proof in Coq, then I'm sure at that point, his proof will be much cleaner as well. Then again, this will never happen.
- wetmore 12y agoThat is like a complete no-go. It took something like 6 years[0] to formalize the proof of Feit-Thomson, one of the first "long" proofs in group theory, and that was done by experts who understood both Coq and the proof. In the time it would take him to write the proof in Coq, dozens of mathematicians could learn the theory and independently verify it. [0] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/
- polarix 12y agoSure. But no dozens of mathematicians are stepping up to take the roughly half a year (and novice-like zen) he anticipates it requiring to understand the proof. So if he wants it to happen: do a lecture series, or programmatize the proof, or write an expanded walkthrough book series to explain it in less condensed form. Or just complain to new scientist and see if any new folks decide to pick up the torch, I guess.
- lambdasgr 12y ago"Oh my god, it's such a big project, nobody should do it alone". It's very obvious, isn't it? 500+ pages of abstract proofs need to be expressed into some kind of programming language. Not to mention, the worst case is that he doesn't even know what coq is, or have never used a programming language (probably just TeX, since he's mathematician) and will take him sometime to pick it up, and then learn how to express his idea using it, etc ... Look at the linux kernel we have right now, let's go back to early 90s, and should we tell Linus not to do it because it's so big? And did it end up Linus doing it all alone himself? Coq is certainly not a short term solution, but definitely a valid one if no one else wants to read his proof, and it's very important for him validate it. The reason I bring Coq up is that in general, I do feel proving things in maths is very much like writing a program in a programming language. Maybe the 500+ pages of proof is like a spaghetti code, refactoring might make it more readable, or more clear, so people are more likely to study it. Or the 500+ pages of proof is very elegantly constructed, just need someone to appreciate it. Coq can certain help in both cases. But then is it worth it for him to do it? That's really he's judgement call based on how important the proof is, what he see he can get out of this, etc. Remember that line from the article you quoted: "Fun ~enormous!"
- jackmaney 12y ago> If nobody understands a mathematical proof, does it count? Nope. That's the social aspect of mathematics: your proofs have to be comprehensible and considered to be correct by those in the mathematical community that read them (at least peer review) before they're accepted.
- mathattack 12y agoA professor once defined a proof as "That which is convincing", and we were free to say, "I am not convinced" While the topic being proven may be technically correct, the act of proving is a social act. The formal notation just makes this more precise than human language.
- Retra 12y agoProof is "that which is convincing to a fair and rational mind." It should compel a rational actor into the verifiable mitigation of some risk. This particular fuss is one of the side effects of mathematicians' failing to properly adopt computers into their process. One of these days we will not accept a proof unless it is computer verified, and there will be no social aspect to it. It should not matter if your proof is 10,000 pages if a computer can follow it.
- lacker 12y agoIt is still better to have a clean 1-page proof. There is no direct value for proving a theorem. Mathematics is nice because it's useful for further mathematics, useful for real-world applications, and beautiful. A 10,000 page proof that only a computer can follow is none of these things.
- Retra 12y agoIt is the second thing. Anyway, the number of pages is arbitrary -- it is a function of your language and terminology. Not every proof can be simplified, so surely there exist useful proofs that require 10,000 pages minimum for a given finite set of terms. So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.
- mathattack 12y agoHe has also criticised the rest of the community for not studying his work in detail, and says most other mathematicians are "simply not qualified" to issue a definitive statement on the proof unless they start from the very basics of his theory. Math this advanced can be very hard to follow. There are more incentives to do original work than check someone else's, especially when they have drifted far off the mainstream. It takes a special arrogance to say, "You have to come to me" and then be angry when nobody follows.
- ObviousScience 12y ago> "simply not qualified" to issue a definitive statement on the proof unless they start from the very basics of his theory How is it arrogant to say people need to study the whole branch, from the beginning, rather than just try to cherry pick a few advanced parts of it, if he really did come up with a substantially new branch? That sounds more like practicality than arrogance to me.
- sukilot 12y agoIt is quite a risk to spend a year or more in dedicated study before seeing any results whatsoever interesting. Why are there no basic lemmas in this new theory?
- mathattack 12y agoThis requires years of in-depth study without guideposts. If it's a brand new field, help people along the way. (Write books, explain the concepts globally, create projects for Phds, etc.)
- ObviousScience 12y agoAs I recall, he's personally tutoring at least one other mathematician, doing lectures, etc -- that is, I'm pretty sure he's doing the last two of your suggestions. Writing books, of course, is a multi-year process in addition to his other work. The problem is that they're disqualifying people who study under him in this manner from verifying his work, which seems like something of a catch-22.
- sramsay 12y agoI understand the trouble, but in this case it seems like the trouble might well be worth it. If the ABC conjecture is proven, the consequences are quite substantial: http://en.wikipedia.org/wiki/Abc_conjecture#Some_consequences http://en.wikipedia.org/wiki/Abc_conjecture#Some_consequence...
- fsakura 12y agoOn a side note: What is the Latex font name used in this document (Published by Shinichi Mochizuki)? http://www.kurims.kyoto-u.ac.jp/~motizuki/IUTeich%20Verification%20Report%202014-12.pdf http://www.kurims.kyoto-u.ac.jp/~motizuki/IUTeich%20Verifica... Looks really nice to eye.
- deleted 12y ago[deleted]
- alex-g 12y agoComputer Modern http://en.wikipedia.org/wiki/Computer_Modern http://en.wikipedia.org/wiki/Computer_Modern
- sshaginyan 12y agoGuys. This is my problem with reading white papers. People use notations and assumptions which I am not familiar with. Hence, I have to go decipher what people are trying to day. There needs to be a course for math notation. Is there a book or a online course I can take to familiarize myself with math as a language.
- eru 12y agoThey use (slighly) different notions in different parts of mathematics. And usually, it's not just the notation that's difficult, but the concepts themselves. In general, you are best off studying introductory texts to the topics you are interested. You will pick up the notation.
- deleted 12y ago[deleted]
- Intermernet 12y agoWrong thread. You want this one https://news.ycombinator.com/item?id=8865316 https://news.ycombinator.com/item?id=8865316
- chocolateboy 12y agos/anger/frustration/
- cromwellian 12y agoIn other news, engineers refuse to do a code review of a pull request with 1 million lines of code changed. As has been mentioned elsewhere, the issue may be the "code bomb" nature of the way the paper was published, and if it was released in even smaller chunks, it may have garnered more analysis.
- MrBra 12y ago"An overview of Inter-universal Teichmüller Theory and [...] how we can begin to understand this theory": http://www.quora.com/Joseph-Heavner/Posts/An-overview-of-Inter-universal-Teichm%C3%BCller-Theory-and-Shinichi-Mochizukis-proof-of-the-ABC-Conjecture-along-with-th http://www.quora.com/Joseph-Heavner/Posts/An-overview-of-Int... Also, from an anonymous post on 4chan @ http://boards.4chan.org/sci/thread/6931488/are-you-ready-for-interuniversal-mellin-transform#p6956712 http://boards.4chan.org/sci/thread/6931488/are-you-ready-for... : "How to understand IUTeich from the bottom up: - Algebra (Israel Gelfand) - The Method of Coordinates (Israel Gelfand) - How to Prove It: A Structured Approach (Daniel Velleman) - Kiselev's Geometry - Planimetry and Stereometry - Trigonometry (Israel Gelfand) - What Is Mathematics? An Elementary Approach to Ideas and Methods (Richard Courant) - A Course of Pure Mathematics (G.H. Hardy) - Linear Algebra (Kenneth Hoffman and Ray Kunze) - Elementary Differential Equations (William Boyce and Richard DiPrima) - Topology (James Munkres) - Calculus On Manifolds (Michael Spivak) - Principles of Mathematical Analysis (Walter Rudin) - Real and Complex Analysis (Walter Rudin) - Functional Analysis (Walter Rudin) - Partial Differential Equations (Lawrence Evans) - Analysis On Manifolds (James Munkres) - Abstract Algebra (David Dummit and Richard Foote) - Algebraic Topology (Allen Hatcher) - Introduction to Smooth Manifolds (John Lee) - Foundations of Differentiable Manifolds and Lie Groups - (Frank Warner) - Galois Theory (Harold Edwards) - Linear Representations of Finite Groups (Jean-Pierre Serre and Leonhard Scott) - A Classical Introduction to Modern Number Theory (Kenneth Ireland and Michael Rosen) - Introduction to Analytic Number Theory (Tom Apostol) - Modular Functions and Dirichlet Series in Number Theory (Tom Apostol) - Riemannian geometry (Peter Petersen) - The Theory of the Riemann Zeta-Function (Edward Charles Titchmarsh) - An Introduction to Teichmüller Spaces (Yoichi Imayoshi and Masahiko Taniguchi) - A Course in p-adic Analysis (Alain Robert) - Foundations of p-Adic Teichmuller Theory (Shinichi Mochizuki) - Mochizuki's papers at http://www.kurims.kyoto-u.ac.jp/~motizuki/papers-english.html http://www.kurims.kyoto-u.ac.jp/~motizuki/papers-english.htm... "
- tottenhm 12y ago> If nobody understands a mathematical proof, does it count? That depends. If it deals with integers, yes. If it deals with real numbers, no.
- whitten 12y agoboo. hiss. (and actually a clever reply tottenhm)