Anybody here has any experience with proof assistant software?

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

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?

>expecting a proof assistant to generate definitions and postulates (because that's how new math is made)

Wat

Why don't I just use artificial intelligence to generate those definitions and train it to find the ones that seem the most interesting?

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

Where the fuck are you getting that implication, son? Because it sure isn't in my words.

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

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

Because you're a moron who doesn't actually know how AI works

...

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.

>rip in pieces
>zyzz come back to us