Future directions
143 views
Skip to first unread message
ookami
Oct 31, 2019, 1:38:28 PM10/31/19
to Metamath
Now that Christmas is approaching, I would love to come up with my personal
wish list, that I slowly gathered over the past years. Okay, I am not going to
command others here to fulfil my needs. But maybe, one or the other point has
1. The user interface
It is common practice nowadays to separate the UI from the so called backend.
The backend is responsible for carrying out commands issued by the user. The
UI should present the user with an overview of his/her options, and perhaps
allow focussing on particular fields of interest.
Why do you want to have these separated? There are people fantastic at creating
intuitive interfaces. Others are more into abstract thinking, and can provide
fast and reliable libraries. Or incorporate third-party software like search
engines.
The current structure of set.mm has UI elements (in form of htmldef entries),
theorem signatures (i.e hypotheses and statement), and proofs in one single
document, which I consider not optimal.
Here's an existing example, where a separation has been successfully carried out:
chess! See http://www.playwitharena.de/ for a screen shot of an UI. To really play
a game you still need an engine like https://stockfishchess.org/. Both UI and
engine are exchangeable.
If we want to go into this direction, we need to standardize the interface between
frontend and backend. And before we can do that, we need to get an overview of
what capabilities are requested by the users -- that are you!
2. Proof templates
At least in the area where I have worked so far, I more than once encountered a
situation, where I needed a specific instance out of a theorem family, that
wasn't provided. The usual action to get around this deficiency was by
looking out for a nearby solution and introduce otherwise unnecessary
administrative proof steps. A good example is the deduction/immediate/closed form
of a theorem. Wouldn't it be nice to have these forms at hand without much ado?
Apart from this convenience aspect, I would really love to extend parts of FOL to
arbitrary dimensions, as applies to substitution [ z / x ] [ w / y ]... , for example.
The current Metamath language has no means of expressing a proof concept, or template,
that contains instructions how to create a proof for a concrete theorem instance.
I really miss such an abstraction layer.
There are some pitfalls here to note: One should keep a compiled form of a theorem
database, where all these abstract notions are collapsed into instances as needed,
instead of interpreting them over and over again. C++ is an example of a computer
language that follows this idea. The executable is stripped of any helper constructs
the programer might have employed in his working process.
Anyway, is there an idea of how to create a meta language/grammar that fits into this
field?
3. Specialization
The gource video from DAW shows in how many different fields of mathematics
set.mm has put its foot into. These are only the traditional fields, others might
For me it is time to break set.mm up into dedicated subunits. Creating a complete
HTML site of all theorems is already a matter of an hour or so on my computer.
Should't there be some support of specialization? Don't get me wrong here. I think
this is difficult, as it needs some sort of linking process, with all kinds of
conflicts lurking (link against classic or intuitionistic logic? Use theorem A or
B out of different units, one using the axiom of choice, the other not?).
I would love to hear from you how you see the future here.
Kind regards
Wolf
wish list, that I slowly gathered over the past years. Okay, I am not going to
command others here to fulfil my needs. But maybe, one or the other point has
been silently pondered by others as well. So lets see whether this results in a
discussion, or even, finally, something more.
1. The user interface
It is common practice nowadays to separate the UI from the so called backend.
The backend is responsible for carrying out commands issued by the user. The
UI should present the user with an overview of his/her options, and perhaps
allow focussing on particular fields of interest.
Why do you want to have these separated? There are people fantastic at creating
intuitive interfaces. Others are more into abstract thinking, and can provide
fast and reliable libraries. Or incorporate third-party software like search
engines.
The current structure of set.mm has UI elements (in form of htmldef entries),
theorem signatures (i.e hypotheses and statement), and proofs in one single
document, which I consider not optimal.
Here's an existing example, where a separation has been successfully carried out:
chess! See http://www.playwitharena.de/ for a screen shot of an UI. To really play
a game you still need an engine like https://stockfishchess.org/. Both UI and
engine are exchangeable.
If we want to go into this direction, we need to standardize the interface between
frontend and backend. And before we can do that, we need to get an overview of
what capabilities are requested by the users -- that are you!
2. Proof templates
At least in the area where I have worked so far, I more than once encountered a
situation, where I needed a specific instance out of a theorem family, that
wasn't provided. The usual action to get around this deficiency was by
looking out for a nearby solution and introduce otherwise unnecessary
administrative proof steps. A good example is the deduction/immediate/closed form
of a theorem. Wouldn't it be nice to have these forms at hand without much ado?
Apart from this convenience aspect, I would really love to extend parts of FOL to
arbitrary dimensions, as applies to substitution [ z / x ] [ w / y ]... , for example.
The current Metamath language has no means of expressing a proof concept, or template,
that contains instructions how to create a proof for a concrete theorem instance.
I really miss such an abstraction layer.
There are some pitfalls here to note: One should keep a compiled form of a theorem
database, where all these abstract notions are collapsed into instances as needed,
instead of interpreting them over and over again. C++ is an example of a computer
language that follows this idea. The executable is stripped of any helper constructs
the programer might have employed in his working process.
Anyway, is there an idea of how to create a meta language/grammar that fits into this
field?
3. Specialization
The gource video from DAW shows in how many different fields of mathematics
set.mm has put its foot into. These are only the traditional fields, others might
want to use ZFC in future to create abstract graph structures like trees, maps. I am
pretty sure, there is much more than that conceivable.
For me it is time to break set.mm up into dedicated subunits. Creating a complete
HTML site of all theorems is already a matter of an hour or so on my computer.
Should't there be some support of specialization? Don't get me wrong here. I think
this is difficult, as it needs some sort of linking process, with all kinds of
conflicts lurking (link against classic or intuitionistic logic? Use theorem A or
B out of different units, one using the axiom of choice, the other not?).
I would love to hear from you how you see the future here.
Kind regards
Wolf
Giovanni Mascellani
Oct 31, 2019, 3:04:05 PM10/31/19
to 'ookami' via Metamath
Hi,
Il 31/10/19 18:38, 'ookami' via Metamath ha scritto:
of things I'd like to implement, and every now and then I have some time
to work on them in the context on my project mmpp[1], but unfortunately
I also have many other things to care about. I wish to win a post-doc
target at working on these things, but I wouldn't know where to start from.
[1] https://gitlab.com/giomasce/mmpp/
> 1. The user interface
>
> It is common practice nowadays to separate the UI from the so called
> backend. The backend is responsible for carrying out commands issued
> by the user. The UI should present the user with an overview of
> his/her options, and perhaps allow focussing on particular fields of
> interest.
>
> Why do you want to have these separated? There are people fantastic
> at creating intuitive interfaces. Others are more into abstract
> thinking, and can provide fast and reliable libraries. Or
> incorporate third-party software like search engines.
In mmpp I have both proof generators and a UI. They are in the same
repository, and in line of principle I tried to make them somehow
independent. The situation, as everything in mmpp, is far from ideal.
However I think the UI has some (very) little merit: it shows the proof
in a tree form, where branches can be collapsed and expanded depending
on what you want to focus on; you can write Metamath code in an input
field and the corresponding HTML rendering immediately appears just
close to it, in order to make it easier to read. The backend
automatically tries to resolve each step using a list of strategies. One
of the strategies is the usual unification algorithm; but there are
other more complex proof generators. One proof generator automatically
solves steps that are just applications of propositional calculus (and
is responsible for monstruosities like [2]; notice that in the whole
subproof rooted at step 457 only propositional theorems are used).
Another proof generator should at some point become an implementation of
Holophrasm[3], but it is not yet complete and it doesn't do any ML;
still, every now and then it chimes in and complete little parts of the
proof for free. I have been working on another generator that tries to
automatically solve predicate calculus steps by feeding them to an ATP
like E[4] and using GAPT[5] to interpret the proof and convert it to ND
style. Most of the code is already there and I am already able to
convert proofs to Metamath, but some glue code that makes this available
to the UI is still missing.
[2] http://us.metamath.org/mpeuni/sbcom3OLD.html
[3] https://github.com/dwhalen/holophrasm
[4] https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html
[5] https://www.logic.at/gapt/
I think I like how in Metamath (at least, in mmpp, but also in mmj2)
what the user does is writing statements and leave it to the program the
find unifications or otherwise solve the step; while in other systems,
like Coq and Lean, which I am trying to learn, you mostly write theorem
names (for example with "rewrite" or "apply" tactics) and the program
computes the expressions. I like writing expressions more than writing
previous theorem names (provided that I have appropriate copy and paste
tools), because I don't remember the theorem names.
> 2. Proof templates
>
> At least in the area where I have worked so far, I more than once
> encountered a situation, where I needed a specific instance out of a
> theorem family, that wasn't provided. The usual action to get around
> this deficiency was by looking out for a nearby solution and
> introduce otherwise unnecessary administrative proof steps. A good
> example is the deduction/immediate/closed form of a theorem.
> Wouldn't it be nice to have these forms at hand without much ado?
>
> Apart from this convenience aspect, I would really love to extend
> parts of FOL to arbitrary dimensions, as applies to substitution [ z
> / x ] [ w / y ]... , for example. The current Metamath language has
> no means of expressing a proof concept, or template, that contains
> instructions how to create a proof for a concrete theorem instance. I
> really miss such an abstraction layer.
I agree with both, and for both at some point I started some work in
mmpp, although nothing is usable yet. I would like rewriting and
substituting to be much easier in Metamath, without having to go through
the whole structure of the assertion (i.e., letting the program go
through it instead of you).
> 3. Specialization
>
> The gource video from DAW shows in how many different fields of
> mathematics set.mm has put its foot into. These are only the
> traditional fields, others might want to use ZFC in future to create
> abstract graph structures like trees, maps. I am pretty sure, there
> is much more than that conceivable.
>
> For me it is time to break set.mm up into dedicated subunits.
> Creating a complete HTML site of all theorems is already a matter of
> an hour or so on my computer. Should't there be some support of
> specialization? Don't get me wrong here. I think this is difficult,
> as it needs some sort of linking process, with all kinds of conflicts
> lurking (link against classic or intuitionistic logic? Use theorem A
> or B out of different units, one using the axiom of choice, the other
> not?).
Here the thing I'd really like to see is namespacing, although that
would be a change in the language, not just of the way we use it. It
would change the core Metamath inference model based on substitution, it
would just change the way things are named.
Just my two cents. I'd like to write code (and proofs) instead of ideas,
but that is what I can do for the moment.
Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles
Il 31/10/19 18:38, 'ookami' via Metamath ha scritto:
> Now that Christmas is approaching, I would love to come up with my
> personal wish list, that I slowly gathered over the past years.
> Okay, I am not going to command others here to fulfil my needs. But
> maybe, one or the other point has been silently pondered by others as
> well. So lets see whether this results in a discussion, or even,
> finally, something more.
The issues you mention make a lot of sense to me. I also have a wishlist
> personal wish list, that I slowly gathered over the past years.
> Okay, I am not going to command others here to fulfil my needs. But
> maybe, one or the other point has been silently pondered by others as
> well. So lets see whether this results in a discussion, or even,
> finally, something more.
of things I'd like to implement, and every now and then I have some time
to work on them in the context on my project mmpp[1], but unfortunately
I also have many other things to care about. I wish to win a post-doc
target at working on these things, but I wouldn't know where to start from.
[1] https://gitlab.com/giomasce/mmpp/
> 1. The user interface
>
> It is common practice nowadays to separate the UI from the so called
> backend. The backend is responsible for carrying out commands issued
> by the user. The UI should present the user with an overview of
> his/her options, and perhaps allow focussing on particular fields of
> interest.
>
> Why do you want to have these separated? There are people fantastic
> at creating intuitive interfaces. Others are more into abstract
> thinking, and can provide fast and reliable libraries. Or
> incorporate third-party software like search engines.
repository, and in line of principle I tried to make them somehow
independent. The situation, as everything in mmpp, is far from ideal.
However I think the UI has some (very) little merit: it shows the proof
in a tree form, where branches can be collapsed and expanded depending
on what you want to focus on; you can write Metamath code in an input
field and the corresponding HTML rendering immediately appears just
close to it, in order to make it easier to read. The backend
automatically tries to resolve each step using a list of strategies. One
of the strategies is the usual unification algorithm; but there are
other more complex proof generators. One proof generator automatically
solves steps that are just applications of propositional calculus (and
is responsible for monstruosities like [2]; notice that in the whole
subproof rooted at step 457 only propositional theorems are used).
Another proof generator should at some point become an implementation of
Holophrasm[3], but it is not yet complete and it doesn't do any ML;
still, every now and then it chimes in and complete little parts of the
proof for free. I have been working on another generator that tries to
automatically solve predicate calculus steps by feeding them to an ATP
like E[4] and using GAPT[5] to interpret the proof and convert it to ND
style. Most of the code is already there and I am already able to
convert proofs to Metamath, but some glue code that makes this available
to the UI is still missing.
[2] http://us.metamath.org/mpeuni/sbcom3OLD.html
[3] https://github.com/dwhalen/holophrasm
[4] https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html
[5] https://www.logic.at/gapt/
I think I like how in Metamath (at least, in mmpp, but also in mmj2)
what the user does is writing statements and leave it to the program the
find unifications or otherwise solve the step; while in other systems,
like Coq and Lean, which I am trying to learn, you mostly write theorem
names (for example with "rewrite" or "apply" tactics) and the program
computes the expressions. I like writing expressions more than writing
previous theorem names (provided that I have appropriate copy and paste
tools), because I don't remember the theorem names.
> 2. Proof templates
>
> At least in the area where I have worked so far, I more than once
> encountered a situation, where I needed a specific instance out of a
> theorem family, that wasn't provided. The usual action to get around
> this deficiency was by looking out for a nearby solution and
> introduce otherwise unnecessary administrative proof steps. A good
> example is the deduction/immediate/closed form of a theorem.
> Wouldn't it be nice to have these forms at hand without much ado?
>
> Apart from this convenience aspect, I would really love to extend
> parts of FOL to arbitrary dimensions, as applies to substitution [ z
> / x ] [ w / y ]... , for example. The current Metamath language has
> no means of expressing a proof concept, or template, that contains
> instructions how to create a proof for a concrete theorem instance. I
> really miss such an abstraction layer.
mmpp, although nothing is usable yet. I would like rewriting and
substituting to be much easier in Metamath, without having to go through
the whole structure of the assertion (i.e., letting the program go
through it instead of you).
> 3. Specialization
>
> The gource video from DAW shows in how many different fields of
> mathematics set.mm has put its foot into. These are only the
> traditional fields, others might want to use ZFC in future to create
> abstract graph structures like trees, maps. I am pretty sure, there
> is much more than that conceivable.
>
> For me it is time to break set.mm up into dedicated subunits.
> Creating a complete HTML site of all theorems is already a matter of
> an hour or so on my computer. Should't there be some support of
> specialization? Don't get me wrong here. I think this is difficult,
> as it needs some sort of linking process, with all kinds of conflicts
> lurking (link against classic or intuitionistic logic? Use theorem A
> or B out of different units, one using the axiom of choice, the other
> not?).
would be a change in the language, not just of the way we use it. It
would change the core Metamath inference model based on substitution, it
would just change the way things are named.
Just my two cents. I'd like to write code (and proofs) instead of ideas,
but that is what I can do for the moment.
Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles
Norman Megill
Oct 31, 2019, 8:10:43 PM10/31/19
to Metamath
On Thursday, October 31, 2019 at 1:38:28 PM UTC-4, ookami wrote:
Now that Christmas is approaching, I would love to come up with my personal
wish list, that I slowly gathered over the past years. Okay, I am not going to
command others here to fulfil my needs. But maybe, one or the other point hasbeen silently pondered by others as well. So lets see whether this results in adiscussion, or even, finally, something more.
I'll make a few comments mostly related to current software. Others can comment on some of your more visionary ideas.
1. The user interface
It is common practice nowadays to separate the UI from the so called backend.
The backend is responsible for carrying out commands issued by the user. The
UI should present the user with an overview of his/her options, and perhaps
allow focussing on particular fields of interest.
Why do you want to have these separated? There are people fantastic at creating
intuitive interfaces. Others are more into abstract thinking, and can provide
fast and reliable libraries. Or incorporate third-party software like search
engines.
The current structure of set.mm has UI elements (in form of htmldef entries),
theorem signatures (i.e hypotheses and statement), and proofs in one single
document, which I consider not optimal.
The $t comment where htmldefs are stored (about 250K in size or 0.7% of set.mm) is currently produced as a separate module 'set-typeset.mm' when you use 'write source set.mm /split', and like other modules it can be worked on independently from the rest of set.mm. (BTW 'help verify markup' has a link to the modularization tag spec for /split.)
Here's an existing example, where a separation has been successfully carried out:
chess! See http://www.playwitharena.de/ for a screen shot of an UI. To really play
a game you still need an engine like https://stockfishchess.org/. Both UI and
engine are exchangeable.
If we want to go into this direction, we need to standardize the interface between
frontend and backend. And before we can do that, we need to get an overview of
what capabilities are requested by the users -- that are you!
2. Proof templates
At least in the area where I have worked so far, I more than once encountered a
situation, where I needed a specific instance out of a theorem family, that
wasn't provided. The usual action to get around this deficiency was by
looking out for a nearby solution and introduce otherwise unnecessary
administrative proof steps. A good example is the deduction/immediate/closed form
of a theorem. Wouldn't it be nice to have these forms at hand without much ado?
For most new theorems in set theory and beyond, the convention has become to use Mario's deduction form. The closed and inference forms can be obtained from these almost immediately inside of a proof, so usually there is no need to state them as separate theorems. For a heavily-used theorem, a separate form might be justified if there is sufficient proof size savings, but that could be done as a separate maintenance activity for theorems with high usage.
Apart from this convenience aspect, I would really love to extend parts of FOL to
arbitrary dimensions, as applies to substitution [ z / x ] [ w / y ]... , for example.
The current Metamath language has no means of expressing a proof concept, or template,
that contains instructions how to create a proof for a concrete theorem instance.
I really miss such an abstraction layer.
There are some pitfalls here to note: One should keep a compiled form of a theorem
database, where all these abstract notions are collapsed into instances as needed,
instead of interpreting them over and over again. C++ is an example of a computer
language that follows this idea. The executable is stripped of any helper constructs
the programer might have employed in his working process.
Anyway, is there an idea of how to create a meta language/grammar that fits into this
field?
3. Specialization
The gource video from DAW shows in how many different fields of mathematics
set.mm has put its foot into. These are only the traditional fields, others mightwant to use ZFC in future to create abstract graph structures like trees, maps. I ampretty sure, there is much more than that conceivable.
For me it is time to break set.mm up into dedicated subunits.
'write source ... /split' produces modules as specialized as you care to make them. Each module can be read by itself and include only those previous modules that are needed.
Creating a complete
HTML site of all theorems is already a matter of an hour or so on my computer.
You can specify a statement range to create a portion of the site; e.g., 'show statement ax-1~df-ex /alt_html' will produce all of propositional calculus (and a couple of predicate calculus statements).
fl
Nov 1, 2019, 9:30:12 AM11/1/19
to meta...@googlegroups.com
The current structure of set.mm has UI elements (in form of htmldef entries),
theorem signatures (i.e hypotheses and statement), and proofs in one single
document, which I consider not optimal.
Here's an existing example, where a separation has been successfully carried out:
chess! See http://www.playwitharena.de/ for a screen shot of an UI. To really play
a game you still need an engine like https://stockfishchess.org/. Both UI and
engine are exchangeable.
If we want to go into this direction, we need to standardize the interface between
frontend and backend. And before we can do that, we need to get an overview of
what capabilities are requested by the users -- that are you!
If there is a graphic user interface to create, it is one for kids. How creating something that would be suitable
for the adolescents to initiate themselves to logic and formal mathematics? The interface should keep
the most interesting intuitions in Metamath (its human-checkable algorithm of substitution mainly,
its transparent management, its proximity with the formal definitions of logic) while removing the most
detering features: variable proper substitution mostly.
Along this path, natural deduction (with a context, not with a stack) would certainly be a mandatory element.
--
FL
vvs
Nov 1, 2019, 12:26:33 PM11/1/19
to Metamath
I don't see any problem with existing verifiers - there are plenty for every taste already. It's the UI that always falls behind. And it seems that there is consensus that it should be based on ND. But the question is: can UI champion be found among theorists?
Giovanni Mascellani
Nov 1, 2019, 6:06:00 PM11/1/19
to meta...@googlegroups.com
Il 01/11/19 17:26, vvs ha scritto:
seemed to me a good one to work on Metamath. The result is the mmpp I
have described in my last email. As I said, I am not a UI champion, so
do not expect too much.
But I wonder: supposing that we had someone willing to implement
whatever interface we would like, what would we ask him? What are the
ways people expect to be comfortable with for editing Metamath proofs or
statements? I am very curious to know what people on this list think.
> But the question is: can UI champion be found among theorists?
I am not a UI champion, but I have tried to come up with an UI that
seemed to me a good one to work on Metamath. The result is the mmpp I
have described in my last email. As I said, I am not a UI champion, so
do not expect too much.
But I wonder: supposing that we had someone willing to implement
whatever interface we would like, what would we ask him? What are the
ways people expect to be comfortable with for editing Metamath proofs or
statements? I am very curious to know what people on this list think.
vvs
Nov 1, 2019, 7:40:31 PM11/1/19
to Metamath
Thanks for the interest in this subject. It's surely tempting to try mmpp at some point in the future.
As for UI I think that the most important thing is that it should be adaptive to users progress. That is it should give a list of possible theorems to use depending on the context and this list should be presented in some creative form. It's a vague description, but without some better real world examples it is best description I could imagine. Introducing some visual elements for stimulating geometric intuition and using mouse might be a good idea. I admit that I was impressed by incredible.pm interface and Jape's Fitch boxes in its UI. As Frederic pointed out earlier there is interesting http://proofs.openlogicproject.org/. There are other browser based proof editors as well.
Sorry if this doesn't make much sense.
Olivier Binda
Nov 2, 2019, 5:27:23 AM11/2/19
to meta...@googlegroups.com
Regarding slapping an UI/Ide over Metamath/MM0
The current format of set.mm doesn't prevent slapping an UI on metamath (you can just parse the whole file and throw away what you don't want)
But, for sure, some things can be done (or have already been done and I'm just not aware of them) to make the process easier
There are a few ongoing attemps to do so
mmpp (Giovanni)
mm0, mm1 and the visual studio plugin (Mario)
mmj2
metamath solitaire ? metamath programm ?
... a few other that I don't know about
The current format of set.mm doesn't prevent slapping an UI on metamath (you can just parse the whole file and throw away what you don't want)
But, for sure, some things can be done (or have already been done and I'm just not aware of them) to make the process easier
There are a few ongoing attemps to do so
mmpp (Giovanni)
mm0, mm1 and the visual studio plugin (Mario)
mmj2
metamath solitaire ? metamath programm ?
... a few other that I don't know about
I'm also going at it too with Mephistolus (closed source, free to use without crap forever, but sadly only available for me at this point (I'm working to make it usefull and available))
I have a different take on the subject as
most ui/ide want the user to write a source and a destination metamath statement and fill the gaps automatically (unification), with some hints
Basically, the software has to compute the way to go from source to target (it is really hard, with a lot of combinatorial computations)
It requires a lot of mathematical skills as you have to be able to write where you want to end up
In Mephistolus, the user starts from some metamath statement and slowly modifies it with theorems/operations (associativity, commutativity, computation reduction, tacticts...) to reach a goal
Basically, the human gives the directions and the computer does all it can to avoid him the hassle of proving trivial/not too hard stuff
It doesn't require math skills as it could be as simple as clicking (or touching) a part of an equation, and then selecting the desired change, in a window that appears (the computer computes all possible results available on applying an operation on this part of the statement)
I believe that it solves what fl has spoken of : with the right UI, Mephistolus would make a 12 years old able to use metamath powered maths
Now, slapping a GOOD UI over Metamath is not as easy as it sounds :
The coding a screen with drag and drop, touch/gestures support, windows is quite doable in a few weeks.
But what happens when you click a button, or drag something isn't.
The UI has to apply transformations on the metamath statements and execute some proof steps and this is what is really hard : you might have a shiny UI but you still have to make it do metamath magic.
So the backend library is what really important. If you don't have one, it is useless to start coding an UI (which is why I haven't even tryied to do it yet, I'm focusing on the math api first)
Other point to consider would be, on what platform do you want your metamath UI ?
Android phones/tablet/ios phone/tablets,windows/mac/linux/unix/native code/the jvm/the web (browser ?)
Mephistolus is aiming at all those targets
BUT
it needs all it's components to be available for those targets
metamath core library : available (it only requires strings/trees)
parsing metamath statements : soon (or already) available as there is a work in progress to make mutli-platform kotlin be a target for antlr : https://github.com/ftomassetti/antlr-kotlin
database/indexing : ouch, here it hurts. Be it graph database (JanusGraph) or indexing libraries (lucene), none of them are available on all platforms, the one I know work on the java virtual machine (JVM) which means taht they are available on the JVM/android but I'm waiting for them to be ported to kotlin (I expect, at one point in time, that all usefull libraries will be ported to kotlin). OR alternative would have to be plugged and maintained for all targets
UI : ouch,it hurts here too : be it Jetpack Compose/Flutter/JavaFx there is no single UI Library available for all targets (waiting for something good, in this space too)
Regarding metamath for metamath experts, something can already be done today (you just need the jvm target, and everything needed is already there today)
In the next months, I'll try to completely prove in metamaths all Mephistolus theorems that I have been using to this day (I have done most of the work already, but now I'm starting to encounter harder stuff (fsumshift ^^)).
Which will make mephistolus usefull for Metamath experts as it will be able to export to metamath all proofs done in mephistolus
And I'll release a raw programm (just text input, no fancy UI) that will enable you to do usefull work in metamath with it
It remains to be seen if you'll like the metamath proofs it produces (you want short, right :) ). But who knows, what value Mephistolus could bring you ? (I have hopes but I won't know before I try :) )
So, still working on backend stuff for the next months/years before coding an UI. :)
I have a different take on the subject as
most ui/ide want the user to write a source and a destination metamath statement and fill the gaps automatically (unification), with some hints
Basically, the software has to compute the way to go from source to target (it is really hard, with a lot of combinatorial computations)
It requires a lot of mathematical skills as you have to be able to write where you want to end up
In Mephistolus, the user starts from some metamath statement and slowly modifies it with theorems/operations (associativity, commutativity, computation reduction, tacticts...) to reach a goal
Basically, the human gives the directions and the computer does all it can to avoid him the hassle of proving trivial/not too hard stuff
It doesn't require math skills as it could be as simple as clicking (or touching) a part of an equation, and then selecting the desired change, in a window that appears (the computer computes all possible results available on applying an operation on this part of the statement)
I believe that it solves what fl has spoken of : with the right UI, Mephistolus would make a 12 years old able to use metamath powered maths
Now, slapping a GOOD UI over Metamath is not as easy as it sounds :
The coding a screen with drag and drop, touch/gestures support, windows is quite doable in a few weeks.
But what happens when you click a button, or drag something isn't.
The UI has to apply transformations on the metamath statements and execute some proof steps and this is what is really hard : you might have a shiny UI but you still have to make it do metamath magic.
So the backend library is what really important. If you don't have one, it is useless to start coding an UI (which is why I haven't even tryied to do it yet, I'm focusing on the math api first)
Other point to consider would be, on what platform do you want your metamath UI ?
Android phones/tablet/ios phone/tablets,windows/mac/linux/unix/native code/the jvm/the web (browser ?)
Mephistolus is aiming at all those targets
BUT
it needs all it's components to be available for those targets
metamath core library : available (it only requires strings/trees)
parsing metamath statements : soon (or already) available as there is a work in progress to make mutli-platform kotlin be a target for antlr : https://github.com/ftomassetti/antlr-kotlin
database/indexing : ouch, here it hurts. Be it graph database (JanusGraph) or indexing libraries (lucene), none of them are available on all platforms, the one I know work on the java virtual machine (JVM) which means taht they are available on the JVM/android but I'm waiting for them to be ported to kotlin (I expect, at one point in time, that all usefull libraries will be ported to kotlin). OR alternative would have to be plugged and maintained for all targets
UI : ouch,it hurts here too : be it Jetpack Compose/Flutter/JavaFx there is no single UI Library available for all targets (waiting for something good, in this space too)
Regarding metamath for metamath experts, something can already be done today (you just need the jvm target, and everything needed is already there today)
In the next months, I'll try to completely prove in metamaths all Mephistolus theorems that I have been using to this day (I have done most of the work already, but now I'm starting to encounter harder stuff (fsumshift ^^)).
Which will make mephistolus usefull for Metamath experts as it will be able to export to metamath all proofs done in mephistolus
And I'll release a raw programm (just text input, no fancy UI) that will enable you to do usefull work in metamath with it
It remains to be seen if you'll like the metamath proofs it produces (you want short, right :) ). But who knows, what value Mephistolus could bring you ? (I have hopes but I won't know before I try :) )
So, still working on backend stuff for the next months/years before coding an UI. :)
Olivier Binda
Nov 3, 2019, 3:43:05 AM11/3/19
to meta...@googlegroups.com
I drew a blacker picture than necessary regarding the state of UI library for Metamath :
So, I would say that, though slapping a UI on metamath requires a lot of work, it should be possible to do a decent job now (provided that the metamath magic is there)
Also, metamath experts don't necessarily require math rendering with Tex-like beauty as they can decipher metamath statements natively.
Regular text widgets would be sufficient for experts (but my target is people that learn maths, so... mathjax is a necessity for me :) )
Best regards,
Olivier
There is one UI library widely available that we can use : the WebView.
It is also necessary as MathJax is the only library I know that is able to render Math with Tex-like capabilities
Using a WebView (and javascript, mathml, mathJax) is a complex solution (that I used in the past to develop a math app on android),
quite slow... but that works really well and that might probably enable selection of parts of equations through touch/clicks (never tried that, might be possible).
Which leaves regular html widget to draw buttons, lists, ...
The WebView is available on android/ios/a browser (obviously) and is embeddable in a native app, so that would solve the UI problem
As javascript would be a component of the app, we would need to find a database/graph/indexing library that work on javascript (if there is no option on kotlin).
But, as of today, regular HashMap or simple data structures might be succifient to do (at first) a decent job regarding the database problem
(at the moment, I use a simple hashmap and list in Kotlin to query metamath theorems, it is sufficient for my needs)
It is also necessary as MathJax is the only library I know that is able to render Math with Tex-like capabilities
Using a WebView (and javascript, mathml, mathJax) is a complex solution (that I used in the past to develop a math app on android),
quite slow... but that works really well and that might probably enable selection of parts of equations through touch/clicks (never tried that, might be possible).
Which leaves regular html widget to draw buttons, lists, ...
The WebView is available on android/ios/a browser (obviously) and is embeddable in a native app, so that would solve the UI problem
As javascript would be a component of the app, we would need to find a database/graph/indexing library that work on javascript (if there is no option on kotlin).
But, as of today, regular HashMap or simple data structures might be succifient to do (at first) a decent job regarding the database problem
(at the moment, I use a simple hashmap and list in Kotlin to query metamath theorems, it is sufficient for my needs)
So, I would say that, though slapping a UI on metamath requires a lot of work, it should be possible to do a decent job now (provided that the metamath magic is there)
Also, metamath experts don't necessarily require math rendering with Tex-like beauty as they can decipher metamath statements natively.
Regular text widgets would be sufficient for experts (but my target is people that learn maths, so... mathjax is a necessity for me :) )
Best regards,
Olivier
Reply all
Reply to author
Forward
0 new messages