Automation

[Filip Cernatescu]

I have a question for set.mm contributors:

Automatic prover for a+b,a-b,a×b,a/b, a<b,a>b... it will be necessary?

[Giovanni Mascellani]

Hi,

Il 09/11/19 12:27, 'Filip Cernatescu' via Metamath ha scritto:

> Automatic prover for a+b,a-b,a×b,a/b, a<b,a>b... it will be necessary?

Maybe not necessary, but I believe it would be good to have automated
provers for everything that can be automated. Unfortunately not any
problem arising in real number (or integer number) theories can be
decided automatically, but some can. Z3 can prove statements (and emit
related proofs) in a range of theories, also using real numbers, and
eventually I would like to be able to convert those to Metamath.

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Olivier Binda]

If what you want is something that is able to compute AND prove by itself that the result of 

 "( ( ( ; 2 6 + ( 2 ^ 3 ) ) x. ( ( ( 7 x. ; 8 9 ) x. ( ; ; 1 2 3 + ( 7 x. ( ! ` 5 ) ) ) ) - ; ; 2 3 8 ) ) / ; 1 4 )"

is ; ; ; ; ; ; 1 4 5 6 4 4 1

I have one prototype working, but I am not yet ready to release it publicly.

[David A. Wheeler]

> Le samedi 9 novembre 2019 12:27:12 UTC+1, Filip Cernatescu a écrit :
> > I have a question for set.mm contributors:
> > Automatic prover for a+b,a-b,a×b,a/b, a<b,a>b... it will be necessary?

mmj2 includes *some* of that. I don't know about "necessary", but it's certainly *useful*.

--- David A. Wheeler

[Filip Cernatescu]

Hello Olivier Binda!

It is awesome what you have done!

Will you release as a open source your project or it will be a closed source project with money?

Regards

[Olivier Binda]

It will be a closed source, but free to use the binary forever (and sources become open after I die or with a 2 years delay or once I have made some decent money out of the project ( I'm not too greedy but we are talking about 3+/5+/8+ years of ongoing development, there)) kind of project.
The feature complete mathematical core should be free to use (with a caveat : a time limit so that once every x months, you have to redownload/update it (for free) so that it stays up to date)
Also, there won't be crap like ads, or pay to unlock (except pay 2€ once to unlock things not necessary to do maths, but that may provide fun/rewarding functionalities)

I intend to make some money out of it, but by providing value to customers (like math lessons for people who learn maths, or developing a game out of it, like candy crush but for teaching people maths). 

If you need a complex calcul done now, please post it and I'll see If it can do it now (and send you the uncompressed proof) and if it cannot be done now, I'll strive to improve my prototype so that it can do it.

Best regards,
Olivier

[Jens-Wolfhard Schicke-Uffmann]

Hi,

For completeness sake (in case anyone needs a integer-oriented automation on short notice),
so does https://github.com/Drahflow/Igor

+ , - , * , ^ on NN0 should be complete
<, <_, >, >_ on RR (including transitivity), should also be complete IIRC
... and of course everything in deduction-form.


Regards,
Drahflow