Anybody here has any experience with proof assistant software?
How advanced is it as of now? Is it actually useful?
I am interested as well
>>8133116
>Anybody here has any experience with proof assistant software?
Yeah I love Cock.
>How advanced is it as of now? Is it actually useful?
Pretty advanced. Yes.
If proof assistants are so good, then why are there mathematicians?
>>8133933
its a fuking ASSISTANT, it only ASSISTS u retard
>>8133933
>if humans evolved from monkeys, why are there still monkeys?
Coq is nice
I don't know how useful it is right now, but I think they're definitely worth learning. Makes you think about mathematical proof in a different way.
>>8133939
If computers are so good at computation, why can't they compute proofs for us, rendering mathematicians useless?
>>8134017
The set of mathematical theorems is recursively enumerable, so why don't we just recursively enumerate all of the theorems until we find, e.g., a formal proof of the Riemann hypothesis?
>>8133116
>Is it actually useful?
Useful for what?
I have found it very useful for confirming that the mathematics I thought up is actually valid (which is far harder than it seems, and there are actually quite a lot of errors in published mathematics). It is not particularly useful for developing new mathematics. Coq is especially bad at this.
>>8134178
So, what, you put your discovered theorem into it, have it search for a proof of the theorem, and it usually finds one in reasonable time?
Do you have to phrase your discovered theorem in the language of set theory?
And if that's so useful, why don't people just stick their conjectures into it and let it search for a proof of their conjectures?
>>8134178
>expecting a proof assistant to generate definitions and postulates (because that's how new math is made)
Wat
>>8134181
Why don't I just use artificial intelligence to generate those definitions and train it to find the ones that seem the most interesting?
>>8134179
>So, what, you put your discovered theorem into it, have it search for a proof of the theorem, and it usually finds one in reasonable time?
No. You need to prove it yourself in the proof assistant. The contribution of the proof assistant is that it will not let you mess up your proof by getting technicalities wrong.
>>8134181
Where the fuck are you getting that implication, son? Because it sure isn't in my words.
>>8134186
But you can't put every single line of the formal proof into the proof assistant. That would be dozens of pages for even one-paragraph lemmas.
One can certainly improve upon formal Hilbert-style proofs to make them more readable, but I'm so skeptical that they've been improved upon that much. Especially considering the diverse range of studies of various areas of mathematics (all of which, while formally expressible in the formal language of set theory, operate many levels of abstraction from talking about mere sets).
>>8134197
>But you can't put every single line of the formal proof into the proof assistant. That would be dozens of pages for even one-paragraph lemmas.
Indeed. That's what some primitive proof assistants such as automath and metamath do, and it's horrible.
>One can certainly improve upon formal Hilbert-style proofs to make them more readable, but I'm so skeptical that they've been improved upon that much.
That depends a bit on the exact proof assistant. Isabelle, for example, can often express proofs that are _reasonably_ close to the conciseness of textual proofs. The proofs consist of statements of the form "then <something> holds, because of earlier-proved properties X, Y, Z", which powerful automated systems will then often be able to verify independently. If you do it right, these automagic steps can often -- but not always -- be of the same step size as you would write in an article.
Coq, by comparison, has less automation and longer, more technical proofs. The great upside of coq is that technical transformations that you want to do can often be a great deal easier than they would be in Isabelle, which occasionally has real problems getting the automation engines to derive trivial technical steps.
>Especially considering the diverse range of studies of various areas of mathematics (all of which, while formally expressible in the formal language of set theory, operate many levels of abstraction from talking about mere sets).
The proof assistants can deal with higher abstractions just fine; that part is not a problem at all. The real problem lies in the step size of the derivation steps that you want to make.
>>8134185
Because you're a moron who doesn't actually know how AI works
>>8133116
>>8134223
I am sincerely disappointed that the only response my reply elicited was that of an insecure person rather than helpful information about using neural networks or evolutionary programming to invent interesting mathematical objects.
>>8134260
>rip in pieces
>zyzz come back to us
