Post-human mathematics
arxiv.org
arxiv.org
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.
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".
Great exposition on the state of the art of the P=NP problem
https://www.quora.com/What-were-the-best-attempts-to-solve-t...
As a mathematician, that seems like my idea of a dystopia. Shiver.
On the other hand, assuming that it doesn't go off and develop sentience on its own, how would a computer figure out such a thing? Assuming that it is programmed in such a way that it only produces correct proofs of (possibly uninteresting) theorems, there'll be no way for it to produce those 'easier' deceptitheorems in order to be rewarded for doing so.
Artificial intelligence will go through its own evolutionary path, and it already is. Machines already build themselves: software is used to design their own architecture.
There are already research labs that use machine learning to design better processors.
So, something like a recommendation algorithm? Netflix for Mathematicians?
I think that almost anyone pre-Amazon would have said that an Amazon-style recommendation engine was impossible. (I pick Amazon as the one with which I'm most familiar, but substitute your favourite.) Amazon groups me with people who read similar books, and can only do so after it knows a bit about what books I read; why couldn't an engine group me with other people who share my mathematical interests, perhaps determined by mining my publication record (or just by asking me), and recommend on that 'social' basis?
You can lump all humans on the same group, your AI just won't find anything interesting for the group by a random search.
P and NP is a very interesting case, since there has been some meta-mathematical results that attempt to rule out certain methods of proof as being capable of producing a proof of it[1]. However, I don't think we have a good characterization of "human-friendly steps" that we could conceivably use to rule out the existence of such a proof completely.
There's also the controversial Computer Assisted Proof. Which I think is a lesser version of completely computer generated proofs where there's the question of procedural errors and the difficulty of checking for them.
If p=np were indeed independent, we could make it an axiom. Then we could do a complete search for a polynomial algorithm for 3sat, and we would be guaranteed to succeed.
Since computing is somewhat a model of the physical world, something like this would surprise me. It seems like computing being modeled on the physical world, the model must contain the answer to the question. But who knows.
However, the thought occurred to me that perhaps p=np could reduce to some undecidable problem (in the halting problem-sense). In that case, solving p=np would be impossible. But we could prove that it's impossible, and the issue would be resolved.
I'm not sure whether this scenario makes any sense. That's why I asked the question.
Notwithstanding that, I don't see how any of this relates to my original question.
Given a program P, it is undecidable whether that program will halt. There is an answer: P either halts or it doesn't. There is just no way to find out (in general).
A good overview of this in a reasonably accessible format can be found here: http://www.scottaaronson.com/blog/?p=710
The same author wrote a good treatment of the implications of the undecidability of P=NP: http://www.scottaaronson.com/papers/pnp.pdf
Scott Aaronson is probably one of the best at explaining theoretical computer science, if you're interested in these topics you should follow his blog.
A search for a provably polynomial algorithm will fail, but that doesn't mean that an unprovably polynomial time algorithm couldn't exist. We might come up with strong arguments for why a particular algorithm would be polynomial in practice. Still, I'd say "independent but false" is more likely than "independent but true."
I've been investigating this exact issue recently, and you're right.
To me the most promising approach seems to be that of "artificial curiosity", where some traditional AI algorithm is rewarded/biased by an "interestingness measure". These are usually based on subjective information, e.g. how "surprising" an observation is, given what we know.
The key seems to be a balancing act between simplicity and complexity: things which are too simple may be trivial or obvious, and therefore uninteresting; things which are too complex may be unintelligible or arbitrary, and therefore uninteresting. This phenomenon is known in psychology as the "Wundt curve".
For anyone who's interested, I've got an ever-growing Bibtex file at http://chriswarbo.net/git/writing/branches/master/Bibtex.bib which contains many references on this topic (all mixed up with completely unrelated stuff though!).
"pay"?
Imagine this: you produce a silicon cube embedded with logic circuits powered through the photovoltaic effect and then eject it into space.
Question: Given an arbitrary powerful computer, is the nature of mathematics such that in principle we could exhaust the points in theorem space by brute force?
E.g. is there in principle a finite amount of math?
For any given statement P and any given theorem T, P OR T is a theorem, meaning you can generate infinitely many theorems from one.
More worryingly, there are infinitely many theorems that are true but impossible to prove. From Gödel's first incompleteness theorem, we know at least one such theorem must exist. Any theorem of the form Unprovable AND TRUE can be proved only if you can prove the unprovable theorem.
From a more general perspective, it's worth remembering that theorems can always be described as a finitely-long string of symbols in some formal logic system, and so running out of theorems to try and prove is like running out of strings.
This job is made much easier by the fact that the proof of this 'interestingness' theorem has a Gödel-number of its own; call it F. And, proving that something is interesting is obviously also interesting. So, just find the situation where:
f(F) = 1
I'll collect my Fields medal later, thanks.
But isn't 'interest' subjective?
EDIT: "determined by" is probably more precise than "decided by" (determination is not necessarily conscious or explicit)
Presumably it means something more like "different (rational, honest, omnipotent) respondents might produce different answers."
Would a machine learning approach be possible? For example, has anyone built a generative model, trained from theorems (and proofs) from math texts or formalized versions thereof?
> Can all interesting proofs be built with human-friendly steps?
Presumably in much the same manner as the Turing test, by showing it to humans (well, human mathematicians) and letting them judge it. In fact, one can imagine a Turing test for ATPs in which they have to produce proofs that will fool a referee. I can't decide whether I think that this would be harder (because who, including they themselves, knows how human mathematicians mentally explore their subject?), or easier (because of the much more specialised domain knowledge), than the full Turing test.
> (because who, including they themselves, knows how human mathematicians mentally explore their subject?), or easier (because of the much more specialised domain knowledge),
Babai's graph isomorphism in quasi-polynomial time proof is approaching this. The algorithm involves handling one special case specially, so it's still within reach of human understanding. But you could imagine an algorithm that handled 1000, or a billion special cases specially, that would be beyond human understanding.
Babai's algorithm is constructed by a human, so there is an intuition behind it. But if such an algorithm arose through genetic programming, I can imagine not ever being able to understand it.
It's possible that factoring is similar: there exists an algorithm for factoring efficiently that involves a large number of special cases. Already, the best algorithms are damn complicated. If the minimum necessary algorithm is large enough, it might forever elude human comprehension.
This is the case with the four-colour theorem's proof. Folks got quite philosophical after that one was published.
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?
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.
How would this be so? The sheer length of the proof rendering it unverifiable in a human lifespan?
Shinichi Mochizuki spent several years compiling a large body of work which he calls "Inter-Universal Teichmuller Theory" which which implies a number of important results in number theory, algebraic geometry, and other areas (if I understand the gist of it). However, he has run into a wall in the mathematical community in that almost no one wants to spend the time to try to understand what he wrote (I believe he said he believes it would take someone well-versed in the field around 6 months of study to get a grasp of it).
If a human could produce enough work in sufficiently dense terms that other mathematicians don't want to touch it, I can imagine a computer could generate exponentially more work in a much less human-readable format than Mochizuki (albeit formally correct).
Even if someone formulated an apparently human-independent mathematical statement of "interesting", you would still the human judgment that this was credible.
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.
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.
Same can be said of engineers.
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.
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.
I am currently developing something very new, and the road to where I want to go is plastered with new concepts I invented. Half of what I need to do is inventing new mathematics as well (in the form of making up new definitions, theorems, and proofs of these theorems) so that I know what exactly my software is doing.
Will a computer one day be able to do what I am doing? I definitely hope so. In fact I'd love to have a computer at my side right now that could prove this freaking theorem I am working on right now. I am pretty sure it is true, but I will need 2 or 3 more days until I am really sure. It would be nice if a computer could tell me in a second if it is true (or not), together with a proof.
I do separate in my mind engineers that can take a blank sheet of paper and create something completely new, and engineers can really only start from something that already is, or a close to what they want, and morph it into something else.
>The ability to speak was clearly favored by evolution, and the
>same might be said of the ability to count from 1 to 10.
https://www.youtube.com/watch?v=tCPzYM7B338 https://www.youtube.com/watch?v=Cbb08ifTzUk
Love this one as a look into the future.
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.
http://www.amazon.com/dp/1579550088/?tag=googhydr-20&hvadid=...
How did they get this kind of spam into arxiv.org?
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.
Posthuman
I don't see the human winning in either case.
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.