/sci/ - Science & Math

Also:
Could such a program use some optimization techniques to make proofs simpler/shorter? For example, if theorem is a corollary of some other huge theorem, maybe we don't need *all* the stuff from the huge theorem, we only need a little bit of stuff.
Or am I a retarded kode monkey?

>>12520776
Sure, you can enumerate every possible proof

>>12521651
god i hate mathematicians

>>12521651
Do it.

>>12521651
First define the space G of proofs. Say V is a space, F:G-->V is a proof homomorphism if and only if...

>>12522045
Wildberger wouldn't mind, it's an entirely finitistic process. Pick your formal language, start enumerating all possible strings in that language plus carriage return (easy), check whether each string gives you a valid mathematical proof (easy), if it does then add it to the pile

>>12520776
Just prove your theorem in Coq and evaluate the proof term into its normal form. It will probably take several times the age of the universe for anything nontrivial, but in theory it'll terminate.

>>12522117
if alphaGo can intuit winning strategy why can't there be an alphaCoq that builds a nontrivial proof

>>12520776
By Godel's incompleteness theorems, the answer is NO.

Given an axiomatic system, there are some true number theoretic statements (i.e. theorems) which cannot be proven from the axioms (and adding more axioms doesn't solve the problem).

>>12520776
Yes, I'm currently working on a proof method similar to induction for the rationals, if brainletberger's fandom turns out to be right then most proofs could surely be able to be solved if you trained a deep learning algorithm to solve by induction and use this method since if will most likely hold for countably infinite sets

>>12520776
yes, it's called automated deduction. If there is a path from the axioms to the statement (it is decidable) - you can go both ways.

>>12520776
Proofing something is usually a non polynomial problem, so unless it turns out that N=NP. It would be a maybe in theory but a definite no in reality, at least for harder problems.

It's called Coq

>>12520776
>any theorem

Turing literally died again after reading that

>>12522177
Okay, serious question; how much of a "problem" really is Godel? Do his incompleteness theorems mean we can never know the whole truth of mathematics, or do we just have to be a lot more clever about how prove things, compared to current axiomatic systems?

I don't mean more clever as in "add more axioms", but as in if there's an even stronger logic that Godel doesn't apply to.

>>12522177
Goedel statements do not have proofs and are therefore not theorems.

>>12522165
I'll give you an alpha cock
*unzips dick*

>>12522554
The latter. For example you can prove consistency of PA assuming transfinite induction up to epsilon-0 (or something like that)

>>12522558
Didn't he calculate them? They weren't just "statements".

>>12522585
By "Goedel statement" I'm referring to a proposition P provably equivalent to the proposition that P has no proof, which he showed exists in any theory strong enough to develop arithmetic in.

>>12522558
This is incomplete. I should have said that in consistent theories Goedel statements do not have proofs and are therefore not theorems. Otherwise the statement has both a proof and a disproof.

>>12522572
True, but it's also possible the stronger logic is inconsistent, in which case that proof isn't very meaningful. The stronger logic can prove Peano arithmetic's consistency but not its own.

>>12522662
Yes, to prove consistency of the stronger logic you would need to move to an even stronger one -- which is not impossible

>>12520776
According to Gödel you either won't have a consistent system or fail to find proof for every theorem.

>>12522572
>>12522662
>>12522683
So, hypothetically, if we were able to construct an infinite family of logics (if such a phrase is even meaningful), each member being stronger than the last, could it be said that such a system could prove all true statements?

>>12522712
Such a system would itself have a Goedel statement.

>>12522386
you mean lean

>>12520776
Boy have I got a faggot for you.
https://en.m.wikipedia.org/wiki/Alan_Turing

>>12522774
Only if it's still recursively axiomatized, so it depends on what >>12522712 has in mind. Without that restriction, there's nothing stopping you from just adding every true statement to your tower of theories as axioms, and then the union would prove all true statements trivially. That's why "recursively axiomatized" is a necessary part of the theorem

>>12522562
your dick has a zipper in it? do you mean unzips pants?

>>12522836
I said what I said

>>12522554
Per Goedel's completeness theorem, the incompleteness theorem is related to the existence of nonstandard models of the natural numbers. These alternate versions of the natural numbers follow all of the axioms in our theory of natural numbers (which I'm assuming to be a first-order theory), but in these alternate natural numbers, there is a number encoding a proof of the Goedel statement, making the Goedel statement false when applied to these numbers.

>>12520776
What counts as a direct proof? Do you mean not using proof by contradiction, or something else?

And what do you mean by "without using any other theorems"? If I just listed all the necessary theorems along with their proofs, as well as any theorems used by those theorems, and so on, and called them steps in the proof, would that be allowed?

>>12520776
It's called high school student.

But otherwise... It is.

There ware mathematical entities like that available on the internet, until somebody bought their founder and paywalled them very much.

It atleast applies for logic sets, in which axioms can be described.

>>12522177
You're thinking of Tarski's theorem.

>>12522801
>adding all true statements
True relative to what system? The problem is that you don't know which statements are true.

>>12520776
angery Roger Penrose noises

>>12520776
Most answer around here are retarded. They invoke issues about incompleteness by parroting Gödelian speak, but this is totally unrelated to OP's question.

What OP is asking for is called "cut elimination", which is a property that most sane logical systems enjoy. Even so, you can always tweak the definition of your system to make cut elimination hold.

If you express the derivation rules of your system as a programming language à la Curry-Howard, even if it's based on classical logic, you can easily write a normalization procedure that performs full cut elimination, and as such, removes the use of all intermediate theorems. It's very easy to do, but doing it efficiently is harder (see e.g. normalization by evaluation) and in practice most of the time the normalized proofs will be so big that it will take eons before the normalization procedure terminates.

TL;DR: YES. And other posters are retarded faggots.

>>12523815
Just plain true, in the sense of model-theoretic truth satisfaction. It's just not a computable construction. It's like using an ultrafilter or choice function, you can't actually construct it but you can still do math with it

>>12524137
Most of the discussion wasn't trying to answer OP's original question; the wrong answer here >>12522177 kind of derailed the thread into talking about Goedel even though it was pointed out the answer was wrong. But thanks for getting the thread back to OP's question with a good answer.