9 ms·
Post-human mathematics
- jessriedel 11y agoCan someone give a better summary of the author's points? The abstract gives an intro, but not much else.
- momo1319 11y agoFull text is here: http://arxiv.org/pdf/1308.4678v1.pdf http://arxiv.org/pdf/1308.4678v1.pdf
- dlsx 11y agoHe basically just elaborates on those points and poses more questions. The whole paper can be summed up in the abstract or, even one sentence; If computers become intelligent enough to become creative, then perhaps they may come up with a better way to comprehend digital units. This paper is junk TBH. There is no math, just posing questions. I could do this all day with theories on A.I. but only until you apply some application to the A.I. do I become interested, otherwise you might as well be writing hollywood fiction.
- waterlesscloud 11y agoBascially, it's the rather common idea that a computer may not reason in ways that are easily comprehensible to human minds. There's not much depth to the paper beyond that.
- jk4930 11y agoHuman brains are severely limited so the mathematics they invent is severely limited and everything new are small, understandable steps that build on huge piles of proven mathematics. A computer can create entirely new huge, complex ideas we wouldn't understand because they don't depend on making small steps.
- sevzi7 11y agoMy brain is much better and doesn't need computer. But I'm doing Java multicore intelligence.
- anentropic 11y agois there any evidence that a computer has ever created a new 'idea' ?
- bendbro 11y agoIf human generated books, artwork, and behavior qualify as new ideas, why don't computer generated things also qualify? https://www.youtube.com/watch?v=tCPzYM7B338 https://www.youtube.com/watch?v=tCPzYM7B338 https://www.youtube.com/watch?v=Cbb08ifTzUk https://www.youtube.com/watch?v=Cbb08ifTzUk
- whatshisface 11y agoI think one of the greatest difficulties in completely automated mathematics would be the discovery of mostly those things which are interesting. If computer mathematics is ever to diverge from human thinking, someone must pay to keep the lights on. Since nobody would pay for random points in theorem-space, it must have some way of figuring out what the human brains down at the breaker box actually want. This to me looks a lot like the problem of computer automated storytelling or even art. Also, I don't think the alien-ness of computer proofs is a given. Perhaps someday some psychologist or philosopher might work out exactly what our cognition likes to work with, upon which time you could write a proof compiler that outputted those things. That raises and interesting question. Can all interesting proofs be built with human-friendly steps? Maybe that's why we haven't worked out P and NP.
- RobertoG 11y agoYour comment brings to memory the book 'Diaspora' by Greg Egan. There is in the novel some mathematical space that represent all the possible theorems, but it cannot be mined automatically because it need some conscious being deciding what problems are "interesting".
- msane 11y agoGreat book, a favorite.
- vinceguidry 11y ago> Maybe that's why we haven't worked out P and NP. Great exposition on the state of the art of the P=NP problem https://www.quora.com/What-were-the-best-attempts-to-solve-the-P-vs-NP-problem https://www.quora.com/What-were-the-best-attempts-to-solve-t...
- sanxiyn 11y agoGraffiti is a computer program which makes conjectures in graph theory, written by Siemion Fajtlowicz. Research on conjectures produced by Graffiti has led to over 60 publications by other mathematicians. https://en.wikipedia.org/wiki/Graffiti_(program) https://en.wikipedia.org/wiki/Graffiti_(program)
- marcelluspye 11y ago> Is there a structure to mathematics which is independent of the human brain? I would venture to say "no". I don't think humans will ever have no place in mathematics, because the problems we deem "important" are often relatively arbitrary. If a "post-human mathematician" starts spewing out thousands of pages of mathematics a second, all in a form only a computer can understand, no one will care. If a computer fells a tree in the woods, it doesn't make a sound. I wouldn't discount the possibility, though, that a future "creative" computer manages to produce a proof indecipherable to humans of a theorem we care about, at which point I think there will be quite a perturbation in the mathematical community. If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved?
- Retra 11y agoThe problem will be solved when any other problems that depend on its solution become solvable.
- johncolanduoni 11y ago> If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved? We've already seen this play out to a certain degree with the proof of the four color theorem[1]. Basically, the problem was reduced to checking about 2000 specific graphs (the checked property was more complex than simple colorability). The reduction part was very complex but still checked by humans, but checking the ~2000 graphs was a computationally expensive process that took computers thousands of hours to complete, which was completely infeasible for direct human verification. There was a lot of controversy over whether this counted as a proof. Since then the proof has been simplified to 600 special cases and run through a proper proof assistant (Coq), so it is now pretty widely accepted as proved. It's not quite analogous since the core of the proof was still human created and checked, and the basic form of the computer generated portions was well understood (i.e. the kinds of steps they used). There is some extra doubt involved when this is not the case, since it's possible the computer came up with a novel proof of inconsistency if we don't know at all how the individual parts of the proof work. [1]: https://en.wikipedia.org/wiki/Four_color_theorem https://en.wikipedia.org/wiki/Four_color_theorem
- Strilanc 11y agoAlmost all of this paper is dedicated to discussing whether or not computers can be "creative". Then it mentions in passing that computer-discovered theorems may be long and impenetrable (even if they are profound). I guess I was expecting some attempted concrete task definitions of creativity, such as "finds and proves statements with many useful implications and applications", and discussion of how well existing theorem provers do at those kinds of tasks. But instead of the "how might we achieve this, and what will change?" paper I was hoping for, this is more of an "are we special?" paper.
- bweitzman 11y agoThe author touches upon creativity being related to making educated guesses about how to proceed with a proof.
- api 11y agoThey'd probably be more... computational: http://www.amazon.com/dp/1579550088/?tag=googhydr-20&hvadid=48305385595&hvpos=1t1&hvexid=&hvnetw=g&hvrand=2373967073518921741&hvpone=28.65&hvptwo=&hvqmt=b&hvdev=c&ref=pd_sl_4j8ledlqpp_b http://www.amazon.com/dp/1579550088/?tag=googhydr-20&hvadid=...
- netcan 11y agoComputers are used more and more but do not play a creative role It's always difficult to get concepts straight when talking about any of these AI-ish questions. The thing that we describe before the fact as "intelligence" is generally stuff we can't imagine mechanizing. Once it is mechanized, and we see the mechanic we don't really like to call it AI. I think it's the same issue for "creative." When humans do mathematics they look for theorems that are interesting intuitively. We don't really understand what this intuition is. If a computer does it, say along the way to solving some other problem, we will be able to look into the mechanic and it probably won't seem like intuition to us.
- sevzi7 11y agoI'm already doing this with Java multicore. Is Java multicore human? No.
- cLeEOGPw 11y agoAs Mike Tyson said "a computer might win a chess match, but he would lose in boxing ring".
- nicklaf 11y agoThat doesn't even make sense. If we're going to compare apples to apples, you'll either have to remove the human's brain from his body and place it in the ring with the computer, or give the computer a proper body. I don't see the human winning in either case.
- dazmax 11y agoIf the rules are that you have to use a human body, good luck computer. Considering what our brains were designed for, you could make the argument that chess is just as unfairly biased in a computer's favor as controlling a human body in a boxing match is in the human brain's favor.
- gohrt 11y agoChess was invented long before computer. It's not unfairly biased; it happens to be a particular human endeavor that computers can (relatively) easily be made much better at.
- YeGoblynQueenne 11y agoI believe what the great thinker is saying is that he is smarter than a computer because he can bash its blinking lights out.
- tux1968 11y agoA tank would win in the boxking ring, but it would lose a chess match.
- PavleMiha 11y agoYou could put a computer inside of a tank and win both, which is pretty much AGI.
- zitterbewegung 11y agoFor mechanical theorem proving there is ACL2 which integrates machine learning into the system. See http://arxiv.org/abs/1404.3034 http://arxiv.org/abs/1404.3034 also Coq has machine learning add ons http://arxiv.org/abs/1410.5467 http://arxiv.org/abs/1410.5467
- nicklaf 11y agoThat is quite interesting, thanks!
- ChuckMcM 11y agoLoved this quote -- "Note, by the way, that a great mathematician is one who does something new, not one who is good at doing again things that have been done before." Same can be said of engineers.
- no_wave 11y agoI think the opposite is true of engineers.
- technofire 11y agoNo, precisely the opposite should be said of engineers. Engineering is about reusing well-known techniques to achieve repeatable, predictable results whose timelines can be estimated. Engineering is not art. When civil engineers build new buildings or bridges (and I'm talking about your common building or bridge, not some iconic project), do they try to innovate and undertake to do things in some new-fangled way every time? No, because this would be extremely costly and dangerous and would render useless much of the past work that's been done testing materials and loads and so forth. When a method is known of constructing a bridge or an overpass that is both safe and economical, a good engineer should just keep doing that, with perhaps some adaption as appropriate on a case-by-case basis. If software developers would stick with tried-and-true tools instead of inventing new frameworks to solve the same old problems and immediately obsoleting the "old" way of doing things each time, we'd have much less legacy code and likely would be much better at estimating software development tasks, and wouldn't have to solve the same problems over and over again.
- joslin01 11y agoYou're right about traditional engineers whose work has been going on for quite some time now. We more-or-less figured out the "correct" way to build a bridge or an on-ramp or most anything physical and tangible. However, your last point is not valid because you're under the fallacy we ever got the framework problem "correct". Who is to say that Django is better than RoR or visa-versa? Software is still a very new craft; you can't say that about masonry. Actually your fallacy stems even further. You're assuming software is predictable. There's degrees of predictability, but most programming starts out as a trek into the unknown. Sure, you might grab a familiar lamp like [Framework X] to shed light along the way, but really you don't know for sure what you're in for. If you did (or do), then you probably spent an insane amount of time spec'ing everything out perfectly. I have no problem with this, but there's even some dissonance between spec & code and the further out that spec gets, the greater the dissonance. Software will always be kinda crazy in my opinion, but I reckon we're getting better with these agile approaches that embrace the unpredictability. In the TDD approach, you have to come up with tests first. This can usually give the programmer or architect a much clearer picture than "step 1: build web app" which will transfer over into their estimates.
- TerryADavis 11y agoThere is human league music. There is angel league music. http://www.templeos.org/Wb/Home/Wb2/Hymns.html http://www.templeos.org/Wb/Home/Wb2/Hymns.html
- tianlins 11y agoI think automated theorem proving replaces the "search function" of a mathematician. But there is another part, which seems to be more important, is the creative insights. For example, inferring and conjecturing a theorem from few "data points". Machines at the moment do not have such capability yet.
- zenogais 11y agoI think creativity is more than just inference from limited data (which computers can do also). It has to do with either discovering a way to connect two or more seemingly unconnected things or discovering a new means by which to connect two or more things. Mechanically churning through a pre-defined possibility space doesn't seem like a sure-fire way to produce either of these effects. Though it is, no doubt, a great way to generate proofs that were previously prohibitively expensive to produce.
- spooningtamarin 11y agohttps://agtb.wordpress.com/2012/04/01/automatic-proof-for-reimanns-hypothesis/ https://agtb.wordpress.com/2012/04/01/automatic-proof-for-re... Love this one as a look into the future.
- deleted 11y ago[deleted]
- nemo1618 11y ago>The ability to speak was clearly favored by evolution, and the >same might be said of the ability to count from 1 to 10. Actually: https://en.wikipedia.org/wiki/Pirah%C3%A3_language#Pirah.C3.A3_and_linguistic_relativity https://en.wikipedia.org/wiki/Pirah%C3%A3_language#Pirah.C3....
- taber 11y agoThe technology of mathematics is not theorems. Think of theorems like unit tests: no matter what framework you use to get a result, it should match the corresponding results that other approaches have yielded. The technology of mathematics is words. Words that define the barriers between abstract objects and their different properties. The set of words that a mathematician uses to approach a problem is where progress is made. Until a computer can conceptualize a problem outside of the words used to describe it, it will never mimic this aspect of abstract thought.
- underlings 11y agoSo I guess this is it then. If people were wondering about what comes after "postmodern" it's probably: Posthuman
- eveningcoffee 11y agoyou please enter digital certificate of virginity of grandmother , or some such nonsense. How did they get this kind of spam into arxiv.org?
- tvural 11y agoHow human mathematicians decide that a problem is "important" is not as arbitrary as people seem to think. The work mathematicians choose to do can be heavily influenced by fashion, but in general, a problem is important if its solution would give insight into many other important, unsolved problems. Given this definition, it wouldn't be difficult to get the computer's definition of an interesting problem to align with ours.
- golergka 11y agoWhile the theme seems interesting, I found the article itself pretty underwhelming. It just describes the current state of affairs and then goes into hypotheticals with less precision and imagination than many sci-fi authors before.