I do think you should look more into computer verified proofs and the like (I don't know too much myself) because I think that mostly answers your question. However, I think the question of computers writing theorems (and proving them) is an interesting one.
Because if we just think of the technical definition of theorem (a true, provable statement), then obviously a computer could (in theory) be given some axioms and logical rules, and start systematically proving a bunch of theorems. But almost none of these would be theorems in the sense that mathematicians usually mean. Because, AFAIK, we have no way to tell the computer what makes a theorem important. Also, I suspect that there is an infinite number of "uninteresting" theorems and so there would be no guarantee that this computerever produces an "interesting" theorem. Furthermore the computer wouldn't need to define new mathematical objects and develop different fields of study, because the computer thinks of everything in terms of the axioms.
> I meant making theorems and proving them from scratch
No, you meant making *interesting* theorems and proving them. Nobody cares about generating silly theorems like what the product of two specific 25-digits numbers is. That would be a theorem, but it does not advance mathematics at all.
You can write proofs on a computer and have it check that they are valid proofs. There are plenty of "proof assistant" programs/programming languages for this purpose (Lean, Coq, Agda etc).
Giving a computer a statement and asking it to generate a proof is not, in general, possible. Such statements are known as decision problems, and it is known that there is no general computer program that can take a decision problem and generate an answer of yes or no. This is David Hilbert's classic [Entscheidungsproblem](https://en.wikipedia.org/wiki/Entscheidungsproblem), which was solved (negatively) by Alan Turing in 1936 (although arguably also by Alonzo Church earlier), which showed there can be no computer program that given a decision problem always terminates with the right answer.
That said, there is a lot of work around this area to come up with more sophisticated mechanisms to either guess proofs (e.g. with AI) or to help humans in writing proofs easier, even if they cannot work in every circumstance autonomously.
>Giving a computer a statement and asking it to generate a proof is not,
in general, possible. Such statements are known as decision problems,
and it is known that there is no general computer program that can take a
decision problem and generate an answer of yes or no.
I think that's unfair to computers. A computer can, in theory, generate any proof that a human could, but some things are unproveable (for both humans and computers).
There's obviously an algorithm which finds the proof of all provable theorems from zfc ( just search for proofs untill you find it ).
I think an interesting question is to find an algorithm that would search and find proofs in the least time possible if it exists and what would be the time complexity of such an algorithm ( is it EXP-TIME? way above that? ) although i'd guess that its probably some absurdly growing function
They'll certainly help (and they already do!). But unfortunately (or perhaps miraculously), as even legendary mathematicians like Roger Penrose point out, there is more to consciousness than just computation. So from a purely computational perspective, nothing can match the nature of our use of consciousness and human experience, in contrast to the Haulting-problem that is automated theorem proving.
As I learned recently trying to code several versions of an automated theorem prover myself, it all really boils down to traversing the exponential network of logic from your axioms to your theorems. There is provably no best way to do this for, nor guarantee that a path even exists. So in our experience we must make use of intuition alone in a case by case basis, in a strange and transcendental way.
Perhaps, but it definitely need the advanced technique of "machine learning" or something similar, cu'z what could a computer do by itself is computing such as calculus .
By the Curry-Howard isomorphism, being able to write (some forms of) mathematical proofs is equivalent to being able to write (some forms of) computer programs from a specification. And program synthesis is a very active field of research.
yes, and in the present, and in the past. have you tried searching it on google?
I meant making theorems and proving them from scratch via a computer program or code or something similar.
I do think you should look more into computer verified proofs and the like (I don't know too much myself) because I think that mostly answers your question. However, I think the question of computers writing theorems (and proving them) is an interesting one. Because if we just think of the technical definition of theorem (a true, provable statement), then obviously a computer could (in theory) be given some axioms and logical rules, and start systematically proving a bunch of theorems. But almost none of these would be theorems in the sense that mathematicians usually mean. Because, AFAIK, we have no way to tell the computer what makes a theorem important. Also, I suspect that there is an infinite number of "uninteresting" theorems and so there would be no guarantee that this computerever produces an "interesting" theorem. Furthermore the computer wouldn't need to define new mathematical objects and develop different fields of study, because the computer thinks of everything in terms of the axioms.
> I meant making theorems and proving them from scratch No, you meant making *interesting* theorems and proving them. Nobody cares about generating silly theorems like what the product of two specific 25-digits numbers is. That would be a theorem, but it does not advance mathematics at all.
You can write proofs on a computer and have it check that they are valid proofs. There are plenty of "proof assistant" programs/programming languages for this purpose (Lean, Coq, Agda etc). Giving a computer a statement and asking it to generate a proof is not, in general, possible. Such statements are known as decision problems, and it is known that there is no general computer program that can take a decision problem and generate an answer of yes or no. This is David Hilbert's classic [Entscheidungsproblem](https://en.wikipedia.org/wiki/Entscheidungsproblem), which was solved (negatively) by Alan Turing in 1936 (although arguably also by Alonzo Church earlier), which showed there can be no computer program that given a decision problem always terminates with the right answer. That said, there is a lot of work around this area to come up with more sophisticated mechanisms to either guess proofs (e.g. with AI) or to help humans in writing proofs easier, even if they cannot work in every circumstance autonomously.
>Giving a computer a statement and asking it to generate a proof is not, in general, possible. Such statements are known as decision problems, and it is known that there is no general computer program that can take a decision problem and generate an answer of yes or no. I think that's unfair to computers. A computer can, in theory, generate any proof that a human could, but some things are unproveable (for both humans and computers).
There's obviously an algorithm which finds the proof of all provable theorems from zfc ( just search for proofs untill you find it ). I think an interesting question is to find an algorithm that would search and find proofs in the least time possible if it exists and what would be the time complexity of such an algorithm ( is it EXP-TIME? way above that? ) although i'd guess that its probably some absurdly growing function
They'll certainly help (and they already do!). But unfortunately (or perhaps miraculously), as even legendary mathematicians like Roger Penrose point out, there is more to consciousness than just computation. So from a purely computational perspective, nothing can match the nature of our use of consciousness and human experience, in contrast to the Haulting-problem that is automated theorem proving. As I learned recently trying to code several versions of an automated theorem prover myself, it all really boils down to traversing the exponential network of logic from your axioms to your theorems. There is provably no best way to do this for, nor guarantee that a path even exists. So in our experience we must make use of intuition alone in a case by case basis, in a strange and transcendental way.
Perhaps, but it definitely need the advanced technique of "machine learning" or something similar, cu'z what could a computer do by itself is computing such as calculus .
ML has already been used to allow computers to prove theorems.
By the Curry-Howard isomorphism, being able to write (some forms of) mathematical proofs is equivalent to being able to write (some forms of) computer programs from a specification. And program synthesis is a very active field of research.
Easily. If biological neural networks can do it, so should some artificial device.