I 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.
Graffiti 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.
You know this reminds me of A Deepness in the Sky where groups of "focused" humans with the aid of computers had to be guided toward what's "interesting" to keep them from going into loops by other normal humans.
> Can all interesting proofs be built with human-friendly steps?
That is a marvelous question. How would one even quantify "human-friendly"?
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),
Indeed, the problem is you have to walk up and down various abstract constructions that define what a human mathematician is.
> Can all interesting proofs be built with human-friendly steps? Maybe that's why we haven't worked out P and NP.
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.
Even people can't always produce human friendly proofs. There's Shinichi Mochizuki who might have proven the ABC conjecture but no one can confirm it because he created a whole method and set of techniques/theories that no one else really gets. This is a person creating a branch so dense that it's taken 3 years and we still haven't determined if it's wrong.
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.
Usually in math we talk about a statement being "independent", which means that it is compatible with the axioms for it to be true as well as false.
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.
If P=NP is independent, then we already know that a complete search for a polynomial algorithm for 3SAT will fail (because if there were such an algorithm it would prove P=NP, so it wouldn't be independent). Adding P=NP as an axiom doesn't change this; instead it effectively augments the system with certain "nonstandard" natural numbers (which are larger than any concretely describable term but "look" like regular natural numbers from within the system), and this mythical polynomial algorithm for 3SAT will have nonstandard length (meaning for pratical purposes that it is infinitely long).
> If P=NP is independent, then we already know that a complete search for a polynomial algorithm for 3SAT will fail
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."
p=np is a well-posed question, so clearly it must have an answer. We can't just make it an axiom.
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.
Just because a question is well-posed doesn't mean it must be provable or disprovable. Consistency of ZFC is also a perfectly well-posed question with a finite answer (if one exists), but we know it is impossible to prove regardless. I don't think we can exclude independence as an option for any currently open question without actually proving or disproving it. (Of course, most mathematicians don't really think that P=NP will turn out to be independent, any more than the Riemann hypothesis or Goldbach's conjecture, but we don't know for sure.)
I'm trying to wrap my head around how P=NP could not have an answer, and I am not having much success. It could be that I am not educated enough to understand.
Notwithstanding that, I don't see how any of this relates to my original question.
You're misunderstanding something. P=NP is about whether two sets are equal. If it's "undecidable" or "independent", then ZFC is consistent with either P=NP or P \neq NP.
Independent doesn't sound like the same thing as undecidable.
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).
Yes, 'undecidable' is used for a similar class of mathematical problems. For example, the continuum hypothesis - another question about an equality of sets - is undecidable in ZFC. This notion is strongly related to undecidability on Turing machines (possibly equivalent, depending on how you look at it).
They are intimately related. If you look at how Gödel's incompleteness theorem is stated, the existence of "effective procedures" (I.e. Computable functions) figures in intimately.
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.
> I think one of the greatest difficulties in completely automated mathematics would be the discovery of mostly those things which are interesting.
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".
Thanks for the link. I'm also working on this. Would love to chat with you (or anybody else reading this), please contact me: juan at juan dot com dot uy
Your 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".
An easy-to-imagine scenario is: a program which solves every NP problem we give it in P time, but we don't understand how or why it works. With bounded probability of error, this would constitute a proof of P=NP. But the program might elude human understanding.
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.
> 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.
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?
Who's the "you" in your question? Humans wouldn't be able to tell; that's the whole point. A computer might "figure out" that it's easier to give us something that looks like what we're looking for instead of what we're actually looking for.
> A computer might "figure out" that it's easier to give us something that looks like what we're looking for instead of what we're actually looking for.
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.
Well, that's why I put "figure out" in quotes; it would probably be closer to an evolutionary process. Some instance of an algorithm stumbles onto a simple process for generating proofs that it deems okay to submit, and never gets its power yanked for doing so because the algorithm fakes us out.
It's a system of evolution: for the software to survive it must be useful, self-fulfilling, or a combination.
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.
Excellent point. But can this be extended to abstract mathematics as well i.e. software reasoning able to gain mathematical insights automatically? That would be very interesting indeed.
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?
This is the type of question that quickly runs into problems wrt incompleteness, but there are a few key points that show that there are infinitely many theorems
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.
Since each theorem has a Gödel-number, there must be a function f(x) -> {0,1} where, when x is the number of an 'interesting' theorem, f(x) is 1, and otherwise it is 0. So, we just need to find this function (or rather, its Gödel number) and then we can iteratively feed all the integers to it, translating the interesting ones back into theorems.
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:
You just defined a subset of the natural numbers, and asserted it has a Godel number. Sorry, there are uncountably many subsets of natural numbers and countably many Godel numbers, so there is no guarantee that this is possible. More subtly, you can consider many "natural" classes of functions, such as computable functions, recursively enumerable functions, etc. and for each such enumeration there will be a "natural" function that escapes the class. Functions to do with definability or (in this case) 'interestingness' are especially susceptible to this. See also "Tarski's theorem on the undefinability of truth".
You can always enumerate all theorems (i.e. all provable sentences of formal logic) by systematically applying rules of inference to axioms and previously obtained theorems. You only need axioms to be recursively enumerable. Though most theorems obtained this way are going to be dull tautologies like "every even number is even"; the hard part here is finding out which theorems are interesting. And it's prohibitively expensive computationally; in fact, it needs infinite memory to store all the previously obtained sentences.
The theorem space is infinite. The theorem space that is learnable in a single human lifetime is probably finite, but we are not anywhere near having explored it.
> Well, except that it simply can not be social recommendation. Math is too big, and interesting results too sparse for that.
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?
That's because there are only a few millions (or is it billions? not really an important difference) of books available, while we don't have names for the kind of number of proofs available in any mathematical system (when they are finite, it is).
You can lump all humans on the same group, your AI just won't find anything interesting for the group by a random search.
>...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.
"pay"?
Imagine this: you produce a silicon cube embedded with logic circuits powered through the photovoltaic effect and then eject it into space.
> 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?
> 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.
Some portion of what is deemed important arises from the interaction between mathematics and physics. It would be fascinating to automate the invention of new mathematical structures and then have a post-human physicist try to apply these new structures.
The main thing I'd say is that either the quality of "creativity" is something that effectively duplicates (or even extends) the human notion of creativity or it's something arbitrary that there could be a way for us to care about.
Even if someone formulated an apparently human-independent mathematical statement of "interesting", you would still the human judgment that this was credible.
I had written what now seems to me to be an unnecessarily long response to this, but along the way I think I thought of an example to demonstrate my point:
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).
Computers 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.
Almost 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.
Loved 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."
No, 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.
You'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.
If we stuck with tried and true we'd all be writing in assembly and Cobol. I remember what it was like in 1981, thankfully we continuously move forward. Building a bridge on the other hand is only barely different than the Romans in many ways.
Depends on what you mean by that, I guess. There is no such thing as software engineering. If there is software that can do what you want it to do, just use it. You don't need to build it again, like you'd have to do with a bridge.
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.
No software ever does exactly what we want it to do, because we are all different and have different demands on our programs. Even the author of a program is usually never truly "finished" with their program, and always find new things to add or behaviors to tweak. That's why software engineering is a thing.
I'd guess at some point computers will become a literal brain prosthetic - instead of writing code by tapping words with your fingers, you'll have the cognitive enhancement offered by a programmable computing machine integrated directly with your conscious awareness.
Wow, ok then. What I love about the quote is the notion that a practitioner who is "great" can do something that no one has ever done before while acknowledging that you can be "good" with just the skills to re-do what has been done before.
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.
Human 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.
Bascially, 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.
The 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.
How 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.
I 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.
I 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.
While 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.
That 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.
If 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.
Chess 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.
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.