George Hotz, a 5+ hours video complaining about Metamath, with 14000+ views and 163 thumb up

[Glauco]

I was googling for a video about Emetamath, Thierry's plugin, but I found this recent video, that caught my attention:

https://www.youtube.com/watch?v=hKi9Q3S1Nsg

The title is "George Hotz | Programming | twitchcoq : pt 3, mostly I want to complain about metamath"

I'm having a late night "dinner", so I've not had time to understand the whole story yet, but it looks like George (a well-known hacker, you can read about his life on Wikipedia) has streamed and recorded a number of multi hours videos (this is the third one) about him programming a parser for Metamath (he read the Metamath book just before the videos).

I've had time to look at the first few minutes, where he complains about set.mm

Glauco

[Jim Kingdon]

Hmm, two thoughts:

1. If reading is more your thing than video, you can get some idea of what this is about from
https://github.com/geohot/twitchcoq

2. Do videos on formal proofs, whether coq or Isabelle or lean or (fill in the blank), whether positive or negative, ever get 14,000 views? Sounds like a lot for a topic which is still off the beaten path for a lot of people.

[ookami]

Thanks for the link, Glauco.

I followed this video up to 2:00:00, and had an editor open to scribble down some notes while I was watching.  Here are the results.  Please note, these are impressions made on the fly, and perhaps not well thought over.

1. Metamath hype: Why on earth is someone like George Hotz interested in Metamath at all? There seems to be a hype around, judging from his first words.

2. Cryptic labels: He is ranting while faced with theorem names on the HTML page of sqr2irr.  No clue whatsoever what they mean.  Compares this to more explicit names found in competing products, and in program code in general.  I think there is indeed headroom for improvement here. Maybe a pop up showing an explanation while hovering over a name alleviates the situation.

3. No directories, just a global scope.  Yes, this is a drawback in my eyes, too.  But this is not an easy task as it seems at first sight.  If you take this idea seriously, i.e. topics are finally independent, you end up with a need for a linker infrastructure.  Compare to compiler.

4. Not conforming to standards.  At various occasions he struggles with details just because they do not meet his expectations. Syntax for example

5. He somehow got lost in the gory technical details of strict proof syntax and verification.  But the core idea of a Metamath proof is applying patterns to symbol strings.  He seems not always be aware of this 'bird eye view'.  I remember when I first looked into Metamath I was not in the least interested in details like how variables are defined.  In fact, I was not concerned with program details at all.  I was satisfied to know how to replay a proof by hand.  Once I learned the top level formalism, I could easily imagine a stack like structure for some automatic verification.
6 Human interface of the Metamath program.  Tries out common commands at random, does not use the help feature.  No GUI.
7. He feels at ease when he detects the formal syntax description of the Metamath language,and elaborates on implementing it in a Python parser.  Here he is on firm grounds and starts exploring Metamath.  Unfortunately, this distracts him from the core idea, in my eyes, see 5. Frog's eye view.

Wolf Lammen

[vvs]

1. Metamath hype: Why on earth is someone like George Hotz interested in Metamath at all? There seems to be a hype around, judging from his first words.

Let's use Occam razor. Why on earth anybody would be interested in Metamath which is even more obscure than Coq or Lean? Was there a hype to attract someone here? Ok, there was Metamath book. I read it, he read it too. Is that a hype? People want to understand mathematics and proofs. They found known textbooks not satisfactory. In fact even some mathematicians find it not satisfactory and they turn to Lean, Coq or Metamath. Were they following a hype? I would call this a movement (e.g. https://xenaproject.wordpress.com), because these people know what they are searching for.

And I can only say it again: Metamath is as good as it gets to render existing proofs, but there is neither good assistant nor automation for newbie to create new ones. There is nothing new at all.

[savask]

I watched though the video and spotted a few things not mentioned in Wolf's notes.

At around 1:02 (1 hour 2 minutes), he starts writing a grammar file based on the EBNF in the Metamath book. The book uses dashes inside symbols on the left hand side of each rule, which is apparently not shared by all EBNF standards, so he has to replace them by underscores. GNU bison supports dashes (but calls it a GNU extension, incompatible with POSIX Yacc), Happy parser verifier (for Haskell) also doesn't allow dashes in symbol names. Maybe it is worthwhile replacing dashes by underscores in the Metamath book EBNF? It may save someone time, in case if they would like to simply copy the grammar file from the book.

At 5:02, he tries mmj2. Apparently there's some sort of trouble launching it on the MacOS (he had to modify the starting script), so maybe that bug should be fixed.

My impression is that most of his complaints come from missing proof-assisting capabilities of the metamath program and mmj2, but main points stand of course. Our tooling is scarce and most of work is done manually anyway. On the other hand, the video has quite a lot of praise for the Metamath book and the design of the language itself (stressing its simplicity), so Metamath clearly has its strong points in comparison with other proof systems.

[Norman Megill]

Thanks for posting your impressions.  I'm not quite sure what to make of it all yet, but it would be interesting to hear more of what people think.

Looking at his YouTube home page, he posted 5 related videos about a month ago.  His exploration of Metamath seems to start in the middle of the 2nd video.

1. "twitchcoq, writing a language we can prove things in"
https://www.youtube.com/watch?v=VTFaWOPspEo  (8 hrs)

2. "twitchcoq :  pt 2, can we prove true is not false | Coq (software)"
https://www.youtube.com/watch?v=-zf8gU0Y5WU (4 hrs)

3. "twitchcoq : pt 3, mostly I want to complain about metamath"
https://www.youtube.com/watch?v=hKi9Q3S1Nsg (5+ hrs)

4. "twitchcoq pt 4, metamath says 2+2=4 | pt 5, program search"
https://www.youtube.com/watch?v=OAXjsUZoOgo (7.5 hrs)

5. "obscure languages sunday : LEAN metamath parser"
https://www.youtube.com/watch?v=4Or-5OLCNDA (6 hrs)

I looked only at brief excerpts so far.  In the second video, after playing mostly with Coq, his curiosity about Metamath seems to start at 2:27:12 when he says, "Metamath zero? What's metamath zero?" although I can't tell what he's looking at.  Then from a Google search, he looks at Mario's arxiv abstract page, then the Hacker News article, and says "This might be a better base.  Coq might be too complex."  At 2:28:17 he starts playing David's Gource video and says "That is(?) really cool" and "Wow, Metamath's been around forever".  I haven't watched the remaining 1.5 hrs.

Norm

[David Starner]

On Sun, Dec 22, 2019 at 4:58 AM vvs <vvs...@gmail.com> wrote:
> Why on earth anybody would be interested in Metamath which is even more obscure than Coq or Lean?

Is it? I've heard of Lean, vaguely, but not really. I've looked at
Coq, and would probably pick it up if I needed to formally prove a
program, but nothing beats the Metamath website for sheer promise from
a mathematical perspective. Maybe in a academic setting, the others
are well-known, but to a general audience interested in mathematics, I
don't see any real alternative to Metamath.

--
Kie ekzistas vivo, ekzistas espero.

[Mario Carneiro]

There is a follow up video https://youtu.be/OAXjsUZoOgo (7 hours!), where he attempts to prove 2+2 = 4 using the axiomatization of peano.mm. This was an unfortunate choice, because peano.mm has a bizarre axiomatization, uses polish notation for no apparent reason, and has *no theorems*, meaning that even the most basic propositional logic is not available without a huge effort. If the addition axioms had been stated with term variables the proof of 2+2=4 would have been relatively straightforward, but instead he spends several hours trying to come to grips with peano.mm's idiosyncratic predicate logic formalization. And of course like any programmer he periodically google searches for things and of course comes up empty. Even searching for "metamath ide" multiple times yielded pretty inconclusive results, with some asteroid meta stuff pointing to a geocities dead link about mmide... Somehow we have to clean up our story here.

I don't have a MacOS machine so I would appreciate the attention of someone who knows their way around one to set up the scripts. The readme on github is actually borrowed directly from Mel's original readme, and is woefully out of date. Any scripts that I don't use are likely to have bit-rotted. He had to remove the -Xincgc option from the java call, and then it ran out of memory on set.mm. Possibly the memory limits in the script are out of date?

This is a really good view at the newbie experience, from someone with a LOT of perseverence. The biggest question on his mind most of the time seems to be "how do people write this?" He's absolutely right that the syntax of metamath is almost adversarial, and he spends a lot of time constructing expressions in the pt 4 video by hand. I think we need to find a way to present this so that we don't ever give the impression that proof blocks are written by humans. He spends his time on miu.mm, then peano.mm, because these are the smallest databases, but I think this is unfortunate because they are both rather unusual by metamath standards. set.mm would have been an optimal starting point, except it's HUGE, which makes introductory stuff harder. Even worse, it starts with a comment that is tens of thousands of lines long, which makes it very difficult to see how "baby's first propositional logic" is supposed to go.

I think we should try to curate a small selection of set.mm propositional logic and predicate logic, enough so that you have all the main theorems but not going for absolute saturation, with interstitial "tutorial" comments explaining the anatomy of an mm file along the way.

Mario

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b2f84723-5ae7-4889-9403-176463bb5fb6%40googlegroups.com.

[vvs]

I think we should try to curate a small selection of set.mm propositional logic and predicate logic, enough so that you have all the main theorems but not going for absolute saturation, with interstitial "tutorial" comments explaining the anatomy of an mm file along the way.

Exactly. Look at Kevin Buzzard's natural number game along these lines - that's the best introduction to Lean's tactical framework. But you should have known it already. BTW, according to Thurston's paper cited in that Buzzard's blog, the best way to disseminate mathematical knowledge is from first-hand experience.

[vvs]

> Why on earth anybody would be interested in Metamath which is even more obscure than Coq or Lean?

Is it? I've heard of Lean, vaguely, but not really. I've looked at
Coq, and would probably pick it up if I needed to formally prove a
program, but nothing beats the Metamath website for sheer promise from
a mathematical perspective. Maybe in a academic setting, the others
are well-known, but to a general audience interested in mathematics, I
don't see any real alternative to Metamath.

What's the most surprising in such discussions is how little people in the field know about each other. If you look at Coq's community they know very little about Lean and vice versa, and both know almost nothing about Metamath. It looks like the best way to dispel superstitions is to post about Metamath on Hacker's news where they are discussing some Lean related talk. And I think David and Mario deserve much credit for popularizing Metamath on different forums.

[ookami]

I left a comment under Hotz's video and invited him to visit this thread.  If we are lucky, we will see his ideas here.

Wolf Lammen

[Jon P]

> I left a comment under Hotz's video and invited him to visit this thread.  If we are lucky, we will see his ideas here.  

That sounds like a nice idea, it might be nice to reach out to him a bit more formally. I'd be willing to answer questions if he has them and I'm sure there's a bunch more people who know much more than me who would too.

I think the reason he is doing this is this project he is doing. 

http://backspace.ai/

I agree that metamath is an awesome starting place for formal logic and so it would be cool if he got into it. There is a contact on that page and I imagine it's better if someone more important than me emails him though I am happy to if no one else is interested. 

[Mario Carneiro]

The videos on youtube are from the "commaai archive", which as mentioned in the description is not affiliated with comma.ai or George Hotz. I wasn't able to find an email for him, but I sent him a message via a PR to the twitchcoq repository (solving the 2p2e4 proof that he got stuck on). With any luck he will pop up on this thread.

On Sun, Dec 22, 2019 at 12:49 PM 'ookami' via Metamath <meta...@googlegroups.com> wrote:

I left a comment under Hotz's video and invited him to visit this thread.  If we are lucky, we will see his ideas here.

Wolf Lammen

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/95aed103-95a1-4f21-95e8-bb14b0f087b0%40googlegroups.com.

[fl]

What's the most surprising in such discussions is how little people in the field know about each other.

Learning a proof checker takes such a long time ! And the underlying logics are different.

What he is looking for is that no?

https://www.youtube.com/watch?v=Rst2hZpWUbU

And the FAQ.

I think that the "metamath" executable itself is better to get acquainted with the system than mmj2. Because it is more coerced.

Unfortunately the absence of parser makes it quite impossible to enter some formula.

-- 

FL 

[fl]

But removing side programs or databases could help the beginner not to get lost.

And also a presentation on the art of finding the theorem you are looking for in set.mm

-- 

FL

[vvs]

Learning a proof checker takes such a long time ! And the underlying logics are different.

As if informal mathematics is somehow easier. But at least they have international events to attend to and learn about each other in person. But that's not for amateurs or ordinary teachers.

What he is looking for is that no?

https://www.youtube.com/watch?v=Rst2hZpWUbU

According to Thurston (and seems that he knows what he's talking about) the best way is personal first-hand experience. Taking math on lectures is not that good at all. And the worse are papers and textbooks: https://arxiv.org/abs/math/9404236

[fl]

According to Thurston (and seems that he knows what he's talking about) the best way is personal first-hand experience.

In his case it doesn't seem effective. It mostly looks like he is going around in circles.

 

Taking math on lectures is not that good at all. And the worse are papers and textbooks: https://arxiv.org/abs/math/9404236

A clever mix of the two perhaps ?

-- 

FL 

[vvs]

Taking math on lectures is not that good at all. And the worse are papers and textbooks: https://arxiv.org/abs/math/9404236

A clever mix of the two perhaps ?

But is that possible? He was concerned about limited feedback and ambiguous language. But at the time there was no effective computer assisted education. Though, I'm not so sure that now it's that different reading even this same thread.

[fl]

A clever mix of the two perhaps ?

But is that possible? He was concerned about limited feedback and ambiguous language. But at the time there was no effective computer assisted education. Though, I'm not so sure that now it's that different reading even this same thread.

I was talking about George Hotz. I haven't had time to read  Thurston's paper yet. Formalizing a proof with metamath is certainly a very good way

to understand an unformal proof. I don't know if you have alreay tried it.

-- 

FL

[David A. Wheeler]

Mmj2 includes a little tutorial. I have occasionally thought of going through the tutorial and recording it as a Youtube video, so that people can see the software without installing it.

I don't know if that would actually be helpful, I'd love to know what people think.
--- David A.Wheeler

[vvs]

Formalizing a proof with metamath is certainly a very good way

to understand an unformal proof. I don't know if you have alreay tried it.

Yes, I did. I proved simple propositional calculus theorems in mmj2 using deductive form. But I'm at loss from a sheer amount of theorems in set.mm and the only help is their name conventions and rudimentary search facility. That's just too painful in comparison to e.g. Lean's tactics mode (or auto completion) which will infer many details without your consent. But the price is high: there is no detailed axiomatic proof which is understandable by humans. For example a simple arithmetic theorem when exported take dozens of megabytes of incomprehensible byte-code (compare to Metamath's proofs) which can't be rendered/pretty-printed and even type checking takes far too much time. Using #check or #print doesn't help either because it used dependent type theory as a foundation.

People can get used to it, mmj2 is not that bad after all. But it needs much more tedious training than necessary, even though it's secondary to my goals. I will do it eventually but only after I'm already proficient enough with Lean (MM0 is not ready yet). Looks like I'm more used to tactics workflow even before I knew that it used tactics behind the scene. I have some previous beginner's experience with other proof assistants with a more user friendly UI but I didn't learn their tactics language before. Good tutorial is a key to become familiar with database and workflow. And a good interactive goal driven UI helps a lot. I'm just don't feel confident without much background in mathematics so I will try to get that confidence before diving into set.mm. Or if Mario's suggestion to create a curated database will be implemented then I could try it sooner.

[heiph...@wilsonb.com]

> Why on earth anybody would be interested in Metamath which is even more obscure than Coq or Lean?

The abundance of discourse available on the Metamath website is absolutely
divine. It's what really made the basic idea of formal logic click for me. In
particular, it's the only source I've encountered that clearly discusses the
distintction between a logic and it's implementation in a metalogic. That had
always been a source of confusion for me in the past.

Not to mention, Metamath's core idea is simply elegant and beautiful.

I have not watched the video, but by reading the comments in this thread, I get
the impression that Hotz's confusion may hav stemmed mostly from an impedence
mismatch between fields.

My education is in pure math (algebraic geometry); however, my work is software
development. The metamath executable definitely runs counter to what Software
Developer me would exepect of tools in the field. However, Math Student me
feels like it's quite straightforward and ergonomic (at least for the small,
simple theorems I've tried proving).

The conventions in set.mm are actually pretty nice, but the naming scheme does
run counter to modern mainstream Software Development Philosophy, which tends
to emphasize "approachability to non-experts" under the moniker of "readable
code." I do recall the website discussing naming conventions in set.mm but
it's burried enough that I would not be able to easily find that again.

Anyway, just the thoughts of someone who also recently encountered Metamath.

Cheers!

> --
> 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 metamath+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj5R7Jk6baAHVOw1QS_7DpE2D94WDGwy_0Tkc-CYomxNDg%40mail.gmail.com.

[Alexander van der Vekens]

On Sunday, December 22, 2019 at 4:34:17 PM UTC+1, Mario Carneiro wrote:

... set.mm would have been an optimal starting point, except it's HUGE, which makes introductory stuff harder. Even worse, it starts with a comment that is tens of thousands of lines long, which makes it very difficult to see how "baby's first propositional logic" is supposed to go.

 

Maybe a first step to purify set.mm could be to extract the "history" in section "1. Recent label changes" at the beginning of set.mm into a separate file - this would save (currently) about 10.000 lines ...

[fl]

 

Let's use Occam razor. Why on earth anybody would be interested in Metamath which is even more obscure than Coq or Lean? 

I just came across a recent presentation by Philip Wadler. The man behind Haskell and the monads. 

https://www.college-de-france.fr/site/xavier-leroy/seminar-2019-12-12-11h15.htm

He doesn't seem to appreciate Coq as a system  for teaching logic. Here he uses Agda to teach simply typed lambda calculus  

(terms evaluation, extrinsic and intrinsic typing ...)

The book he is using is:

https://plfa.github.io/

Metamath has a formalization of simply typed lambda calculus  by Mario Carneiro. 

http://us.metamath.org/holuni/mmhol.html

You can use Philip Wadler's book to catch what it is all about before delving into Carneiro's code.

-- 

FL

[vvs]

The book he is using is:

https://plfa.github.io/

Metamath has a formalization of simply typed lambda calculus  by Mario Carneiro. 

http://us.metamath.org/holuni/mmhol.html

You can use Philip Wadler's book to catch what it is all about before delving into Carneiro's code.

Thanks for the pointers. It's always good to have companion books to a proof assistant ecpesially if it can be applied to one of Metamath's databases.

I almost finished "Theorem Proving in Lean" and there is "Logic and Proof" which used Lean as a foundation:

https://leanprover.github.io/logic_and_proof/

There are many useful pointers in Metamath's bibliography. I've also read Richard Bornat's book "Proof and Disproof" which might serve mostly as a practical guide to natural deduction in Jape (which has a nice UI for beginners implemented using tactics language, BTW), but also has some information about software verification:

http://www.eis.mdx.ac.uk/staffpages/r_bornat/

But honestly, for starters it should not matter as much about logical foundations as it's about assistant, UI, practical workflow and database organization, oriented towards non-mathematicians or undergraduates. Careful selection of theorems from a proof database with good explanations could make a wonderful tutorial in logic, arithmetic and using a proof assistant. That's how natural number game looks like and I enjoyed it as such:

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

David asked what others think about extending mmj2's tutorial. And that's what I thought.

[Norman Megill]

Possibly, although that might be a good way to ensure it rarely gets updated. :)  We've had a pretty good record of keeping it maintained, and I think that's partly because it's at the top where everyone sees it.

The label change list already is a separate file called  set-header.mm if you use 'write source set.mm /split'.  Currently predicate calculus is broken out into a stand-alone mm file called set-pred.mm, but we could further split that into set-prop.mm and set-pred.mm, or however we want.  Maybe we could add a comment on the 2nd line of set.mm, "To break this file into smaller modules, in the metamath program type 'read set.mm' followed by 'write source set.mm /split'.", which newcomers would see when first opening set.mm.

While we could release set.mm in the form of multiple modules (currently 38) created by /split, that would mean extra work to keep David's autotools updated and possibly cause other confusion as people add, delete, rename, or merge modules in their mathboxes etc.  I would prefer not to do that since it doesn't really buy us anything.

Another alternative would be to keep only the past year or so and discard older history.  Or we could abandon it completely and rely on git, although it might be hard to infer label change history because things are often simultaneously moved and renamed.

Historically, I added the label change list around the time other people started to make significant set.mm contributions.  People would sometimes work on their part for months then send me their update or mathbox.  I used the list to make a script to update the labels in their work so it could be integrated into the current set.mm.  Together with the top date to identify what set.mm version they modified, the label change list made it much easier to get their work updated.  Now almost everyone (but not all) uses GitHub to submit their work.

A couple of months ago, when I located some old material that allowed me to fill in missing dates before 5-Aug-1993, the list enabled me to track the history of many label changes.   Of course that was a one-off change that will likely not be repeated.

Norm

[Glauco]

Mmj2 includes a little tutorial. I have occasionally thought of going through the tutorial and recording it as a Youtube video, so that people can see the software without installing it.

I don't know if that would actually be helpful, I'd love to know what people think.
--- David A.Wheeler

 

Years ago I decided to prove "something" in Metamath, after having seen your video showing a session in which you prove "Reciprocal of cotangent is tangent" .

I'll be really glad if you'll find some time to record other tutorials.

Glauco

[Jim Kingdon]

On December 23, 2019 4:00:23 PM MST, Glauco <glaform...@gmail.com> wrote:
>
>
>> Mmj2 includes a little tutorial. I have occasionally thought of going
>
>> through the tutorial and recording it as a Youtube video, so that
>people
>> can see the software without installing it.
>>
>> I don't know if that would actually be helpful, I'd love to know what
>
>> people think.
>> --- David A.Wheeler

I went through that tutorial when I was learning mmj2. I found it a bit hard to figure out the mechanics of flipping through the tutorial at the same time that everything else was new, so I think a video could be nice.

Not that there is necessarily a magic bullet in helping people climb this learning curve, but recording a video of the existing tutorial is less work than a lot of things I could think of.

[David A. Wheeler]

I really appreciate others' willingness to summarize the videos by Hotz, e.g.:
https://www.youtube.com/watch?v=hKi9Q3S1Nsg

Below are my comments on those summaries, in the hope that we can learn
about potential improvements:

On Sat, 21 Dec 2019 21:16:08 -0800 (PST), "'ookami' via Metamath" <meta...@googlegroups.com> wrote:
> I followed this video up to 2:00:00, and had an editor open to scribble
> down some notes while I was watching. Here are the results. Please note,
> these are impressions made on the fly, and perhaps not well thought over.

>
> 1. Metamath hype: Why on earth is someone like George Hotz interested in
> Metamath at all? There seems to be a hype around, judging from his first
> words.

Well, that's cool. I obviously think Metamath is interesting as well :-).
And while he has complaints, it's hard to think of anything you can't complain
about, and his GitHub repo ends up saying some positive things about Metamath.

Specifically, https://github.com/geohot/twitchcoq
says in its README:
"Reimplementing a subset of Coq in Python.
Just kidding, Coq is too complex.
We implemented metamath instead.
It (slowly) verifies set.mm as of 11/3/2019
Ideally, Coq and friends should be rewritten in metamath. It's really the future, just wish it looked better. But omg, this is the proper stack for formal math, "formalism" is alive and well and is the truth in philosophy."

> 2. Cryptic labels: He is ranting while faced with theorem names on the HTML
> page of sqr2irr. No clue whatsoever what they mean. Compares this to more
> explicit names found in competing products, and in program code in
> general. I think there is indeed headroom for improvement here. Maybe a
> pop up showing an explanation while hovering over a name alleviates the
> situation.

Huh? There *is* a pop up showing an explanation when hovering over a name,
in both the GIF and Unicode versions. Try it out! Just go here:
http://us.metamath.org/mpegif/sqr2irr.html
and hover over any of the theorem names; you'll see the first sentence of the theorem
comment displayed. For example, step 5 uses breq2 ; just put your
mouse over that and it displays "Equality theorem for a binary relation..."

I do agree that the pop-ups are not very discoverable (if you don't know they
are there, it's not obvious to try it out). Also, hover doesn't work on most
mobile devices (touch screens generally can't hover), and mobile devices are
the most common way to view HTML pages (though they CAN detect a click-down).

POTENTIAL IMPROVEMENT:
Maybe there'd be a way to the hover information more discoverable
AND modify things so it's invokable in mobile devices (say by onclick).

The underlying Metamath language doesn't require short names, it's simply a
convention in set.mm, iset.mm, and many others.
We do have naming conventions, but it's fair to say that the names aren't too obvious.

I'd be fine with longer names, though I don't know if others would be.
In a few cases we have short names that perhaps could be a little longer, e.g.,
"sqr" is currently short for "square root" in set.mm, but that is arguably
ambiguous with "squre"; we could use "sqrt" instead.
If we want names to be much easier to read for newcomers, though, I think
the obvious way would be to insert separators between the named parts.
The obvious separator is "_", so we could rename "sqr2irr" into "sqrt_2_irr".
We could even spell things out more fully, e.g., "squareroot_2_irrational".
Metamath tools won't have any problem with that, and compression tool
like zip will compress that to a similar size, though of course the
expanded file would be a lot bigger.

I don't know if we *should* have longer names in set.mm and friends,
but I think it's worth exploring.

> 3. No directories, just a global scope. Yes, this is a drawback in my
> eyes, too. But this is not an easy task as it seems at first sight. If
> you take this idea seriously, i.e. topics are finally independent, you end
> up with a need for a linker infrastructure. Compare to compiler.

I'm sympathetic to this complaint. Indeed, when we discussed the
"usage is discouraged" I recommended more information to provide
information hiding. I don't think it's complicated to do, and I think it'd
could be a good idea, though of course the devil's in the details.

> 4. Not conforming to standards. At various occasions he struggles with
> details just because they do not meet his expectations. Syntax for example

Can you be more specific? "Not what I expect" doesn't mean it's bad.

> 5. He somehow got lost in the gory technical details of strict proof syntax
> and verification. But the core idea of a Metamath proof is applying
> patterns to symbol strings. He seems not always be aware of this 'road
> map'. I remember when I first looked into Metamath I was not in the least
> interested in details like how variables are defined. In fact, I was not
> concerned with program details at all. I was satisfied to know how to
> replay a proof by hand. Once I learned the top level formalism, I easily
> could imagine a stack like structure for some automatic verification.

Not sure what we can do to help there.

> 6 Human interface of the Metamath program. Tries out common commands at
> random, does not use the help feature. No GUI.

I prefer mmj2's GUI over Metamath.exe for proofs, so no argument there :-).
But of course, you can use one of several tools for writing proofs.

> 7. He feels at ease when he detects the formal syntax description of the
> Metamath language,and elaborates on implementing it in a Python parser.
> Here he is on firm grounds and starts exploring Metamath. Unfortunately,
> this distracts him from the core idea, in my eyes, see 5.

That's cool. Though there's already a parser and verifier in Python, I wonder
why he didn't start there:
https://github.com/david-a-wheeler/mmverify.py

--- David A. Wheeler

[David A. Wheeler]

On Sun, 22 Dec 2019 05:26:30 -0800 (PST), savask <sav...@yandex.ru> wrote:
> I watched though the video and spotted a few things not mentioned in Wolf's
> notes.
>
> At around 1:02 (1 hour 2 minutes), he starts writing a grammar file based
> on the EBNF in the Metamath book. The book uses dashes inside symbols on
> the left hand side of each rule, which is apparently not shared by all EBNF
> standards, so he has to replace them by underscores. GNU bison supports
> dashes (but calls it a GNU extension, incompatible with POSIX Yacc), Happy
> parser verifier (for Haskell) also doesn't allow dashes in symbol names.
> Maybe it is worthwhile replacing dashes by underscores in the Metamath book
> EBNF? It may save someone time, in case if they would like to simply copy
> the grammar file from the book.

I don't think switching dashes would help. Like all language specs, the EBNF is high-level.
An implementation should make a number of changes to implement it
efficiently. For example, you need to rewrite them to avoid left/right recursion
as necessary for LL or LALR parsers. By that point, switching the labels is trivial.

We could separately post a GNU bison implementation. If someone wants to
start with GNU bison, that'd be a far better help. Of course, it's so trivial to
parse Metamath files that I'm not sure it'd help much. Does anyone think
that'd be worth the trouble to create?

> At 5:02, he tries mmj2. Apparently there's some sort of trouble launching
> it on the MacOS (he had to modify the starting script), so maybe that bug
> should be fixed.

I don't have a Mac, so I can't reproduce that. Can someone with a Mac help us
reproduce & then help us fix that?

> My impression is that most of his complaints come from missing
> proof-assisting capabilities of the metamath program and mmj2, but main
> points stand of course. Our tooling is scarce and most of work is done
> manually anyway.

I agree. There's nothing fundamental about Metamath that prevents the
implementation of higher-level & more powerful tactics, but Metamath
currently doesn't have that. I'd love to see those additions.

> On the other hand, the video has quite a lot of praise for
> the Metamath book and the design of the language itself (stressing its
> simplicity), so Metamath clearly has its strong points in comparison with
> other proof systems.

Sounds sensible.

--- David A. Wheeler

[Norman Megill]

On Friday, January 3, 2020 at 6:56:21 PM UTC-5, David A. Wheeler wrote:

> 2. Cryptic labels: He is ranting while faced with theorem names on the HTML
> page of sqr2irr.  No clue whatsoever what they mean.  Compares this to more
> explicit names found in competing products, and in program code in
> general.  I think there is indeed headroom for improvement here. Maybe a
> pop up showing an explanation while hovering over a name alleviates the
> situation.

Huh? There *is* a pop up showing an explanation when hovering over a name,
in both the GIF and Unicode versions. Try it out! Just go here:
  http://us.metamath.org/mpegif/sqr2irr.html
and hover over any of the theorem names; you'll see the first sentence of the theorem
comment displayed. For example, step 5 uses breq2 ; just put your
mouse over that and it displays "Equality theorem for a binary relation..."

The primary purpose of a label is to identify a theorem uniquely.  In books this is accomplished with equation/theorem numbers, which are much more cryptic than our labels but don't seem to bother the readers or at least the author.  Principia Mathematica was written entirely with nothing but numeric labels with the exception of a handful of very common cases like Simp and Syl.  The reader gets used to "*2..." being mostly about implication, negation, and disjunction, "*3..." about conjunction, "*4..." about biconditional, etc.  We try to provide at least a hint of what the theorem is about using our conventions, but an unambiguous description of the theorem is impossible to achieve, and we don't pretend that it does.  Information about the theorem is provided by its description and its actual content, just like in books.  Both of these are searchable and are the main ways that I locate a theorem whose name I forgot, perhaps assisted by a label with wildcards.  Both are instantly available for the reader in a web page proof either by hovering over the label or clicking it.

Note that at the top of set.mm I added a link to label conventions.

For me personally, an important reason to keep labels short is to make them easier to type.  Maybe this isn't everyone's experience, but I find it easier to remember labels that are shorter (especially if they follow a convention, which we try to do).  To remember a long label means having to remember all pieces of the label, their order, and, since they are never going to be spelled out in full English, what abbreviations were chosen.  There seems to be a threshold label length of maybe around 8 to 10 characters where I start to make mistakes typing it in (after glancing at it in another window) and end up resorting to copy/paste, slowing me down.

The Wikiproofs site (wikiproofs.org) seems to be down, but looking it up on archive.org it uses theorem labels like "introduceBiconditionalFromImplicationsInConsequent".  Personally I think that would slow me down and I would dislike it.  IIRC Jim Kingdon contributed to that project, and it would be interesting to hear his experience with long labels.

Currently, the longest label in set.mm is aiffnbandciffatnotciffb, which is in a mathbox.  While it attempts to describe the theorem, it doesn't do so unambiguously, and I doubt I could remember its exact spelling even long enough to type it without making a mistake unless I looked directly at it.  We would almost certainly change it to a much shorter label should it be moved to the main set.mm.

Another smaller consideration is the set.mm file size.  Inside of proofs in the current set.mm, there are 1.1 million instances of labels with an average length of 5.8 bytes.  Each extra byte of average label length would add a megabyte to the file size.  (The 5.8 length is distorted by short labels for syntax axioms, and the average label length for just theorems, which I didn't calculate, would be longer.)

I do agree that the pop-ups are not very discoverable (if you don't know they
are there, it's not obvious to try it out). Also, hover doesn't work on most
mobile devices (touch screens generally can't hover), and mobile devices are
the most common way to view HTML pages (though they CAN detect a click-down).

POTENTIAL IMPROVEMENT:
Maybe there'd be a way to the hover information more discoverable
AND modify things so it's invokable in mobile devices (say by onclick).

I don't know how to solve the mobile problem, but for PC browsers perhaps it would be useful to add to each page a sentence on each page saying something like, "Hover over a label link for more information."
 

The underlying Metamath language doesn't require short names, it's simply a
convention in set.mm, iset.mm, and many others.
We do have naming conventions, but it's fair to say that the names aren't too obvious.

I'd be fine with longer names, though I don't know if others would be.
In a few cases we have short names that perhaps could be a little longer, e.g.,
"sqr" is currently short for "square root" in set.mm, but that is arguably
ambiguous with "squre"; we could use "sqrt" instead.
If we want names to be much easier to read for newcomers, though, I think
the obvious way would be to insert separators between the named parts.
The obvious separator is "_", so we could rename "sqr2irr" into "sqrt_2_irr".
We could even spell things out more fully, e.g., "squareroot_2_irrational".
Metamath tools won't have any problem with that, and compression tool
like zip will compress that to a similar size, though of course the
expanded file would be a lot bigger.

Our current square and square root conventions are "sq" and "sqr" resp.  I'm almost certain I've seen "sqr" used for square root in at least one computer language although I can't recall which one right now.  I don't see the problem with omitting the "t" since any confusion is instantly resolved by hovering over the label, if the content of the proof step doesn't make it obvious.  If people are truly confused by this, I suppose we can add the "t", but until now no one has complained about it.

I don't see the point of "squareroot_2_irrational" - long to type, annoying to shift for the _, and not necessarily easy to remember precisely (is it "2" or "of_2"? does it have "is"? why isn't it "square_root" since they are 2 words in English?).  And theorems that can be described unambiguously like this one in a few words are very rare.  Our convention is pretty clear on the abbreviations "sqr", "2", and "irr", making "sqr2irr" easy to remember (for me at least) and type.

Norm

[Jim Kingdon]

On January 3, 2020 7:12:23 PM PST, Norman Megill <n...@alum.mit.edu> wrote:

>The Wikiproofs site (wikiproofs.org) seems to be down

The content is at https://github.com/jkingdon/wikiproofs along with a
few notes about the tools which were used.

>, but looking it
>up on
>archive.org it uses theorem labels like
>"introduceBiconditionalFromImplicationsInConsequent". Personally I
>think
>that would slow me down and I would dislike it. IIRC Jim Kingdon
>contributed to that project, and it would be interesting to hear his
>experience with long labels.

I guess on the whole it feels pretty similar to set.mm for me.
"InConsequent" was consistently used the way metamath uses a trailing
"d". "detach" was in many theorem names and corresponds to "mp" found in
similar metamath theorems, etc.

I think there was a whole "introduce"/"eliminate" naming convention
which corresponds to many texts (see for example sections A.2.4, A.2.5,
A.2.6, and following sections in the HoTT book), but I don't remember
how well developed that was.

I wouldn't get super hung-up on abbreviations versus whole words. I
think the latter do provide for an easier on-ramp in the early stages.
The former are faster to type (especially if we assume limited/no
autocomplete tools), and do provide a certain conciseness.

More important than abbreviations versus words, I think, is how
consistently the conventions are followed and how natural they feel.
Metamath has made a lot of improvements in this area and at least for me
the difference between "expd" and "exp3a" (or whatever it used to be
called, I forget already) is like night and day. I hope we continue to
improve our names. We haven't reached perfection yet but a spirit of
slow but steady improvement is what has gotten us as far as we have gotten.

I feel like I should conclude by summing up the wikiproofs experience. I
suppose the capsule summary (for wikiproofs and also ghilbert) is that
it is hard for a new system - even one which is compatible or partly
compatible - to get off the ground. But I hope people keep trying. Not
because there is anything wrong with metamath . After all, after trying
to learn/create a whole bunch of provers, metamath is the one which has
so far stuck with me. But because there are still things to work on,
whether it is making it easier to write proofs, easier to browse/read
them (already a big strength of metamath over most others I've seen),
easier to handle very large proof databases (set.mm is a tiny fraction
of known mathematics), easier for people to contrbute proofs, or
whatever other area(s). I'm pretty sure that one or more will eventually
succeed, whether metamath zero, or milpgame, or something else out
there, or something which doesn't even exist yet.

[Alexander van der Vekens]

I fully agree with Norm that we should not change our general conventions/usage of labels as "identifiers": they should be short, concise and consistent (besides the primary property of being unique). Of course we should still continue to improve the conventions and their usage.

Since labels and comments seem to be not sufficient to understand theorems and their proofs, the introduction of "names" or "titles" for theorems may help. Actually, many comments consists of a name/title only (besides the parentheticals),

e.g. ~necom:  $( Commutation of inequality.  (Contributed by NM, 14-May-1999.) $),

or the first sentence is like a name/title,

e.g. ~cramer:   $( Cramer's rule.  According to Wikipedia ... $).

In many cases, however, the comment contains more information, and a name/title cannot be "extracted" easily/automatically,

e.g. ~ixpn0: $( The infinite Cartesian product of a family ` B ( x ) ` with an empty
       member is empty.  The converse of this theorem is equivalent to the
       Axiom of Choice, see ~ ac9 .  (Contributed by Mario Carneiro,
       22-Jun-2016.) $)

I think the name/title of this theorem could be "Infinite Cartesian product with empty member". To identify names/titles of theorems, we either can use conventions (for example the first sentence of a comment, or the part of the first sentence up to the first punctuation mark) or a special parenthetical - for ~ixpn0 for example:

$( (Title: Infinite Cartesian product with empty member)  The infinite Cartesian product of a family ` B ( x ) ` with an empty ...

or an additional information comment - for ~ixpn0 for example:

$( $j title Infinite Cartesian product with empty member $) 

$( The infinite Cartesian product of a family ` B ( x ) ` with an empty ...

Such a name/title could be used in the HTML/LATEX outputs, both in the overview (new column "Title" or "Name" between columns "Label" and "Description") and for a single theorem (in a new line "Title: ..." between "Theorem <label>" and "Description: ....") and in the proofs (new column "Title" or "Name" or "Theorem" between columns "Ref" and "Expression"). At least such a name/title could be used as hover information (instead of using the first part of the comment, which could contain more informatioin than necessary/useful, e.g. for ~usgrass the hover text is "An edge is a subset of vertices, analogous to ~ umgrass .  (Contributed by Alexander..." - "An edge is a subset of vertices" would be better/sufficient).

What do you think about this approach?

[Alexander van der Vekens]

PS: In contrast to a label, the name/title needs not to be unique! It should only give a more descriptive hint to the meaning ot the theorem. For example, ~sbie, ~sbied and ~sbiedv could have the same title "Substitution conversion: implicit to explicit". That two of them are in deduction form or two of them use bound-variable hypotheses instead of distinct variable restrictions can/should be mentioned in the comment as usual (or this information can be obtained from the suffixes of the labels!).

[ookami]

I am going to answer to each point separately so to not let grow the
text to inappropriate length.

>> 2. Cryptic labels: He is ranting while faced with theorem names on the HTML
>> page of sqr2irr.  No clue whatsoever what they mean.  Compares this to more
>> explicit names found in competing products, and in program code in
>> general.  I think there is indeed headroom for improvement here. Maybe a
>> pop up showing an explanation while hovering over a name alleviates the
>> situation.

> Huh? There *is* a pop up showing an explanation when hovering over a name,
> in both the GIF and Unicode versions. Try it out! Just go here:
>  http://us.metamath.org/mpegif/sqr2irr.html
> and hover over any of the theorem names; you'll see the first sentence of the theorem
> comment displayed. For example, step 5 uses breq2 ; just put your
> mouse over that and it displays "Equality theorem for a binary relation..."

> I do agree that the pop-ups are not very discoverable (if you don't know they
> are there, it's not obvious to try it out). Also, hover doesn't work on most
> mobile devices (touch screens generally can't hover), and mobile devices are
> the most common way to view HTML pages (though they CAN detect a click-down).

Yes, there is indeed a pop up.  At the time I wrote those lines, I was not
aware of this feature.  I don't remember whether George Hotz accidently invoked
one... If he did it had no effect on his opinion.

I personally need no help of this kind.  For one, I know the theorems in my field
pretty well, and, second, if I need additional information, such as the precise
form of hypotheses, I call the theorem's page directly. I more often need a search
function.  I use the mmtheorems' page to look for related theorems, and if nothing
else helps look into set.mm directly.

So we have two aspects here: George's apparent need for immediate explanation as a
newbee, and my needs for a more elaborate search function.

A newbee needs an overview to find her/his way through a big proof like sqr2irr.
I think s/he is overwhelmed by the flurry of detail information, where important
subtheorems stand indiscriminately side by side with 'glue' theorems transforming
intermediate results just to link two major substeps.  There is some help given by
the proof indentation, other possible structuring aid at the discretion of proof
creators is the use of appropriate lemmas, or explanatory remarks in the heading
text.  I wonder whether additional inline features like markers, frames and the
like could guide through a long proof. So far, there is no way to add educational information to the proof itself, preferably added on request.

My personal wish list is headed by an appropriate search function.  So far I
always use metamath as my primary working tool.  Maybe other products like mmj2
or Milpgame feature more elaborate search functions.  For a textual search in
set.mm in an editor it would be helpful to have all variables appear in a fixed order,
i.e. x / ph / A always appear as the first use of their kind, y / ps / B come
second, and so on, so I can predict how a desired theorem looks like textually.
On the web page I would like to see another link 'related theorems' next to
'nearby theorems' assembling theorems of a kind (deduction, inference, tautology,
possibly more variants specializing on certain aspects).

> POTENTIAL IMPROVEMENT:
> Maybe there'd be a way to the hover information more discoverable
> AND modify things so it's invokable in mobile devices (say by onclick).

> The underlying Metamath language doesn't require short names, it's simply a
> convention in set.mm, iset.mm, and many others.
> We do have naming conventions, but it's fair to say that the names aren't too obvious.

> I'd be fine with longer names, though I don't know if others would be.
> In a few cases we have short names that perhaps could be a little longer, e.g.,
> "sqr" is currently short for "square root" in set.mm, but that is arguably
> ambiguous with "squre"; we could use "sqrt" instead.
> If we want names to be much easier to read for newcomers, though, I think
> the obvious way would be to insert separators between the named parts.
> The obvious separator is "_", so we could rename "sqr2irr" into "sqrt_2_irr".
> We could even spell things out more fully, e.g., "squareroot_2_irrational".
> Metamath tools won't have any problem with that, and compression tool
> like zip will compress that to a similar size, though of course the
> expanded file would be a lot bigger.

> I don't know if we *should* have longer names in set.mm and friends,
> but I think it's worth exploring.

As for the naming conventions (I reply to Norm's related answer here as well),
my first impulse is 'why not having both?'.  What about alias names beside
the current shorthand form (saving typing (errors)), say a descriptive display
name, that is used on the web page on demand. And is found in a search
instruction as well.

I work as a programmer, and there is a lesson learned by professionals in this
area.  Use descriptive names wherever possible.  It helps others understanding/
reworking your code, and the same obviously holds for proofs.  As a quick
introduction see https://www.geeksforgeeks.org/java-naming-conventions/.

The price paid for not following these conventions in the early days of
programming amounts to immense waste of working time.  While the current size
of Metamath with some 30000 theorems is perhaps not demanding enough for
strict rules, I forsee a time where you cannot do without anymore.

Wolf Lammen

[ookami]

Follow up.

>> 3. No directories, just a global scope.  Yes, this is a drawback in my
>> eyes, too.  But this is not an easy task as it seems at first sight.  If
>> you take this idea seriously, i.e. topics are finally independent, you end
>> up with a need for a linker infrastructure.  Compare to compiler.

> I'm sympathetic to this complaint. Indeed, when we discussed the
> "usage is discouraged" I recommended more information to provide
> information hiding. I don't think it's complicated to do, and I think it'd
> could be a good idea, though of course the devil's in the details.

Let me first explain, why I think breaking up the whole file into pieces along
the borders of topics is not enough.

The main reason for this is allowing diversification.  We already see that
an alternative to ZFC, intuitionistic logic, is developed in parallel.  And in
my mathbox you find propositional logic based on Lukasiewicz axioms.  It
would be nice to let higher abstraction levels of mathematics (I call them
modules here) depend on whatever foundations the user requests.  In such a
situation there is need for a descriptive layer that programmers call interface.
The module declares what prerequisites must be fulfilled to be valid, and
other, more foundational modules, provide this demands.  The idea is to let
modules be interchangeable.

Such a situation is already solved by programming infrastructure, and programs
that check the validity and compatability of interfaces are called linkers.
In my eyes advanced forms of Metamath should feature such an infrastructure.

The good news is, that this problem is already solved, and we just have to
adapt an existing solution.  The bad news is, the amount of work to adapt this
solution appears still daunting to me.

Wolf Lammen

[Alexander van der Vekens]

Hi Wolf,

On Saturday, January 4, 2020 at 11:40:11 AM UTC+1, ookami wrote:

...

As for the naming conventions (I reply to Norm's related answer here as well),
my first impulse is 'why not having both?'.  What about alias names beside
the current shorthand form (saving typing (errors)), say a descriptive display
name, that is used on the web page on demand. And is found in a search
instruction as well.

This goes in the direction of my previous post, see  https://groups.google.com/d/msg/metamath/XPYuatviNV0/R7iGhHynDQAJ

Alexander

[ookami]

Follow up.

>> 4. Not conforming to standards.  At various occasions he struggles with
>> details just because they do not meet his expectations. Syntax for example

> Can you be more specific?  "Not what I expect" doesn't mean it's bad.

Unfortunately, this is a summary of impressions I got on various occasions, and
I missed to note them down as I encountered them while watching.  So I must remain
short of the details.

As for the 'syntax' I mentioned, it is actually a grammar describing a syntax.
Doing so is a commonplace in computer science.  The problem here is that
the wheel is reinvented.  And somebody like George Hotz knows grammars and
grammar parsers well enough to understand standard grammar descriptions
immediately.  Instead he is forced to leap over a hurdle by adapting to a particular
notation.  He was able to do so, but an ideal Metamath could stay clear of such
obstacles.

Ok, once and for all, let me be clear here.  Metamath roots back in the early 90's,
and it is simply unfair to assume it is up to current standards.  Norm, assembling
all the details and perform their formalization was great work, and I do not want to
blame anyone for the current state, which is not bad, by the way.  That said, one can
and should think about future directions.

Wolf Lammen

[ookami]

Follow up.

>> 5. He somehow got lost in the gory technical details of strict proof syntax
>> and verification.  But the core idea of a Metamath proof is applying
>> patterns to symbol strings.  He seems not always be aware of this 'road
>> map'.  I remember when I first looked into Metamath I was not in the least
>> interested in details like how variables are defined.  In fact, I was not
>> concerned with program details at all.  I was satisfied to know how to
>> replay a proof by hand.  Once I learned the top level formalism, I easily
>> could imagine a stack like structure for some automatic verification.

> Not sure what we can do to help there.

This is an educational problem.  We have documentary on our web site, and carefully
read, one should be in theory fit enough to start contributing.  If people fail
to succeed in doing so, or get lost in details, or their patience is stressed, then
we can either shrug our shoulders and let them go, or we provide a better means of
introduction like a quick overview, tutorial and the like.  To be clear here,
George Hotz is just one person eager to learn, others may have different problems.
We certainly do not want to adapt to a single person.  Instead we should allow
people to give feed back, and suggest improvements.  Over time we learn how to
improve.

Wolf Lammen

[ookami]

Final post.

While I was writing my answer in several posts, I noticed that other had published their opinions as well.  My state as of writing was Norms post.  I have to apologize that that I could not react to more recent posts, and I will not follow suit before tomorrow.  If you have replied to my posts already, thanks for your attention.

Wolf Lammen

[David A. Wheeler]

David A. Wheeler:

>> POTENTIAL IMPROVEMENT:
>> Maybe there'd be a way to the hover information more discoverable
>> AND modify things so it's invokable in mobile devices (say by onclick).

Norman Megill:

>I don't know how to solve the mobile problem, but for PC browsers
>perhaps
>it would be useful to add to each page a sentence on each page saying
>something like, "Hover over a label link for more information."

At least that would be easy, but that text would be far away from the hovering area and thus might be easily missed. It also wouldn't solve it for mobile users.

We can't be the only ones with that problem. Here's one article that suggests an alternative:
https://uxmovement.com/mobile/how-to-display-tooltips-on-mobile-forms/

Basically, add a symbol where you want the tooltip, so that mobile users have something to press and everyone has an indication that there is something there The same article uses a colored "?" with a circle around it (we could add that right after the symbol reference). We could use CSS so that the symbol is not displayed when printed, since it would not be useful in that case. I don't know how hard that would be, but it would probably not be too hard.

What do people think about that idea?

--- David A.Wheeler

[vvs]

Basically, add a symbol where you want the tooltip, so that mobile users have something to press and everyone has an indication that there is something there  The same article uses a colored "?" with a circle around it (we could add that right after the symbol reference). We could use CSS so that the symbol is not displayed when printed, since it would not be useful in that case. I don't know how hard that would be, but it would probably not be too hard.

What do people think about that idea?

--- David A.Wheeler

This looks fine to me.

But reading that thread I can't help but think how difficult it is to put oneself in someone else's shoes. Actually, there are very different use cases for Metamath. You can either read existing proofs or make a new ones. And while those suggestions above are quite good for the first case they are not improving the second. Using browsers instead of IDE is not a good idea, unless there is a web editor for Metamath proofs that is. Another reason for confusion might be that there are experienced contributors forgetting about novices learning the craft. The latter want a tutorial database with quite different and simplified conventions and theorems.

[David A. Wheeler]

Norman Megill:

>The primary purpose of a label is to identify a theorem uniquely.

>Note that at the top of set.mm I added a link to label conventions.

As someone who helped write the section on label conventions, I appreciate that. :-)

>For me personally, an important reason to keep labels short is to make them

>easier to type. Maybe this isn't everyone's experience, ...

> since they are never
>going to be spelled out in full English, what abbreviations were chosen.
>There seems to be a threshold label length of maybe around 8 to 10

>characters where I start to make mistakes typing it in...

>The Wikiproofs site (wikiproofs.org) seems to be down, but looking it
>up on
>archive.org it uses theorem labels like
>"introduceBiconditionalFromImplicationsInConsequent". Personally I
>think
>that would slow me down and I would dislike it. IIRC Jim Kingdon
>contributed to that project, and it would be interesting to hear his
>experience with long labels.

I would also like to hear their experiences. I suspect full names like that would be suboptimal for set.mm, but I'm willing to be convinced otherwise. One problem with long names like that is that in the two-column format there would be much less room on a phone for the expression.

>Another smaller consideration is the set.mm file size. Inside of
>proofs in
>the current set.mm, there are 1.1 million instances of labels with an
>average length of 5.8 bytes. Each extra byte of average label length would
>add a megabyte to the file size.

>> If we want names to be much easier to read for newcomers, though, I
>think
>> the obvious way would be to insert separators between the named parts.
>> The obvious separator is "_", so we could rename "sqr2irr" into

>> "sqrt_2_irr". ...

>I don't see the point of "squareroot_2_irrational" - long to type,
>annoying
>to shift for the _, and not necessarily easy to remember precisely (is
>it
>"2" or "of_2"?

Yes, I think squareroot_2_irrational is probably too long ( though as I noted above, I'd be interested to hear other opinions). But changing our label conventions so that underscores are between the abbreviations might be a good idea. That would produce labels of the form sqr_2_irr. That might make it a lot easier for people. Currently you have to know the entire set of abbreviations to read what the parts are. If you don't recognize the first abbreviation, it's harder to understand the rest. If we added underscore separators, it'd be much easier for newcomers to understand the label convention and be able to understand at least some of the parts. As the database gets bigger, it becomes harder and harder to remember all the abbreviations, so having a separator is starting to become more and more justifiable. We could make a few exceptions if you think that's important, e.g., for 2p2e4.

It also wouldn't add that much more space. I'm guessing there is an average of 4 abbreviations in a label, so we'd add an average of 3 underscores to each label. That means the average label would change from 5.8 to 8.8. That is very doable. It is not a killer in disk space, and it is also within your goal length for labels. Even if the average is 6 abbreviations, which I doubt, that would make the average label length 10.8 which isn't really all that bad, especially since the underscores are really just separators and thus easy to remember.

One nice side effect of using underscores as separators in labels is that we can instruct css break on underscores, which could improve the formatting in some cases.

It'd be a pain to rename everything, but that is something that can be done once and could be almost entirely automated.

--- David A.Wheeler

[Mario Carneiro]

On Sat, Jan 4, 2020 at 10:08 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:

But changing our label conventions so that underscores are between the abbreviations might be a good idea. 

It'd be a pain to rename everything, but that is something that can be done once and could be almost entirely automated.

I doubt this. Determining where the breaks are would be a highly nontrivial task that I would not trust to a computer without oversight, and it will hit almost all theorems, so this is not an easy task at all.

Mario

[David A. Wheeler]

Norman Megill:

>Our current square and square root conventions are "sq" and "sqr" resp.
>I'm almost certain I've seen "sqr" used for square root in at least one
>computer language although I can't recall which one right now. I don't
>see
>the problem with omitting the "t" since any confusion is instantly
>resolved
>by hovering over the label, if the content of the proof step doesn't
>make
>it obvious. If people are truly confused by this, I suppose we can add
>the
>"t", but until now no one has complained about it.

I am fine with sq as square, but square root is almost universally notated as sqrt.

Here is a list of just some of the languages that use sqrt for square root:
Fortran
C
Python
Excel
Java
C#
JavaScript
Common Lisp
Scheme
Mathematica
Octave / Matlab

In short, the standard abbreviation for square root is sqrt. We would make others' lives simpler by using the same abbreviation everyone else does.

--- David A.Wheeler

[Jim Kingdon]

On 1/4/20 6:59 AM, vvs wrote:

> Another reason for confusion might be that there are experienced
> contributors forgetting about novices learning the craft. The latter
> want a tutorial database with quite different and simplified
> conventions and theorems.

That's an interesting suggestion. We could keep debating set.mm
conventions for a long time (and I suppose we likely will whether I
recommend it or not) but there are a lot of reasons why I don't expect a
fundamental rethink of naming in set.mm. Even "sqr" versus "sqrt" which
I thought might be low hanging fruit, affects a lot more theorems than I
realized before I ran "show label *sqr*" and started looking through the
results.

But a tutorial is a different context. There are (well, should be) far
fewer theorems. I could even imagine going big and thinking about things
like using more illustrations, graphic design which is less
information-dense, and any number of things which would be either
difficult or undesirable for set.mm itself.

Now, writing tutorials (or textbooks or other teaching material -
especially if you want them to be good) is real work so I don't want to
deny that. But if someone's creative juices do flow in that direction,
it might be a chance to "think outside the set.mm box" to one extent or
another.

[Alexander van der Vekens]

It becomes more and more difficult to follow this thread, because many different topics are discussed. Maybe it would be a good idea to start new threads (one for each topic: abbreviation of square root, conventions for labels, presentation of tooltips, etc), although they all have their origins in the video of George Hotz...

[David A. Wheeler]

Oh, oversight would be absolutely necessary. I think a first cut could be partly automated by noticing which symbols exist, finding their df-NAME, and splitting by NAME in that label. But it would clearly take some time.


--- David A.Wheeler

[Chris Bailey]

Hi, I sometimes use a mac. Here's a description of what my process has been to (kind of) get mmj2 working.

1. Clone and get the metamath executable running somewhere (let's say /Users/chris/metamath/)

2. Clone the mmj2 repo at (/Users/chris/mmj2/)

3. Following the 'quickstart' advice in the mmj2 README, double click MacMMJ2.command

4. Get error

```

./MacMMJ2.command Exception in thread "main" java.lang.UnsupportedClassVersionError: mmj/util/BatchMMJ2 : Unsupported major.minor version 52.0

```

5. Update JDK on the advice of google

6. Error changes to :

```

Unrecognized option: -Xincgc
Error: Could not create the Java Virtual Machine.
Error: A fatal exception has occurred. Program will exit.

```

7. Remove `-Xincgc` from MacMMJ2.command

8. Get another error about not finding files

9. Change paths in startup script to point to files on my system (I found that it requires the full path)

10. Get error :

```

I-UT-0015 **** Processing RunParmFile Command #1 = LoadFile,set.mm
I-UT-0015 **** Processing RunParmFile Command #2 = VerifyProof,*
I-UT-0015 **** Processing RunParmFile Command #3 = Parse,*
Java heap space
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space

```

11. Change the file specified in RunParms.txt to something other than set.mm

Thoughts :

- The quickstart section should inform users that they need to edit the startup script to get the program to work instead of telling them to double click it.

- The quickstart section says (thought it doesn't tell you how) you shouled edit `RunParms.txt`, but not that you need to edit `MacMMJ2.command`

- The placeholder paths in MacMMJ2.command (/users/Userone/mmj2jar/mmj2.jar)  should probably be changed to something that signals to users who are just scanning to try and find a problem (or to non-computer people who are expecting MMJ2 to just work out of the box) that they need to be replaced with paths entered by the user specific to their machine.  Or you can just put a comment or something.

- The link to `INSTALL.html` in the README links to the page with the raw HTML code for said file on github, not the rendered version, so is not very helpful.

- Whatever the defaults are for mac, they're not able to parse set.mm without running out of memory (or something). See #10 above.

For reference, the `MacMMJ2.command` file I ended up with looked like :

```

java -Xms128M -Xmx256M -jar /Users/chris/Downloads/mmj2/mmj2jar/mmj2.jar "/Users/chris/Downloads/mmj2/mmj2jar/RunParms.txt" Y "/Users/chris/Downloads/mmj2/mmj2jar/" "/Users/chris/Downloads/metamath/metamath/" ""

```

And the output of `java -version` on my machine is :

```

java version "13.0.1" 2019-10-15
Java(TM) SE Runtime Environment (build 13.0.1+9)
Java HotSpot(TM) 64-Bit Server VM (build 13.0.1+9, mixed mode, sharing)

```

On Friday, January 3, 2020 at 6:13:47 PM UTC-6, David A. Wheeler wrote:

I don't have a Mac, so I can't reproduce that. Can someone with a Mac help us
reproduce & then help us fix that?

--- David A. Wheeler