An Algorithm that produces Mathematical Theorems?

[Unity+]

Does an algorithm exist that uses the most fundamental theorems of mathematics and creates even more theorems that build up mathematics?

 

If not, I am thinking about pursuing a project as such. Though it might not be completely efficient to make one, I want to see if it is possible to produce one.

[imatfaal]

I think the answer is yes. A quick search of my memory banks found this blogpost

 

http://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/

 

FYG Timothy Gowers is a Field's Medalist so it isn't exactly amateur speculation.

 

If you cannot find any more on it on the web I will re-think - I definitely heard a podcast all about a computer algorithm that generated true propositions of increasing complexity

[Unity+]

I think the answer is yes. A quick search of my memory banks found this blogpost

 

http://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/

 

FYG Timothy Gowers is a Field's Medalist so it isn't exactly amateur speculation.

 

If you cannot find any more on it on the web I will re-think - I definitely heard a podcast all about a computer algorithm that generated true propositions of increasing complexity

The only problem is the algorithm he presented, he stated, only solves mathematical problems and doesn't take a current conjecture and say "Yes, this conjecture is true" and it outputs the proof as such.

 

 

 

Over the last three years, I have been collaborating with Mohan Ganesalingam, a computer scientist, linguist and mathematician (and amazingly good at all three) on a project to write programs that can solve mathematical problems.

For example, the algorithm I am referring to would be one that can take a conjecture, like the Collatz conjecture, and even if there are infinite numbers to test with the computer would find a proof that would prove that the conjecture is true.

 

Unless his algorithm can do similar things. I might be wrong on this.

Edited February 28, 2014 by Unity+

[Bignose]

Normally, a 'proof by computer' in the way you are suggesting is done when the number of cases to study is high, but finite -- and you can then sic the computer on the task of exhaustively checking each case.

 

I would say that I would be surprised if any time soon we have any system that can be inputted a conjecture and be outputted a proof, other than a simple lookup database.

 

The algorithm being talked about above seems to be good for exploring the space of truths given certain inputs. I imagine you can help direct it by giving it a certain limited about of givens. But that can be limiting, because often you don't know what axioms you will end up using to get to the final result.

 

In short, proof making is still largely an art form, and computers haven't been all that good at recreating art-type stuff. Though, they do seem to get better at it every day.

[Unity+]

Normally, a 'proof by computer' in the way you are suggesting is done when the number of cases to study is high, but finite -- and you can then sic the computer on the task of exhaustively checking each case.

 

I would say that I would be surprised if any time soon we have any system that can be inputted a conjecture and be outputted a proof, other than a simple lookup database.

 

The algorithm being talked about above seems to be good for exploring the space of truths given certain inputs. I imagine you can help direct it by giving it a certain limited about of givens. But that can be limiting, because often you don't know what axioms you will end up using to get to the final result.

 

In short, proof making is still largely an art form, and computers haven't been all that good at recreating art-type stuff. Though, they do seem to get better at it every day.

I am currently working(though with little success on a concrete algorithm) on an algorithm that takes the Fundamental Theorem of Mathematics and tries to "tree-branch" theorems using a fundamental and semi-fundamental theorem of mathematics. It involves a "theorem constant", which is not a numeral value but a logic-based value that is detected through out theorems, which would help determine new theorems. Though, again, it is conceptual and is merely at the drawing board still.

 

If I get any progress, I will post it and see if anyone things it has potential.

[John]

What is the Fundamental Theorem of Mathematics?

As for the general idea of an automated theorem prover, let me post some thoughts, with the caveat that my own study of logic is limited. Hopefuly, if any logicians turn up, they won't find anything completely objectionable.

 

The halting problem limits what can be accomplished by an automated theorem prover under current physically realizable models of computation. There is no general algorithm capable of deciding the truth or lack thereof of an arbitrary statement regarding the natural numbers. We can use a Gödel numbering system to encode formal statements as natural numbers, thus it follows that there is no general algorithm capable of deciding the truth or lack thereof of an arbitrary formal statement.

 

There is the concept of the oracle machine, which is essentially a Turing machine paired with a "black box" capable of solving the halting problem for Turing machines. Certain conjectures (including the Collatz conjecture, I believe) would be relatively easy for such a machine to solve. However, even an oracle machine would still be incapable of solving the halting problem for equivalent oracle machines, and in fact we don't know whether such a machine can be built in the first place.

As far as I know, it's also an open question whether human brains can solve the halting problem, and so we may someday discover we share this limitation with computers. Certainly we share a more fundamental limitation in that, by Gödel's first incompleteness theorem, any "sufficiently strong" formal system (examples of which include Peano arithmetic and Zermelo-Fraenkel set theory) contains true statements which aren't provable in the system. Thus, even ignoring the infinitude of formal statements, generating a complete set of theorems (and leaving out false statements) in a given theory is impossible, using a computer program or otherwise.

Now, automated theorem provers have been in use for years now, and programs have been used to assist in proofs (perhaps most notably in the case of the four-color theorem). However, it's difficult (and perhaps impossible) for a computer program to determine what results are mathematically interesting, and it's difficult (and perhaps impossible) for a computer to take a bird's eye view of mathematical theory and develop deep insights into how everything works. Simply spitting out results isn't the aim of mathematics. Rather, we seek human understanding of how mathematics works. An automated theorem prover doesn't, and perhaps can't, offer that generally.

Of course, if we develop a true AI, then maybe all bets are off.

Edited March 1, 2014 by John

[Unity+]

Now, automated theorem provers have been in use for years now, and programs have been used to assist in proofs (perhaps most notably in the case of the four-color theorem). However, it's difficult (and perhaps impossible) for a computer program to determine what results are mathematically interesting, and it's difficult (and perhaps impossible) for a computer to take a bird's eye view of mathematical theory and develop deep insights into how everything works. Simply spitting out results isn't the aim of mathematics. Rather, we seek human understanding of how mathematics works. An automated theorem prover doesn't, and perhaps can't, offer that generally.

That depends on what you mean by an automated theorem prover. While they used computer algorithms to be proved, there was a specific task for such a proof given to the algorithm. What I am referring to is a generalized form of an algorithm.

 

While I agree that the point of proofs are to give a human understanding of mathematics, it is important to realize that computers would give much help to providing an understanding if this algorithm were produced. In fact, if such an algorithm were developed it would provide a way for mathematicians to use similar patterns of proofs to understand theorems and conjectures.

 

 

 

The halting problem limits what can be accomplished by an automated theorem prover under current physically realizable models of computation. There is no general algorithm capable of deciding the truth or lack thereof of an arbitrary statement regarding the natural numbers. We can use a Gödel numbering system to encode formal statements as natural numbers, thus it follows that there is no general algorithm capable of deciding the truth or lack thereof of an arbitrary formal statement.

I can see the issue here. Machines are limited to how they can interpret truth because truth is ultimately defined by their own rules as well. However, doesn't this also apply to Mathematics in general? We base proofs off of theorems that are based off of theorems, which are eventually based off axioms of Mathematics. As the definition of an axiom states, an axiom is a starting point of reasoning(http://en.wikipedia.org/wiki/Axiom). Therefore, the same principle could apply to a machine as axioms would be defined for a machine from which it would know truth from in the same way we hold truth to our axioms of Mathematics. Therefore, wouldn't truth be defined by the axioms presented to such a machine and provide an end point of a proof just like how we use axioms to provide an end point to our proofs? This is a very interesting topic, I must say.

 

 

 

What is the Fundamental Theorem of Mathematics?

Though there isn't really a fundamental theorem of mathematics, it seems there must be because of the existence of many other fundamental theorems that exist that are potentially semi-fundamental theorems of mathematics. That is what I was approaching.

Edited March 1, 2014 by Unity+

[John]

That depends on what you mean by an automated theorem prover. While they used computer algorithms to be proved, there was a specific task for such a proof given to the algorithm. What I am referring to is a generalized form of an algorithm.

 

While I agree that the point of proofs are to give a human understanding of mathematics, it is important to realize that computers would give much help to providing an understanding if this algorithm were produced. In fact, if such an algorithm were developed it would provide a way for mathematicians to use similar patterns of proofs to understand theorems and conjectures.

Certain results can be proved via computer program, and I agree the output of such a program can potentially aid a human user in deepening his understanding. However, no general algorithm exists that's capable of deciding the truth of arbitrary statements. This is the essence of the halting problem as it relates to automated theorem proving.

 

And I'm referring to "automated theorem provers" in the sense of http://en.wikipedia.org/wiki/Automated_theorem_proving.

 

I can see the issue here. Machines are limited to how they can interpret truth because truth is ultimately defined by their own rules as well.

 

However, doesn't this also apply to Mathematics in general? We base proofs off of theorems that are based off of theorems, which are eventually based off axioms of Mathematics. As the definition of an axiom states, an axiom is a starting point of reasoning(http://en.wikipedia.org/wiki/Axiom). Therefore, the same principle could apply to a machine as axioms would be defined for a machine from which it would know truth from in the same way we hold truth to our axioms of Mathematics. Therefore, wouldn't truth be defined by the axioms presented to such a machine and provide an end point of a proof just like how we use axioms to provide an end point to our proofs? This is a very interesting topic, I must say.

The issue is a bit more fundamental than that, and in some ways is connected to Gödel's incompleteness theorems, which are very deep results about the nature of formal systems. I won't venture too far into details (mainly because there's a lot I've forgotten since I really studied mathematical logic ), but proofs of and discussions about the halting problem, the incompleteness theorems, and their relationship to each other, can be found all over the Web.

 

Suffice it to say that, in any sufficiently strong formal system (and this includes a choice of axioms), there are statements which are true but unprovable, and it's impossible for the system to prove its own consistency. These are fundamental limitations on what we can deduce from any given set of axioms.

 

Though there isn't really a fundamental theorem of mathematics, it seems there must be because of the existence of many other fundamental theorems that exist that are potentially semi-fundamental theorems of mathematics. That is what I was approaching.

Well, in various areas of mathematics, there are certain results considered important enough that we call them "fundamental," but I'm not sure the word is being used in quite the way you're taking it.

 

It's a minor point, anyway. I just wondered if you had some specific theorem in mind.

[Unity+]

Certain results can be proved via computer program, and I agree the output of such a program can potentially aid a human user in deepening his understanding. However, no general algorithm exists that's capable of deciding the truth of arbitrary statements. This is the essence of the halting problem as it relates to automated theorem proving.

 

And I'm referring to "automated theorem provers" in the sense of http://en.wikipedia.org/wiki/Automated_theorem_proving.

 

 

The issue is a bit more fundamental than that, and in some ways is connected to Gödel's incompleteness theorems, which are very deep results about the nature of formal systems. I won't venture too far into details (mainly because there's a lot I've forgotten since I really studied mathematical logic ), but proofs of and discussions about the halting problem, the incompleteness theorems, and their relationship to each other, can be found all over the Web.

 

Suffice it to say that, in any sufficiently strong formal system (and this includes a choice of axioms), there are statements which are true but unprovable, and it's impossible for the system to prove its own consistency. These are fundamental limitations on what we can deduce from any given set of axioms.

 

 

Well, in various areas of mathematics, there are certain results considered important enough that we call them "fundamental," but I'm not sure the word is being used in quite the way you're taking it.

 

It's a minor point, anyway. I just wondered if you had some specific theorem in mind.

In mind, I would be referring to the Fundamental theorem of algebra, for example.

[Unity+]

Certain results can be proved via computer program, and I agree the output of such a program can potentially aid a human user in deepening his understanding. However, no general algorithm exists that's capable of deciding the truth of arbitrary statements. This is the essence of the halting problem as it relates to automated theorem proving.

 

And I'm referring to "automated theorem provers" in the sense of http://en.wikipedia.org/wiki/Automated_theorem_proving.

 

 

The issue is a bit more fundamental than that, and in some ways is connected to Gödel's incompleteness theorems, which are very deep results about the nature of formal systems. I won't venture too far into details (mainly because there's a lot I've forgotten since I really studied mathematical logic ), but proofs of and discussions about the halting problem, the incompleteness theorems, and their relationship to each other, can be found all over the Web.

 

Suffice it to say that, in any sufficiently strong formal system (and this includes a choice of axioms), there are statements which are true but unprovable, and it's impossible for the system to prove its own consistency. These are fundamental limitations on what we can deduce from any given set of axioms.

 

 

Well, in various areas of mathematics, there are certain results considered important enough that we call them "fundamental," but I'm not sure the word is being used in quite the way you're taking it.

 

It's a minor point, anyway. I just wondered if you had some specific theorem in mind.

Another thing that would be interesting to see is the limitations of proofs for a given system of axioms. For example, would it be provable to determine the exact amount of simplified theorems that would result from a set of axioms?

[John]

For some sets of axioms, perhaps. However, I think it's difficult to precisely define what we mean when we talk about enumerating simplified theorems.

 

For instance, by "theorem," do we mean a result we find interesting? Do we mean "theorem" in the sense of proof theory, where it refers to a well-formed formula of a formal language? I would assume the latter, based on the context of the conversation and because the former is subjective, but in the latter case I would imagine there are infinitely many theorems except perhaps in certain extremely simple or restrictive languages.

 

This brings us to the question of simplification. Where do we draw the line? If we're talking about a formal proof of some theorem in a formal language, then what we have is a list of statements following from previous statements. In a precise sense, at what point do we divide the list into a "simplified" section and a "redundant" section? Ultimately, would it make sense to regard anything besides the axioms themselves as simplified, since everything else just follows from them?

[Unity+]

For some sets of axioms, perhaps. However, I think it's difficult to precisely define what we mean when we talk about enumerating simplified theorems.

 

For instance, by "theorem," do we mean a result we find interesting? Do we mean "theorem" in the sense of proof theory, where it refers to a well-formed formula of a formal language? I would assume the latter, based on the context of the conversation and because the former is subjective, but in the latter case I would imagine there are infinitely many theorems except perhaps in certain extremely simple or restrictive languages.

 

This brings us to the question of simplification. Where do we draw the line? If we're talking about a formal proof of some theorem in a formal language, then what we have is a list of statements following from previous statements. In a precise sense, at what point do we divide the list into a "simplified" section and a "redundant" section? Ultimately, would it make sense to regard anything besides the axioms themselves as simplified, since everything else just follows from them?

Well I imagine a tree branch-type system where theorems branch off from the axioms that are given. If we are to define simplification, there must be a limit to the definition of a theorem. For example, maybe a theorem that comes from the Fundamental Theorem, or set of axioms, must only contain 2 to 3 of the axioms that exist within the Fundamental Theorem.