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.

https://en.wikipedia.org/wiki/Graffiti_(program)

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"?

> 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.

[1]: https://en.wikipedia.org/wiki/Natural_proof

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.

https://en.wikipedia.org/wiki/Computer-assisted_proof

Could P=NP be undecidable?

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.

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.

> 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".

You may enjoy Automated Theory Formation in Pure Mathematics (2012).

https://books.google.com/books?id=qJrSBwAAQBAJ

Thanks, I've not managed to get my hands on the book but have read a few snippets. I've certainly read as many of Colton's papers as I can find :)

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!).

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".

Great book, a favorite.

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.

> But you could imagine an algorithm that handled 1000, or a billion special cases specially, that would be beyond human understanding.

This is the case with the four-colour theorem's proof. Folks got quite philosophical after that one was published.

> 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?

> 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-t...

Wouldn't it be a lot easier to present theorems that look interesting and look true, but are not, and are not trivially simple to verify?

No? How would you even tell?

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.

The hypothesis class that the ML algorithm works within is proofs, checkable by something like Coq, so that can't actually be done.

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.

>> "...random points in theorem-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?

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:

    f(F) = 1

and we're done!

I'll collect my Fields medal later, thanks.

Your condition `f(F) = 1` doesn't seem to do anything to distinguish your meta-theorem `F` from any other interesting theorem.

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.

> I think one of the greatest difficulties in completely automated mathematics would be the discovery of mostly those things which are interesting.

So, something like a recommendation algorithm? Netflix for Mathematicians?

Well, except that it simply can not be social recommendation. Math is too big, and interesting results too sparse for that.

> 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.

> I think one of the greatest difficulties in completely automated mathematics would be the discovery of mostly those things which are interesting.

But isn't 'interest' subjective?

If your definition of subjective is "decided by humans", then yes.

EDIT: "determined by" is probably more precise than "decided by" (determination is not necessarily conscious or explicit)

> If your definition of subjective is "decided by humans", then yes.

Presumably it means something more like "different (rational, honest, omnipotent) respondents might produce different answers."

>...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.

Brilliant, now we have free random points in theorem-space. Now what?

Presumably, you use them for long distance communications, early-warning systems, surveillance, scientific experimentation, &etc.

I'm working on this for my thesis. Would love to chat, please contact me juan at juan dot com dot uy