Short answer : At the moment (19/11/2019) Mephistolus is a library, written in the (new but promising) Kotlin langage. It is mostly a tooling layer over metamath that holds :
a Metamath parser : for turning strings into Metamath trees an experimental Math API : for mutating Metamath trees and proving the mutations, a bit like we, humans, do maths simple math services : for automatically providing the numerous hypotheses needed by theorems, like A =/= 0, A e. B, A <_ B, ... a collection of Mephistolus theorems (like metamath deduction theorems but that make handling any number of antecedents easier) a Mephistolus proof checker a Mephistolus to MetaMath proof exporter a Metamath Proof checker (to test the exported metamath proofs) The only user that this library will probably ever have is me. But, I intend to use this library to build a free (but closed) app that allows anyone to read/write/use ( metamath) proof checked maths I have 2 targets for the app : - mathematicians - the general public (say everyone between 16 and 99 years old) First, I am focusing on mathematicians and my priority is to build the library so that it enpowers the metamath-experts among mathematicians to have a better/faster workflow. Basicaly, I would like Mephistolus to allow expert meta-mathematiciens to prove what they want, without hassle, faster and with all the help a computer (and code by me) can muster (it is a goal for Mephistolus to be fun, powerful and hassle free). As of now, I do not know if you have a use yet for the help that Mephistolus can provide : It only handles a few operators (+, -, /, *, ^, !, -u, -., /\\, \//, A., E., [_ / ]_, [ / ], F/, F/_, e., <, <_, C_, sum_ It can apply any metamath theorem but it can only provide sugar/fun math api for Mephistolus-theorem So, I am slowly improving it, in the hope that one day, it will provide enough to make people want to use Mephistolus more than, say mmj2 which is powerful and efficient, now. The snipets I post are to give people some idea what to expect. This is neither the user experience, nor a gui. You are right, I should document how you build a proof in Mephistolus. I'll think how (maybee slides ?) to explain what could be done with Mephistolus Thanks for the pointers, Olivier Le mardi 19 novembre 2019 09:32:09 UTC+1, Mario Carneiro a écrit : > > Have you thought about providing a limited release, or a recording of you > using the program? It's not really clear to me what the overall program is, > and you post snippets that lack the context to make sense of them (I don't > think you are expecting people to run them, but I don't even know what > language they are written in). Is this the end user experience or is there > some GUI front end? The code snippets on their own only provide a myopic > view into the development process. > > I know you want to ultimately sell this program, and I don't want to make > you do anything to compromise that, but you might get more and better > feedback if you provide a more comprehensive overview of what the program > is. > > Mario > > On Tue, Nov 19, 2019 at 3:23 AM Olivier Binda <[email protected] > <javascript:>> wrote: > >> Let's make this the Thread about Mephistolus (it'll help prevent me >> spamming the metamath group). >> I'll report the Mephistolus progress in here and maybee also, post stuff >> about it's internals and design decisions >> ( and ask a lot of help for metamath experts when I'm at a loss, I'll be >> in you gentle care :)) >> >> Milestone 5 has been reached, with the first Mephistolus-proof exported >> and proof checked in Metamath for an exercise I give to my students (now >> only 400+ more to go :) ) : >> >> >> |- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) >> ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) ) >> >> >> Here is the high level human proof : >> >> /** proving that ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. >> ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) ) */ >> val assertion = "( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) >> )".toSingle("∨1c e. CC", "∨3c e. NN0") >> val result = "( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) )".toStatement() >> val step = "|- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( >> 0 ... ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) >> )".toStatement() >> val i = "∨2s".toStatement() >> val j = dummy(MType.S, assertion.origin, *assertion.context.toTypedArray()) >> val proof = assertion >> .s(AxSum) >> /*.s(A_times_Sum)*/ // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( 1 - ∨1c >> ) x. ( ∨1c ^ ∨2s ) ) >> .c(rotX) >> // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ∨1c ^ ∨2s ) x. ( 1 - ∨1c ) ) >> .c(Ax_BsubC) >> // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ( ∨1c ^ ∨2s ) x. 1 ) - ( ( >> ∨1c ^ ∨2s ) x. ∨1c ) ) >> .eq(P.c.a.th(Ax1), P.c.c.th(Aexp_Bp1)) >> // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ∨1c ^ ∨2s ) - ( ∨1c ^ ( ∨2s >> + 1 ) ) ) >> .s(Sum_AsubB) >> // ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨2s e. ( >> 0 .. ∨3c ) ( ∨1c ^ ( ∨2s + 1 ) ) ) >> .c(Sum_CDI) { arrayOf(j, statement1, "( ∨1c ^ ( ( $j - 1 ) + 1 ) >> )".toStatement()) } // ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ >> ∨5s e. ( ( 0 + 1 ) .. ( ∨3c + 1 ) ) ( ∨1c ^ ( ( ∨5s - 1 ) + 1 ) ) ) >> .eq(P.c.b.a.mut(Engine::reduceAddition)) >> // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. >> ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ( ( ∨5s - 1 ) + 1 ) >> .eq(P.c.c.c.th(rotSubP)) >> // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. >> ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ( ∨5s - ( 1 - 1 ) ) ) >> .eq(P.c.c.mut(Engine::reduce)) >> // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. >> ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ∨5s ) ) >> .eq(P.a.th(ApSumA) { arrayOf("( ∨1c ^ 0 )".toStatement()) }, >> P.c.th(SumA_pA) { arrayOf("( ∨1c ^ ( ∨3c + 1 ) )".toStatement()) }) // >> ( ( ( ∨1c ^ 0 ) + sum_ ∨2s e. ( ( 0 + 1 ) ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ >> ∨5s e. ( 1 ... ( ( ∨3c + 1 ) - 1 ) ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) >> ) >> .eq(P.a.a.mut(Engine::reduce), P.a.c.b.mut(Engine::reduce), >> P.c.a.b.c.th(rotPSub)) // ( ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c ^ >> ∨2s ) ) - ( sum_ ∨5s e. ( 1 ... ( ∨3c + ( 1 - 1 ) ) ) ( ∨1c ^ ∨5s ) + ( ∨1c >> ^ ( ∨3c + 1 ) ) ) ) >> .eq(P.c.a.b.c.mut(Engine::reduce)) >> // ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( >> sum_ ∨5s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) ) >> .s(rotPSub) >> // ( 1 + ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - ( sum_ >> ∨5s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) >> .c(rotSubSub) >> // ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ >> ∨5s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) ) >> .eq(P.c.a.c.th(Sum_CDV) { arrayOf(i, "( ∨1c ^ $i )".toStatement()) }) >> // ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ >> ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) ) >> .eq(P.c.mut(Engine::reduce)) >> // ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) >> /** done */ >> >> >> >> Here are the goals for Milestone 6 (let's make Mephistolus a concrete >> goal driven development, instead of a feature driven development) : >> >> >> context("Exo 2.7") { >> it("a") { >> val s = "sum_ ∨2s e. ( 1 ... ( ∨1c - 1 ) ) ( ( 5 x. ( 3 ^ -u ∨2s ) ) >> - ( 4 x. ( 2 ^ ( ( 2 x. ∨2s ) - 1 ) ) ) )".toSingle("∨1c e. NN") >> } >> it("b") { >> val s = "sum_ ∨2s e. ( 0 ... ∨1c ) ( ( 1 / 4 ) ^ ( 2 x. ∨2s ) ) >> )".toSingle("∨1c e. NN0") >> } >> it("c") { >> val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ( ( ( ( ∨1c ^ 2 ) x. ∨2s ) + ( >> ∨1c x. ( ∨2s ^ 2 ) ) ) - ( 3 x. ( ∨2s ^ 3 ) ) ) / ( ∨1c ^ 4 ) >> )".toSingle("∨1c e. NN0") >> } >> it("d") { >> val s = "sum_ ∨2s e. ( 0 ... ∨1c ) ( ( ( ( ∨2s x. ( ∨2s - 1 ) ) x. ( >> 3 ^ ∨2s ) ) - ( 5 ^ ( ∨2s - 1 ) ) ) / ( 3 ^ ∨2s ) )".toSingle("∨1c e. NN0") >> } >> it("e") { >> val s = "sum_ ∨2s e. ( 0 ... ( ( 2 x. ∨1c ) - 1 ) ) ( 5 / ( 6 ^ ( >> ∨2s - 1 ) ) )".toSingle("∨1c e. NN0") >> } >> } >> context("Exo 2.10") { >> it("1 (induction)") { >> val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ∨2s x. ( ! ` ∨2s ) ) = ( ( ! ` >> ( ∨2s + 1 ) ) - 1 )".toSingle("∨1c e. NN") >> } >> it("2 (telescopic sums)") { >> val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ∨2s x. ( ! ` ∨2s ) >> )".toSingle("∨1c e. NN") >> } >> } >> >> >> >> Milestone 6 will be reached with 2 other real world proofs involving >> only sums (say Exo2.7a and Exo 2.7b) and for 1 real world proof by >> induction (say Exo 2.10.1) >> >> Best regards, >> Olivier >> >> >> >> >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected] <javascript:>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/3c43167b-f7ad-4eff-b90e-a75460fd5862%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/3c43167b-f7ad-4eff-b90e-a75460fd5862%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6cec5455-65b8-4f9f-b777-37aa6ef7265d%40googlegroups.com.
