Re: [Metamath] Putting typesetting "extra spaces" rules in .mm database.

['David A. Wheeler' via Metamath]

> On May 23, 2024, at 10:38 PM, Marshall Stoner  wrote:
> 
> My github repository is https://github.com/mbstoner53 .
> 
> I had to make my own branch of metamath.exe and edit the function
> called getTextLongMath in the file mmwtex.c  to get the spacing to look right 
> for an extra symbol I defined in my own database.  I notice even the comment 
> in the file itself calls it a "kludge".  
> 
> I think if more and more symbols are added to the set.mm all of the extra 
> spacing rules to make html look prettier should be stored in the database 
> itself somehow rather than in the source file mmwtex.c.  I don't know if 
> anyone thinks this would be worth it.  I have an idea on how to do it, but 
> I'm not familiar enough with how the source code works to do it all alone.
> 
> Anyways my idea would be to place a list of regex expressions like...

I don't know if that's the *best* way, but a general mechanism for improving 
formatting
that's part of the database does sound like a good idea.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/8CCD6004-1CA9-4C9D-8F37-B3EE0B28F857%40dwheeler.com.

Re: [Metamath] Metamath Christmas challenge

[David A. Wheeler]

Savask:

> > Igor, congratulations!

I agree, Igor, congrats!!

> On Jan 2, 2024, at 12:07 PM, Igor Ieskov  wrote:
> 
> Thank you! Sure, I will add it into my mathbox after some enhancement.

That's great! I'm hoping that you'll format it so that it (or at least some of 
the supporting parts)
can eventually be moved into the "main" body as well.

This theorem of Ryley ("every rational number is a sum of three cubes of 
rational numbers") is
general, so I think it's worthy to eventually be the main body. We often put
things in mathboxes first, then *later* move them into the body, so it'd be a 
pretty typical progression.

> At the beginning I didn’t know what approach to use. That’s why there are 
> theorems in different forms in the beginning. Initially I created all three 
> forms (inference, deduction and closed) for each theorem because I didn’t 
> know what form I would need further in the proof. But somewhere in the middle 
> of the proof I realized that I need only deduction. Before creating a pull 
> request I will remove all redundant theorems.

I agree. Putting most things in deduction form makes it easier to combine 
results, and you can always create the other forms from deduction form.

> > By the way, did you end up using some automation to finish the proof, or 
> > you did it all by hand after all?
> 
> The parts where I needed to compare or transform polynomials have been proved 
> in semi-automatic mode. Everything else has been done manually. I heavily 
> used the bottom-up prover of mm-lamp, but I count it as “manual mode” because 
> it is able to find only very simple proofs. By the semi-automatic mode I mean 
> a new automation functionality which I added to mm-lamp while working on this 
> proof. It is currently not available on the mm-lamp web site, but I will 
> release it in one of the next versions (hopefully in the next one).

I'm looking forward to this new automation functionality in metamath-lamp!

I think metamath-lamp is a nice proof assistant for Metamath.
If you're interested in learning more about metamath-lamp, I wrote this guide:
https://lamp-guide.metamath.org/
and the first chapters of that guide are also available as videos:
https://www.youtube.com/playlist?list=PL1jSu6GGefBk3RhHW5Srpc2qxWMqhga9J

Metamath-lamp isn't perfect of course. Its "unification" algorithm currently 
has a known weakness
(it's really just a "match" algorithm, so sometimes you have to hand-execute 
replacements
that would be automatic in tools like mmj2 that use full unification).
That's not fundamental to the tool, it's just a weakness of its current 
implementation.
In addition, mmj2 has some nice situation-specific automation that 
metamath-lamp currently lacks.
That said, you can start using metamath-lamp without installing anything ("just 
use your
web browser"), and it even works well on a mobile phone without installing 
anything.
That "ease of getting started" makes metamath-lamp a nice addition to our 
collection of tools.
So congrats to Igor for both the proof *and* for developing the metamath-lamp 
tool!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/06ED1B45-4C8F-4551-A60D-EE8116DE4ED6%40dwheeler.com.

Re: [Metamath] Same alphabet requirements in Word theorems

[David A. Wheeler]

> On Dec 31, 2023, at 7:32 PM, Jerry James  wrote:
> 
> Greetings,
> 
> Due to some real life events, I had to step away from metamath last year.  
> First, I want to apologize for ghosting the community on the last couple of 
> pull requests I made in 2022.  I hope you can forgive me for that.

Welcome back!! I had the same problem in the latter part of 2023, where some 
personal challenges meant I was mostly unavailable & I'm only starting to be 
able to engage more.

We're grateful for whatever time you can apply.

> I would like to get involved again.  When I stepped away, I was working on 
> some material related to formal languages.  Some modifications to the 
> existing Word theorems would make that easier.  In particular, some theorems 
> that mention two words in their antecedents require that both words be over 
> the same alphabet, but the proofs work even if they are not.  That is, these 
> theorems only require that certain objects be words, and the alphabets in 
> question do not affect the proof.  This matters when trying to prove theorems 
> about, for example, a language composed of words with prefixes from language 
> 1 and suffixes from language 2, where the two languages are not necessarily 
> over the same alphabet.\

We've often relaxed requirements on various theorems as they were found 
unnecessary (unless there was some special rationale, and I don't see one 
here). I think the same is true for this case. I'm glad you noticed this 
circumstance & look forward to your work!

I'll note that Gödel's Incompleteness Theorem is #6 in the Metamath 100 list 
<https://us.metamath.org/mm_100.html>. If you make it easier to do proofs 
related to formal languages, and add more theorems about it, your work might 
make it easier to complete that theorem.

> Unions can be used; e.g., if I have W e. Word S and X e. Word T, then the 
> existing theorems can be used by specifying that both words are elements of ( 
> S u. T ).  That works, but it irks me that I have to do extra work because 
> the theorems unnecessarily constrain the alphabets.
> 
> Would the community object if I start removing the same-alphabet constraints 
> where they are not necessary?  I have opened a pull request for the first 
> such theorem, eqwrd: https://github.com/metamath/set.mm/pull/3731.

It looks great! I see several people already reviewed it, all liked it, and 
it's already been merged. So I think you have your answer :-).

This is exactly the process we like! Propose things incrementally so it's 
easier to review the change, tweak it where appopriate, merge, repeat. Thanks 
so much.

> Wishing everybody a happy new year.  Regards,

You too!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/093EC33A-70C8-4CCC-92B4-1B9C00E2071F%40dwheeler.com.

Re: [Metamath] Metamath Website not loading

[David A. Wheeler]

> On Sep 5, 2023, at 6:11 AM, Sophie  wrote:
> 
> The main page gives a 403 Forbidden Error, whilst the subpages give a 404 Not 
> Found Error 

There was a problem with the webpage generation a few days ago, which I fixed 
by forcing an early regeneration. The problem should now be fixed.

The long-term solution is to rewrite the regeneration script, which is 
currently *way* overcomplicated. I've started doing taht, but "real life" keeps 
getting in the way :-).

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/73DDF362-E2F7-4591-8824-27CA497C31BC%40dwheeler.com.

Re: [Metamath] Did someone train a LLM on the set.mm

[David A. Wheeler]

The set.mm repo has a small set of Wiki pages.
I've been putting notes about automated proving, especially AI/ML, here:
https://github.com/metamath/set.mm/wiki/Automated-proving

I hope to someday work on AI/ML for creating Metamath proofs, but I haven't
had a chance to do it. I encourage anyone interested to give it a try, I think 
it's
*extremely* promising.

--- David A. Wheeler


> On Aug 19, 2023, at 8:32 PM, Amaury Hayat  wrote:
> 
> Hi Marcel,
> 
> There were actually several papers based on Transformers for Metamath. You 
> can probably check these two and the reference therein and it will give you a 
> good idea of what was done and what can be achieved (up to last year) :)
> 
> https://arxiv.org/abs/2009.03393
> 
> https://arxiv.org/abs/2205.11491
> 
> For transformers learning more or less complicated specific maths notions 
> (ODE, stability of ODEs, equilibrium in graphs, linear algebra, etc.) you can 
> check for instance https://arxiv.org/abs/1912.01412 (learning to solve ODEs), 
> https://arxiv.org/abs/2006.06462 (learning to predict advance properties such 
> as stability, controllability, etc.),  https://arxiv.org/abs/2112.03588 
> (learning to find equilibrium in graphs), https://arxiv.org/abs/2112.01898 
> (learning linear algebra). There are probably many other references but these 
> can give you a good start and their models and dataset are public.
> 
> Best,
> 
> 
> Le dim. 20 août 2023 à 06:30, 'Marcel Richter' via Metamath 
>  a écrit :
> I had a lot of fun training transformers on some toy data, and now i am 
> thinking what to do next. I was surprised how fast even small transformers 
> lern long multiplication. 
> 
> Anyone know if someone trained a GTP on set.mm yet.
> 
> set.mm is only ~40mb, i guess that is not enough to avoid overfitting really 
> fast. Anyone produced some procedural generated metamath code?
> 
> I belive a well trained model could be of great help as some kind of 
> methamath copilote.
> 
> Have a nice day :D
> 
> -- 
> 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/metamath/1fe3d510-bd01-4097-8d04-6d4baac1f696n%40googlegroups.com.
> 
> -- 
> 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/metamath/CAP92Bfkp3sWACxYbBnK%2Bz9Ah%3DOt4fw8cvewU2VnJKgSr99STeQ%40mail.gmail.com.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/ACE9F6A9-30FC-43E0-8CDD-8D6926F94A5D%40dwheeler.com.

Re: [Metamath] Trouble understanding Deduction style

[David A. Wheeler]

> On Aug 15, 2023, at 10:15 AM, Jim Kingdon  wrote:
> 
> Thanks for saying something. The reference to trud (cited in your "From Td to 
> Ti" section) is supposed to be mptru .
> This has been corrected in git - 
> https://github.com/metamath/set.mm/blob/dde226ae813a3024357bc5b5bccbdda0785c5fe0/mmnatded.raw.html#L277
>  - but has not been updated on https://us.metamath.org/mpeuni/mmnatded.html 
> yet, presumably due to 
> https://github.com/metamath/metamath-website-scripts/issues/2 concerning 
> website updates.

I expect this to be a temporary situation. I'm working on replacing the scripts 
with something much simpler that actually completely works. Personal issues 
have limited the time I've been able to spend on this, but I don't expect it to 
take too long.

> As for an update to the pdf , that might need to await a new volunteer or a 
> whole lotta patience - the last edition was done by someone who totally 
> doesn't have time for a new project at the moment (if I can be so bold as to 
> say that on his behalf).

I wonder who that could be :-).

It's true I don't have time for a new project at the *moment*, but I think we 
do eventually need to update the Metamath book. My current plan is to for me to 
do a mild update, with review by all, and keep Norm's name on the top (since he 
wrote most of the content). I'm not sure when it'll happen, but I do plan for 
it to happen eventually.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/BE71EB7E-2062-4BA2-93B5-0D69FDD01C4F%40dwheeler.com.

Re: [Metamath] Trouble understanding Deduction style

[David A. Wheeler]

> On Aug 15, 2023, at 9:17 AM, Jeroen van Rensen  
> wrote:
> 
> Hello everyone,
> 
> I am reading metamath.pdf and I have a few questions about section 3.9.3 
> Deduction style, specifically the conversion methods between Td, Ti and T.
> 
> T is a statement in closed form (with no hypotheses).
> Td is a statement in deduction form (where all hypotheses are implications 
> with the same antecedent).
> Ti is a statement in inference form (where all hypotheses don't have the same 
> antecedent).
> 
> The section states that is is possible to go from Td to Ti, from Td to T and 
> from T to Ti. I have trouble understanding the first two conversions.
> 
> Take for example:
> • 
> T: !!q -> q
> • Td: p -> !!q |- p -> q
> • Ti: !!q |- q
> From Td to Ti
> 
> "To prove some assertion Ti in inference form, given assertion Td in 
> deduction form, there is a simple mechanical process you can use. First take 
> each Ti hypothesis and insert a T. → prefix (“true implies”) using a1i. You 
> can then use the existing assertion Td to prove the resulting conclusion with 
> a T. → prefix. Finally, you can remove that prefix using trud, resulting in 
> the conclusion you wanted to prove."
> 
> This is how I understand it:
> • 
> Take !!q as a hypothesis
> !!q
> • Add the prefix "T ->" (true implies)
> T -> !!q
> • Use Td to get:
> T -> q
> • Remove the prefix using trud???
> What I don't understand is how you can use trud to go from T -> q to q.
> trud states that for wff q, (q -> T) and not in reverse. Am I missing 
> something here?

Sorry about that! We renamed trud to mptru on Sep 13, 2022.
So you should use mptru instead.

Maybe we should note something in trud.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/4522FE76-8345-4DE9-A7D3-59D02A6FC0BC%40dwheeler.com.

Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space

[David A. Wheeler]

It *appears* to me that us.metamath.org <http://us.metamath.org/> is now 
working properly again,
now that it has more storage space.

Please let me know of any problems with the site.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/B917DB42-BE5E-44C5-B766-E7DC120DD16E%40dwheeler.com.

Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space

[David A. Wheeler]

FYI: I've doubled the storage of us.metamath.org <http://us.metamath.org/> (it 
was only down for a minute to resize things).

That *should* eliminate problems updating the final published results on the 
website.
I guess we'll find out tomorrow!

--- David A. Wheeler


> On Jul 25, 2023, at 11:04 AM, David A. Wheeler  wrote:
> 
> 
> 
>> On Jul 24, 2023, at 5:25 PM, David A. Wheeler  wrote:
>> 
>> All:
>> 
>> I plan to briefly take down us.metamath.org, a few hours from now, to
>> double its storage space.
> 
> New plan: I plan to do this tonight instead.
> 
> --- David A. Wheeler
> 

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/33EBFEE8-7CB8-4639-8674-DBB934C04E7D%40dwheeler.com.

Re: [Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space

[David A. Wheeler]

> On Jul 24, 2023, at 5:25 PM, David A. Wheeler  wrote:
> 
> All:
> 
> I plan to briefly take down us.metamath.org, a few hours from now, to
> double its storage space.

New plan: I plan to do this tonight instead.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/5655DCCB-1B71-4AA6-9562-44ACC6E8AE91%40dwheeler.com.

[Metamath] Expect to take down us.metamath.org for a brief time to increase its storage space

[David A. Wheeler]

All:

I plan to briefly take down us.metamath.org, a few hours from now, to
double its storage space.

As a quick background,d the
us.metamath.org <http://us.metamath.org/> daily downloads the latest things, 
runs update programs,
then updates the *served* pages & serves them.
The us.metamath.org site is currently running out of storage (disk) space, which
means theorems & such are not being updated.
I did some cleanups that I hoped would help, but that's not been enough.

That will cost me more per month, but I believe
this will immediately eliminate the problem so we're back to having
up-to-date theorems there. It's not clear how long it will be down once I start,
but it'll be a one-time event as it resizes the partition.

Thank you!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/AF390425-2DA8-4FD5-8F1B-FD94A684E756%40dwheeler.com.

Re: [Metamath] Submitting a theorem to set.mm

[David A. Wheeler]

> On Jul 17, 2023, at 5:21 PM, Larry Lesyna  wrote:
> 
> I am ready to submit my first theorem to Metamath. I tested it in my local 
> copy of set.mm and I have created a personal fork.  I could submit a pull 
> request, but I think it would be better if my submission could be reviewed 
> before doing so.  I appreciate any advice.

WONDERFUL! We're always delighted to have new contributors.
Jim Kingdom gave some great advice.  Welcome aboard!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/ADE2F615-6313-4B94-BF57-18634E6ECCB3%40dwheeler.com.

Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm.

[David A. Wheeler]

> On Jul 16, 2023, at 9:04 PM, Marshall Stoner  wrote:

>  I do have a good text on ZFC set theory ("Axiomatic Set Theory" by Suppes) 
> and have taken a class on that a long time ago.  It just isn't super formal 
> and doesn't cover logic or proof theory at all.  I'd like to find a better 
> introduction to logic but I'd hate to buy a clone of Mendelson.  It's tough 
> to tell how good a text is based on reviews.

It's not exactly what you're looking for, but you might find this paper 
interesting, which tries to justify the ZFC axioms:

Believing the Axioms. Penelope Maddy. The Journal of Symbolic Logic, 
Vol.53,No.2.(Jun.,1988),pp.481-511.
https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf

It sounds like you're looking for something similar for predicate and 
propositional logic.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/821F29E4-25F3-41DA-8FF0-E35CFEB254A5%40dwheeler.com.

Re: [Metamath] Metamath-lamp version 14 released, now with undo

[David A. Wheeler]

On Fri, 14 Jul 2023 20:44:09 -0400, "David A. Wheeler"  
wrote:

> Metamath-lamp version 14 has been released!

I know I said this is a minor update, but from the point of view of usability, 
I think this is an important change to the tool.

The addition of undo means that you can change your mind. Thus users will feel 
more free to experiment.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/E1qKVTB-X2-I8%40rmmprod07.runbox.

[Metamath] Reminder: We still have Metamath 100 entries to complete!!

[David A. Wheeler]

A reminder - we still have some "Metamath 100" challenge problems that
would be great to complete. The full list of "proofs to be done" are here:

https://us.metamath.org/mm_100.html#todo

For your convenience I've copied the list below.
No, we're not expecting anyone to do #33 (Fermat's Last Theorem)
right now, but some of these seem relatively within our grasp.

If you're not planning to do one, but have tips on how to do it, please post a 
reply.
But it'd be even better to have more done :-).

--- David A. Wheeler

=

• 6. Gödel's Incompleteness Theorem
• 8. The Impossibility of Trisecting the Angle and Doubling the Cube
• 12. The Independence of the Parallel Postulate
• 13. Polyhedron Formula
• 16. Insolvability of General Higher Degree Equations
• 21. Green's Theorem
• 24. The Undecidability of the Continuum Hypothesis
• 28. Pascal's Hexagon Theorem
• 29. Feuerbach's Theorem
• 32. The Four Color Problem
• 33. Fermat's Last Theorem
• 36. Brouwer Fixed Point Theorem
• 40. Minkowski's Fundamental Theorem
• 41. Puiseux's Theorem
• 43. The Isoperimetric Theorem
• 47. The Central Limit Theorem
• 50. The Number of Platonic Solids
• 53. π is Transcendental
• 56. The Hermite-Lindemann Transcendence Theorem
• 59. The Laws of Large Numbers
• 62. Fair Games Theorem
• 82. Dissection of Cubes (J.E. Littlewood's "elegant" proof)
• 84. Morley's Theorem
• 92. Pick's Theorem
• 99. Buffon Needle Problem
• 100. Descartes Rule of Signs


-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/B0B0A51E-D92C-489C-BBE0-DF8E7268040F%40dwheeler.com.

[Metamath] Metamath-lamp version 14 released, now with undo

[David A. Wheeler]

Metamath-lamp version 14 has been released! This is minor update.

The main change is the addition of undo functionality.
By default the tool remembers the last 20 changes
(this is configurable). You can see those last states & restore the one you 
want.

For more information:

Application page (try it out): https://expln.github.io/lamp/latest/index.html
Documentation: https://lamp-guide.metamath.org/
Tutorial videos: 
https://www.youtube.com/playlist?list=PL1jSu6GGefBk3RhHW5Srpc2qxWMqhga9J
Source code repo (including issues and pull requests): 
https://github.com/expln/metamath-lamp

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/B7493F56-321E-493A-87F6-D4880C1A83B4%40dwheeler.com.

Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm.

[David A. Wheeler]

> On Jul 3, 2023, at 10:58 PM, Marshall Stoner  wrote:
> 
> Thanks.  I was not very specific because I was waiting to make sure I was 
> actually subscribed to the group.  I attached the pdf to show you the idea of 
> what I'm doing.  I would like to provide the quickest and easiest way forward 
> to that start of ZFC theory while still being formally precise.  Like you 
> said, there are far too many theorems to easily convert into a "book form" 
> that includes everything.

It's up to you, but one possibility would be create a document in the set.mm 
repo
with the name `mmSOMETHING.raw.html`. These are just normal HTML files, but 
anything in
`...` is processed by metamath-exe to generate nicer-looking HTML for the 
equations.
This is how we generate, for example, mmcomplex.raw.html - this is processed and
turned into mmcomplex.html for use as a final document. There's no obligation 
to use
that mechanism, but you might find it useful.

I've thought about creating a "tour guide" of sorts that points out and 
explains the highlights
(without going into the details of *every* theorem) - it sounds like you might 
have a somewhat
similar goal. If it's in the set.mm repo, it can be updated along with the rest 
of set.mm.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/A659D0DC-5DB5-4D10-B7D9-CFB0660EE959%40dwheeler.com.

Re: [Metamath] Video of "Introduction to Metamath-lamp, part 3"

[David A. Wheeler]

> On Jun 26, 2023, at 1:47 AM, Igor Ieskov wrote:
> Hi David,
> All three parts are great. I have not found any issue.

Thanks! Anyone who's interested in the full playlist of Metamath-lamp tutorials 
can go here:
https://www.youtube.com/playlist?list=PL1jSu6GGefBk3RhHW5Srpc2qxWMqhga9J

All: please "like" any of the videos if you liked them; that makes the Youtube 
algorithms happy.

> BTW, I didn't know that hypotheses in the explorer are marked with such large 
> circles in Firefox. In Chrome those circles are smaller. I will try to fix 
> this.

I wouldn't worry about it. It's distinct and that's what matters.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/B2A86777-7993-4DF8-813F-82AE9631DA22%40dwheeler.com.

[Metamath] Metamath-lamp version 11 has been released!

[David A. Wheeler]

All:

Metamath-lamp proof assistant version 11 has now been released!
This is a proof assistant for Metamath that can run directly on your
web browser, including one on your smartphone.
You can use it here: https://expln.github.io/lamp/latest/index.html

Major additions in version 11:
* Added an "explorer tab" and dynamic tabs for existing proofs, enabling users 
to examine the current context at any time.
* Works well on smartphones (e.g., supports "long-click" or "long-tap")
* More unified UI - all edits by default use a "long-click".
* Supports identifying one provable statement as the "goal statement" and 
treats it specially, making the UI easier to use.
* Visualization can be enabled or disabled per justification
* More control over which fields are displayed during editing

Documentation is available at: https://lamp-guide.metamath.org/

Videos showing how to use Metamath-lamp version 11:
"Introduction to Metamath-lamp, part 1" - https://youtu.be/b-RfoUuQpAQ
"Introduction to Metamath-lamp, part 2" - https://youtu.be/WOp2xQ8mEE4
"Introduction to Metamath-lamp, part 3" -  https://youtu.be/Aqp3jAM2b60

I'm posting this on behalf of @expln, who actually wrote the tool;
I'm just trying to help potential users by writing some documentation & making 
videos.
<https://github.com/expln/metamath-lamp/issues/120>

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CDE8F7A0-0E49-4BE0-AD13-47E8064F67CD%40dwheeler.com.

[Metamath] Updated video of "Introduction to Metamath-lamp, part 2"

[David A . Wheeler]

I have an updated version of the video "Introduction to Metamath-lamp, part 2":
https://youtu.be/WOp2xQ8mEE4
In this video I've improved the explanation around addition is associative, and 
also
added a demonstration that metamath-lamp's automation could have found it 
directly.

Last-minute comments welcome. It's currently unlisted;
I soon plan to switch it to "public".

Part 1 now has the last few useless seconds removed:
https://youtu.be/b-RfoUuQpAQ
and again, I plan to switch this from "unlisted" to "public" soon.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/A2D5D152-F042-4921-B5C9-AD052F1680F1%40dwheeler.com.

[Metamath] Draft Metamath-lamp video, part **2**

[David A. Wheeler]

And here's a draft version of a video for "Introduction to Metamath-lamp, part 
2":
https://youtu.be/GZIXJp4QepU

Again, this is "unpublished" so I can redo if there's a serious problem, please 
let me know of one.

This is a follow-on to the draft part 1, here:
https://youtu.be/b-RfoUuQpAQ

There were earlier comments about the problem of using metamath-lamp
without clear instructions. My hope is that these videos, plus the 
documentation at
<https://lamp-guide.metamath.org <https://lamp-guide.metamath.org/>>, will 
provide useful instructions.
I'll eventually make more videos, but I'll need time for that :-).

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/EFC02447-962A-486A-97EC-18EC60A273D8%40dwheeler.com.

[Metamath] Metamath-lamp video, part 1

[David A. Wheeler]

I intend to make some videos to help people learn how to use metamath-lamp,
in the same way that I made videos for mmj2.

Here's my part 1, which is just a quick intro & tries to help people who
"stumble" into the video & may not know what a Metamath is:
https://youtu.be/b-RfoUuQpAQ

Let me know of any serious problems with this part?
That video is "unpublished" in the sense that the link isn't public, so
I can re-record it if there's a serious problem.

Actual content to follow, probably as a "part 2" instead of trying to merge 
them.
I intend to show 2+2=4 as my (first) demo, in case you weren't sure if that was 
true :-).
I'll use an updated lamp-guide as my script.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/58CF3612-0DF8-4D0D-B8FA-94393EA15B0D%40dwheeler.com.

[Metamath] Metamath website page updates continue

[David A. Wheeler]

I have yet another proposed change to the Metamath website.
This focuses on updating the FAQ on the Metamath home page,
with a few tweaks elsewhere. E.g.:
* I moved links to much-less maintained material to the "other.html" page,
  e.g., Metamath Music.
* The home page no longer tells people to email Norm.
* A new FAQ entry is a brief memorial to Norm.

The proposed change is here (click on "files changed"):
https://github.com/metamath/metamath-website-seed/pull/9

As always, comments/suggestions/reviews are very welcome!

I stopped at the "Downloads" section, which needs a cleanup,
but that work is for a future day.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C620B94E-93B1-47DA-8F1C-745EA071A087%40dwheeler.com.

Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it

[David A. Wheeler]

Here is my latest attempt to define Metamath - comments?

> Metamath is a simple and flexible computer-processable language that
> supports rigorously verifying, archiving, and presenting mathematical proofs.

This is in part a response to Jim Kingdom, who
noted that he emphasizes "checking with a computer". Fair enough,
so I thought putting "rigorously verifying" first would be sensible.
At first I was worried iif putting "rigorously" first would be confusing, but I 
think it's far;
Metamath really *does* provide added rigor for archiving and presenting.

Please post feedback and/or approval of this & related changes here:

https://github.com/metamath/metamath-website-seed/pull/8

I realize not everyone cares about the front page, and that's fine,
but I think it's important to update these pages to help potential newcomers.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/73A596A8-3133-46CA-A1C3-0E612F7C9215%40dwheeler.com.

Re: [Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it

[David A. Wheeler]

This pull request proposes an update to the early part of the us.metamath.org
website main page:

https://github.com/metamath/metamath-website-seed/pull/8

Comments welcome.

The rest of the page also needs updating, but it took me a little while just to 
get this far.
If we keep working on making improvements it'll be a *lot* easier for
newcomers to understand what this Metamath thing is all about.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/E4966258-3F6A-4B48-9383-0132D1EEF9D8%40dwheeler.com.

Re: [Metamath] How are typecodes used/enforced by the Metamath program?

[David A. Wheeler]

> 
> 
> 
> On Mon, Jun 5, 2023 at 1:43 AM Humanities Clinic  
> wrote:
> Hihi, I have read most of Dr Megill/Wheeler's Metamath book, as well as most 
> of the MPE pages, and I understand that typecodes are used to specify the 
> type of a variable in $f statements.
> (1) How and when does Metamath ensure the types are "enforced"? When does it 
> throw an error? (Oh, please do let me know which part of Dr Megill/Wheeler's 
> book has the answer if I have missed it.)

> On Jun 6, 2023, at 1:32 AM, Mario Carneiro  wrote:
> Most theorem applications involve subproofs showing that the substitutions 
> are well typed. For example if you apply ax-mp, this has two main premises |- 
> ph and |- ( ph -> ps ), but also two syntax subproofs "wff ph" and "wff ps". 
> So you have to prove that your substitution is in fact a well formed formula 
> before you can apply it, and the $f hypotheses can be used as the base case 
> here - if your formula is a variable like "ch" then you can apply wch $f wff 
> ch $. to prove "wff ch".

As always, Mario gave a fantastic answer. Here are a few additional notes that 
may help you understand it.

A Metamath proof *always* includes the steps necessary to create the 
expressions (statements & parts of statements) used in the proof. The 
verification process checks those steps to ensure that the types are correct in 
all cases. These steps are sometimes called "inessential". The HTML published 
proofs normally don't show the inessential steps for theorems, but these steps 
*do* show for axioms (since for an axiom there are no other steps to show). You 
can easily use the metamath-exe program to show every step, even the 
inessential ones, at your option. The development version of metamath-lamp can 
also show the inessential steps or not (at your option).

You might look at axiom ax-ext in set.mm:
  https://us.metamath.org/mpeuni/ax-ext.html
Steps 1 & 2 let us introduce set variables z and x, which are type setvar.
Step 3 uses the justification "wel" to create "z e. x" *and* allows the verifier
to determine it's a wff.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/9BA1807A-203C-4685-A7A8-D4A6BD83D6EE%40dwheeler.com.

Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

[David A. Wheeler]

> On Jun 5, 2023, at 8:48 AM, Thierry Arnoux  wrote:
> 
> Yes, the PR has not been merged in yet, so until then you will need check my 
> branch out.
> 
> This feature required an "XML" library and I've kept it optional, so you will 
> only be able to access it if the program is compiled with the "xml" feature, 
> like so:
> 
> cargo run --features xml -- ../set.mm/set.mm --time --export-graphml-deps 
> deps.graphml
> 
> Or 
> 
> cargo build --features xml

I appreciate making it optional.

Can you make it so the *default* is to include it, and then optionally exclude 
it?
That way, people can use options to build it for special purposes, but the
"out of the box" functionality has whatever people might like?

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/03E6D2BE-FC76-4663-A563-9BE08D9DF2A1%40dwheeler.com.

[Metamath] Updating the metamath website - esp. "What is Metamath" & what's distinct about it

[David A. Wheeler]

I think we need to update the "main" pages of the metamath website,
e.g., the main <https://us.metamath.org/>.
Implementing this will primarily involve changes to the repo:
https://github.com/metamath/metamath-website-seed especially:
https://github.com/metamath/metamath-website-seed/blob/main/index.html
For example, I'd like to update its information & make changes to
further welcome potential new contributors.

To do that, at the top of the page (before the table) I'd like to have ONE 
sentence
that says "what Metamath is" along with a link to more info. Here's my proposed 
text:

> Metamath is a simple, robust, and flexible computer-processable language for 
> archiving, presenting, and rigorously verifying mathematical proofs. See the 
> FAQ for more details.

We'd then update the FAQ. Early in the FAQ I'd like to have updated text
that explains in more detail what Metamath is, along what is
*distinct* about Metamath.
The goal is to help newcomers understand what Metamath is, in today's context.
Below is an attempt at those initial entries,
based on the text of the website & the Metamath book.

I'm sure it needs work. I'd love to hear suggestions.

--- David A. Wheeler

=

Q: What is Metamath, with a little more detail?
A:
Metamath is a simple, robust, and flexible computer-processable language for 
archiving, studying, and rigorously verifying mathematical proofs.
Metamath allows you to state your axioms (assumptions), then state theorems and 
their associated proofs.
A collection of axioms and proofs depending on them is called a "database", and 
we support several databases
for various axiomatic systems.
While simple, Metamath is also powerful; the Metamath Proof Explorer (MPE) 
database has over 23,000 proven theorems and is one of the top systems in the 
“Formalizing 100 Theorems” challenge. <https://www.cs.ru.nl/~freek/100/>
Metamath supports rigorously archiving mathematical knowledge in a computer 
database, providing precision,
certainty, and the elimination of human error.

Q: What is distinctive about Metamath?
A:
Metamath is probably unlike anything you have encountered before
Here are distinctive traits of Metamath compared to other top systems for 
formalizing mathematics:

* The Metamath language is simple and robust, with an almost total absence of 
hard-wired syntax. We believe that it provides about the simplest possible 
framework that allows essentially all of mathematics to be expressed with 
absolute rigor.
* Metamath is not tied to any particular set of axioms, instead, axioms are 
defined in a database.
* Metamath final proofs show every step, no exceptions, where each step
  is *only* an application of an axiom or a previously-proved statement.
  Most other proof systems allow statements (like "simp", "auto", or "blast")
  which only assert that a proof could be found instead of
  showing every step. Metamath's approach makes it possible for anyone to 
follow backwards every
  step of every proof. This also makes verification fast, because
  the system does not need to rediscover proof steps.
* Many tools support Metamath, instead of one "canonical" tool that in practice 
everyone uses.
  Metamath was originally implemented by the "metamath-exe" tool, but today you 
can use Metamath without using the original tool.
* The Metamath verifier has been re-implemented in many different
  programming languages, so verification can be done by multiple
  independent implementations. This greatly reduces the risk of accepting an 
invalid
  proof due to an error in the verifier.
* Substitutions (the fundamental operation in Metamath)
  are easy to understand, even by those who are not
  professional mathematicians. Anyone can look at a proof, then click on any 
step
  to see why that step is justified, and repeatedly follow that process back to 
axioms.
* Proofs stay proven.  In some systems, changes to the system's
  syntax or how a tactic works causes proofs to fail in later versions,
  causing older work to become essentially lost.
  Metamath's language is
  extremely small and fixed, so once a proof is added to a database,
  the database can be rechecked with later versions of the Metamath program
  and with other verifiers of Metamath databases. 
  If an axiom or key definition needs to be changed, it is easy to 
  manipulate the database as a whole to handle the change
  without touching the underlying verifier.
  Since re-verification of an entire database takes seconds, there
  is never a reason to delay complete verification.
  The set.mm began development in 1992 and proofs from that year
  are still in use.
  This aspect is especially compelling if your
  goal is to have a long-term database of proofs.

Of course, other systems may have advantages over Metamath
that are more compelling to you, depending on what you value.
Some users of Metamath also use or develop

Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

[David A. Wheeler]

> On Jun 6, 2023, at 7:33 AM, Humanities Clinic  
> wrote:
> 
> With assistance on the Github repo page itself, I was able to solve the 
> problem, appreciated it.
> 
> I have found that both on the web pages of MPE and on the GraphML output from 
> running, metamath-knife set.mm --time --export-graphml-deps deps.xml, 
> dependencies between definitions are missing.
> 
> For example, df-grp is defined in terms of the following constants:
> Mnd 
> Base 
> `
> +g
> 0g
> (And all other "primitive" constants" like { A. ...)
> 
> Hence, each constant can be a node, and there can be an edge for each "used 
> in the definition of" relation.
> 
> Can this sort of graph be extracted from set.mm using metamath-knife, or be 
> obtained by any other means?

I'm sure metamath-knife could be modified to do that.

Another approach, though a little painful, is that you could scrape the 
generated HTML about set.mm to get this information.

I don't remember if metamath-exe has an option to list the constants in use 
(other than when generating the HTML). It obviously *has* that information 
internally.

--- David A. Wheeler


-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/8D6DA1C8-5816-4C2B-95E8-9E4C1E4E4391%40dwheeler.com.

Re: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional?

[David A. Wheeler]

> On Monday, June 5, 2023 at 9:18:51 AM UTC+8 samiro.d...@rwth-aachen.de wrote:
> '=' stands for class equality: https://us.metamath.org/mpeuni/wceq.html (e.g. 
> equality of numbers)
> '↔' stands for the logical biconditional: 
> https://us.metamath.org/mpeuni/wb.html (i.e. equality of truth values)

> On Jun 5, 2023, at 1:26 AM, Humanities Clinic  
> wrote:
> 
> Erm yes I know that.. But it's a little confusing when one sign should/can be 
> used instead of the other.. Can someone clarify?

Sure! If the left & right sides are classes (including sets), use "=".
If the left & right sides are wffs (that is, values that are true or false), 
use "<->".

So you'd say A = B and ( ph <-> ps ), not the other way around.
The constant true is represented as "T." and the constant false is "F.",
so you'd compare to them using "<->". Here's a true statement:
( T. <-> A. x x = x )

While we're mentioning it, set.mm is picky about parentheses. Here are the 
conventions:

* When a function that takes two classes and produces a class is applied
  as part of an infix expression, the expression is always surrounded by
  parentheses.  For example, the use of "+" in ( 2 + 2 ).
* Predicate expressions in infix form that take two or three wffs
  (a true or false value) and produce a wff are also always
  surrounded by parentheses, such as ( ph -> ps ).
* In contrast, a binary relation
  (which compares two classes and produces a wff)
  applied in an infix expression is *not* surrounded by parentheses. This
  includes set membership, for example, "1 e. RR" (1 is a member
  of the set of real numbers) has no parentheses. This also includes "=".

You can find other set.mm conventions in:
* set.mm general conventions - https://us.metamath.org/mpeuni/conventions.html
* set.mm label naming conventions - 
https://us.metamath.org/mpeuni/conventions-labels.html

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/F49861B9-4EFE-47B5-9DFB-89F4D2D26A48%40dwheeler.com.

Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

[David A. Wheeler]

> On Jun 4, 2023, at 9:14 AM, Humanities Clinic  
> wrote:
> 
> I am stating more specifically the goals I have in mind when I asked: 
> https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com?utm_medium=email_source=footer
> 
> I need to explore the "graph" of statements in set.mm. Specifically, I need 
> to (1) find all sinks and sources quickly (2) Isolate one walk/path/trail 
> between two specified nodes (3a) MOST IMPORTANTLY: With arrow keys on the 
> keyboard, navigate between adjacent nodes. Up arrow - for the parent of the 
> node. Down arrow - for the child of the node. Left and right arrows - for the 
> siblings of the node (3b) I need to explore the subgraph of (only) all 
> definitions in the way outlined in (3a), so I need to be able isolate this 
> subgraph from the entire graph.

I think building on Thierry's code will get you there.

It's a different visualization, but you might also be interested in my video 
"Metamath Proof Explorer (set.mm) contributions visualized with Gource through 
2020-04-29" at <https://www.youtube.com/watch?v=LVGSeDjWzUo>.

This video shows the set.mm database's structure and growth over time. Each 
little circle represents an assertion (mostly theorems). It's structured by 
section and subsection, not by internal theorem dependencies. Even so, it may 
be of interest to you. The code to generate this is all publicly available.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/ECFCA016-49FC-4BFE-94D4-F4B27CB75BB9%40dwheeler.com.

Re: [Metamath] Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

[David A. Wheeler]

> 
> 
> On 04/06/2023 15:14, Humanities Clinic wrote:
>> I am stating more specifically the goals I have in mind when I asked: 
>> https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com?utm_medium=email_source=footer
>> 
>> I need to explore the "graph" of statements in set.mm. Specifically, I need 
>> to (1) find all sinks and sources quickly (2) Isolate one walk/path/trail 
>> between two specified nodes (3a) MOST IMPORTANTLY: With arrow keys on the 
>> keyboard, navigate between adjacent nodes. Up arrow - for the parent of the 
>> node. Down arrow - for the child of the node. Left and right arrows - for 
>> the siblings of the node (3b) I need to explore the subgraph of (only) all 
>> definitions in the way outlined in (3a), so I need to be able isolate this 
>> subgraph from the entire graph.


> On Jun 4, 2023, at 4:11 PM, Thierry Arnoux  wrote:
> I've quickly written an extension to metamath-knife which generates a GraphML 
> file with all theorem dependencies. You can find the PR here:
> https://github.com/david-a-wheeler/metamath-knife/pull/112
> It adds an option "export-graphml-deps", so that the tool can be called using:
> metamath-knife set.mm --time --export-graphml-deps deps.xml
> which generates a "deps.xml" GraphML file.
> The file generated using the current version of set.mm is around 60Mb, 
> includes 43922 nodes and 1324402 edges.


Thierry: Thanks so much! That looks really helpful.

Clearly what's needed now is something that can read a GraphML file and provide 
the UI desired.
I don't know what tools can do that, but I did a quick search and found 
information about GraphML viewers.
These links might be helpful.:
* yWorks' yEd tools - https://www.yworks.com/products/graphmlviewer#editors
* Gephi - https://github.com/gephi/gephi
* https://stackoverflow.com/questions/30928008/view-graphml-file (you can use 
graphviz)
* https://en.wikipedia.org/wiki/GraphML

If you have a tool with the interface desired, but requires a different input 
format,
I imagine it shouldn't be hard to convert GraphML into what you need.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/873B9FC5-AFAB-46ED-A0A9-3E6FA30AC39B%40dwheeler.com.

[Metamath] "Metamath-lamp Guide" now visible at: https://lamp-guide.metamath.org/

[David A. Wheeler]

All:

The "Metamath-lamp Guide", explaining how to use metamath-lamp,
is now available here:

https://lamp-guide.metamath.org/

It's much prettier now, both on screen and when printed.
This page is automatically regenerated when
changes are merged into the main branch of:
https://github.com/metamath/lamp-guide/
So if you have suggestions/improvements, please create
issues or pull requests there.

Thanks!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C168DA15-99F0-4290-BCA7-1F77476D8908%40dwheeler.com.

[Metamath] Re: I intend to create a new metamath org repository named "lamp-guide"

[David A. Wheeler]

> On May 29, 2023, at 6:26 PM, David A. Wheeler  wrote:
> 
> All:
> 
> I intend to create a new metamath org repository named "lamp-guide"
> to host the "Metamath-lamp Guide".

I have created a new metamath repo:
<https://github.com/metamath/lamp-guide>

to host this guide. I believe this repo implements this:
https://github.com/expln/metamath-lamp/issues/65

Please file issues if you see any issues, or even better, please provide pull 
requests :-).

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/EAAE2B09-F619-46D3-A545-FB4AEFC41703%40dwheeler.com.

[Metamath] I intend to create a new metamath org repository named "lamp-guide"

[David A. Wheeler]

All:

I intend to create a new metamath org repository named "lamp-guide"
to host the "Metamath-lamp Guide".
This is at the request of the maintainer of metamath-lamp.
Below is the backstory.

Let me know ASAP if there's a problem. I can't imagine what the problem
would be, though, so I intend to do this soon.
Everything is under the MIT license, though if that's
an issue I think I can simply relicense it as the author of this material
(e.g., as MIT OR CC-BY-4.0).

--- David A. Wheeler



I've been working to create a guide for the
proof assistant metamath-lamp. The guide currently in the
metamath-lamp repo:
https://github.com/expln/metamath-lamp

However, the maintainer of metamath-lamp (Igor Ieskov / @expln)
would prefer that the guide be in its own separate repository instead
of being intermingled with the code:
https://github.com/expln/metamath-lamp/issues/65

I intend to keep the
history of the guide's development in case that's useful, so I'll
probably make a copy of it using git & push it back.
(I don't want GitHub to say "this is a fork of XYZ", so I probably
won't use GitHub's fork command unless someone knows how to undo that).

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2590BEAB-A417-4057-AADB-247F9FF0AA27%40dwheeler.com.

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

[David A. Wheeler]

> On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote:
> 
> Ask and ye shall receive!! As of this morning the first draft of the 
> metamath-lamp guide is available here: 
> https://github.com/expln/metamath-lamp/blob/master/docs/guide.md 

> On May 27, 2023, at 10:17 AM, 'Alexander van der Vekens' via Metamath 
>  wrote:
> I wanted to proof ( 5 + 7 ) = ; 1 2.

Ouch, that's a worst case goal for metamath-lamp when compared to mmj2.
The mmj2 tool has automations *specifically* for simple calculations like this,
while metamath-lamp does not. But it's a valid goal, so carry on!

> The replacement of a temporary variable is a little bit cumberson: if you 
> want to replace  by 6, you cannot change it at one place (and then it is 
> replaced everywhere, as in mmj2), but you have to click A (apply a 
> substitution to all statements), then enter  and 6 manually.

In mmj2 you still need to manually replace the work variable () by its 
replacement somewhere (6).
The current assumption in metamath-lamp is that for substitutions you'll always 
use the replacement command instead.

That said, I think you're right, it would be better if metamath-lamp also 
allowed people to
just edit a work variable into an expression and have unify automatically do 
the replacement.
I've added that as a proposal here:

https://github.com/expln/metamath-lamp/issues/43

> In the following, a second line with 5 e. NN0 was created (with the massage 
> This statement is the same as the previous one - '2' ) - at first, it was not 
> possible to get rid of it, I succeded, however, after a while...

You should be able to select the statement & then choose "delete". If that 
didn't work, I'd love to know why.

> At the end, I needed about one hour to finish the proof successfully (with 
> metamath.exe it was done within a few minutes).
> To summarize, I think metamath-lamp is not stable/intuitive enough to be 
> suitable for a beginner at the moment.
> 
> Finally, it would be very helpful if screen shots were available in this user 
> guide.

Good point. In the long term I intend to create a video, just like I did with 
mmj2,
but screen shots are still a good idea.

Thanks for the feedback! I think you're right that metamath-lamp needs 
improvements
in its UI & capabilities. However, I think some of that suggests a need to 
improve its documentation
to clarify how to use it; mmj2 also has some oddities that work fine once you 
know what they are.
I'm going to work on improving its documentation to hopefully make it easier.

I still think it is helpful to have at least one tool that work "without an 
install" and can
immediately work on smartphones.
mmj2's automations and some specific mechanisms give it power that metamath-lamp
currently lacks, but some people may be unwilling to go through the effort of 
installing a tool
just to try it out. I'm hoping that metamath-lamp can be, at the least, a way
to entice people into trying to create metamath proofs themselves.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/94A90A04-E450-4228-A412-7060542EACA7%40dwheeler.com.

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

[David A. Wheeler]

> On May 26, 2023, at 4:19 PM, 'Alexander van der Vekens' via Metamath 
>  wrote:
> 
> I just had a look at metamath-lamp itself and at the video. It is actually 
> very impressive, but, to be honest, I have no idea how to use it. There is an 
> urgent need for instructions, a user guide, a tutorial, etc. before it can be 
>  recommened for beginners...

*Absolutely* 100% agreed!! As I said:

> A problem for metamath-lamp is the lack of instruction showing how to *use* 
> it.
> ... But it wouldn't take much to create
> a basic help document & a few videos to help people get started.

Ask and ye shall receive!! As of this morning the first draft of the
metamath-lamp guide is available here:
https://github.com/expln/metamath-lamp/blob/master/docs/guide.md

I intend to add more to it. I think it needs at least 3 worked examples of 
proofs,
with more desirable.  It currently shows how to prove 2+2=4, and that should 
help.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/1F56F8ED-E284-476F-9F63-003B9CBBC34B%40dwheeler.com.

[Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

[David A. Wheeler]

I've been experimenting with the proof assistant metamath-lamp, including
abusing poor Igor with a variety of suggestions :-).

In short: I'm quite impressed with metamath-lamp.
Of the functions that I routinely *use* in mmj2,
the only one that I really miss is mmj2's automation routines.
I'm sure automation could be added to metamath-lamp (it's not a lot of mmj2).
What's more, metamath-lamp is quite useful even without them.
It has a few minor issues due to its newness, but there's a lot to like.

More importantly, metamath-lamp brings something new & *VERY* valuable:
It can be used without installing *anything*. That makes it an *extremely* 
helpful tool for people
who might be interested in trying to develop metamath proofs, because it
eliminates that startup time. Metamath-lamp even works well on a
good smartphone (it currently has a minor UI problem due to the lack
of an "alt/opt" key, but that is easy to fix). Even if someone switches tools
later, metamath-lamp is a great "gateway drug" :-).

I would encourage others to check out metamath-lamp:
* Source code Repo: <https://github.com/expln/metamath-lamp>.
* Use it: <https://expln.github.io/lamp/latest/index.html>
* Video demo (no audio): 
https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?usp=sharing

A problem for metamath-lamp is the lack of instruction showing how to *use* it.
metamath-lamp has a number of tooltips, but it's easy to not notice them.
It also has no help file or document, and the only demo video has no sound.
In contrast, mmj2 comes with a nice long hands-on tutorial, and I created a 
Youtube
video that walks through that whole tutorial. But it wouldn't take much to 
create
a basic help document & a few videos to help people get started.

We currently have a "Q: Where do I start?" on the metamath.org front page that 
ends with this:

You can experiment with simple proofs in the Metamath Solitaire applet. To 
actually create real metamath proofs, you'll want to download a tool. A common 
tool is mmj2. David A. Wheeler produced an introductory video, "Introduction to 
Metamath & mmj2" [retrieved 4-Aug-2016].


I would like to modify this text to help welcome people in, but also note at 
least metamath-lamp, and
probably other tools as well.

I propose changing it to something like this (at least once better tutorials 
are available):


To create real metamath proofs, you'll want to download a tool. We suggest 
trying one of these tools for creating metamath proofs:
* metamath-lamp. This is an easy-to-use web-based GUI proof assistant. You 
don't need to install anything - just use your browser. To learn how to use it, 
see [video not appearing in this film]. Go *here* to start using it.
* mmj2. This is a GUI proof assistant written in Java, so you must install it 
as well as a Java Virtual Machine (JVM) to run it. This is probably the most 
common tool currently in use for creating metamath proofs. It includes some 
automation to automatically complete some proofs. David A. Wheeler produced an 
introductory video, "Introduction to Metamath & mmj2" [retrieved 4-Aug-2016].
* metamath-exe. This is the original tool, written in C, for supporting the 
metamath formal system. This is a text command line tool for supporting 
metamath and includes a proof assistant. See the [metamath book] for more 
information on how to use it. The name of the command is "metamath", but we 
often call it "metamath-exe" to distinguish this program from other programs 
and the underlying Metamath system. If you do not like using GUIs or you have 
specialized needs, this might be the proof tool for you.

Once you learn how to use one tool, it's very easy to learn how to use another, 
so we encourage you to "just start" with any one.


I'm sure it could be worded better, and maybe we should list other tools or 
link to a longer list of Metamath proof assistants. The point is to help people 
get started - I'd love to see even more people join in the fun of creating and 
improving Metamath proofs.

I didn't list some other proof assistants because it was my understanding 
they're inactive:
* mmpp <https://github.com/giomasce/mmpp>
* Igor <https://github.com/Drahflow/Igor>
Metamath Zero is a different beast, so I didn't list it either.

We probably need to fix up the "tools" list page, and link to that: 
<https://us.metamath.org/other.html>.
But I think showing new users a huge list is overwhelming.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/A628CEEF-6D8D-493C-AC15-B88C6F738953%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

> On May 9, 2023, at 7:53 AM, Igor Ieskov  wrote:
> 
> mm-lamp v10 is released with few new features:
> 
>   • Autocompletion for parentheses - when you type an opening parenthesis 
> followed by a space then the closing parenthesis is added automatically and 
> the cursor is placed in between those parentheses.
>   • Syntax validation and “syntax aware” selection.
>   • Graphical visualization of justifications.
> 
> The below demo almost repeats the proof from the v1 demo but using the new 
> features this time:
> 
> https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?usp=sharing

This is awesome!. Thanks for continuing this work.
I think the ability to "create proofs without installing anything" is a 
potential game-changer
in terms of making it easier for people to start creating Metamath proofs.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/B3F8957C-E3A4-43C7-86F0-49850F409393%40dwheeler.com.

Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs

[David A. Wheeler]

> On May 7, 2023, at 12:23 PM, Jon P  wrote:
> Re this one thing I wondered about is whether adding english text between the 
> statements might help a language model understand what is happening? It would 
> be very repetitive so maybe it makes no sense but here is an example. ...

The underlying Metamath proof format *does* support comments internal to the 
proof.
See the Metamath book appendix E ("Metamath Language EBNF").

However, in *practice* tools don't use that information to generate output, nor 
do they
take any steps to keep such comments. I'm not sure anyone is seriously 
interested in processing them.
Maybe we should, but then we'd have to think about how to handle changes.

> I think maybe that makes it easier to understand what is happening and gives 
> the language model something to grip on to which training?

Perhaps, but no one's trying to do that. Currently, if there's a trickiness, 
it's documented in the high-level description of the statement as a whole. If 
if's more sophisticated, it might be better split out as its own theorem.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/42E62100-7A9C-4B2E-BC50-7D82E6F62F5A%40dwheeler.com.

Re: [Metamath] Speculations on how to help machine learning systems generate metamath proofs

[David A. Wheeler]

On March 25, 2023, I posted some speculations on how recent AI/ML improvements 
might be applied to create Metamath proofs. Like any hypothesis, experiments 
are necessary to see whether or not they're true. That said, I think good 
hypotheses are a helpful first step.

I have a few other notes & speculations. My hope is that these posts will 
inspire some of those experiments. See below for more.

--- David A. Wheeler



First, there is a *lot* going on to make AI/ML technologies more widely 
available.

For example, we have "OpenLLaMA: An Open Reproduction of LLaMA":
https://github.com/openlm-research/open_llama

That also includes efforts to make it easier to run these kinds of tools 
locally and/or on servers controlled by others.
For example, WebGPU has been recently implemented by Chrome & Firefox is 
expected to release that soon.
I expect that will make it easier to run machine learning algorithms, including 
on client-side JavaScript
(where it might be possible to run an ML algorithm without having to install 
anything, just use your browser).

I can' summarize it all, there's too much going on. If someone can point us to 
sites which are keeping
track of this, or to key new results, that'd be awesome.

Second, I think we should keep thinking about ways we could output Metamath 
proofs
to make it easier for machine learning systems
to learn how to create new proofs. I discussed a lot of that in my March 2023 
post, such
as presenting proofs "backwards" (start from the goal).

One challenge is that most outputs include step numbers and step references.
Those are challenging for an ML tool to
figure out what the underlying relationship is, because it has to convert those 
numbers into
"spatial" relationships that aren't obvious. For training purposes it might be 
best to do something
else, thought it's not clear what. One option would be to omit step numbers,
and for references use relative steps (+1). Or instead of step numbers, use 
reference names
based on the label of the statement that uses.
We could also add {...} to surround groups, to
help the ML system learn groupings. Other ideas welcome.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/F31053C1-966F-459B-9CC4-5945D8B81FFC%40dwheeler.com.

Re: [Metamath] eqsb3lem vs eqsb3v

[David A. Wheeler]

> On May 2, 2023, at 4:08 PM, Zheng Fan  wrote:
> 
> Why do we have these two identical lemmas in the database, none of which has 
> any discouragement tag? 

Probably because no one noticed.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/8B2230F4-C969-4E38-A6C3-64E617B9DC6B%40dwheeler.com.

[Metamath] Speculations on how to help machine learning systems generate metamath proofs

[David A. Wheeler]

As you know, AI (artificial intelligence) / ML (machine learning)
systems have *already* generated Metamath proofs.

However, the recent breakthroughs in AI/ML, particularly in
large language models (LLMs) like GPT-3 & GPT-4 (which is really multimodal)
make me hope that these newer systems can create (or help create) proofs for the
Metamath system, such as for the set.mm and iset.mm databases.
I'm hoping some people reading this email will be doing that!

I've had some experience over the years with AI/ML systems, so I have
some speculations of how we might help such systems be more likely to
be successful. Like all speculations, they may not be true; they are
hypotheses based on educated guesswork. Still, hypotheses are a good
starting point for experimentation, and I'm hoping that some of them
will be correct & lead to better proofs.

Some of this thinking was inspired by the paper by Bubeck et al,
"Sparks of Artificial General Intelligence: Early experiments with GPT-4"
<https://arxiv.org/abs/2303.12712>. You might to read it and/or see the summary 
video
"'Sparks of AGI' - Bombshell GPT-4 Paper: Fully Read w/ 15 Revelations"
by AI explained <https://www.youtube.com/watch?v=Mqg3aTGNxZ0>


--- David A. Wheeler

=== Speculations ===

1. Many of the newer generative models have an odd limitation: they start
generating text without knowing where they'll end up as a conclusion.
This is highlighted by Bubeck et al several times as "lack of planning".

One way to address this limitation today would be train the system & have it
generate metamath proofs "backwards". That is, the first statement is the goal,
followed by the items supporting it (repeatedly). Many humans develop proofs 
this
way anyway (start with what you want, then work backwards).

Of course, this is a general problem, and there may be general solutions.
"Memory Augmented Large Language Models are Computationally Universal"
by Dale Schuurmans <https://arxiv.org/abs/2301.04589> shows that
"transformer-based large language models are computationally universal when 
augmented with an external memory."
Even with such augmentations, it may still easier for proof generation tools to
work "backwards" by default, as that is likely to *tend* to be easier for them.

2. More training data == better results in general.
Newer systems & models can learn more quickly, but it's still true that more 
training
data tends to produce better results. Therefore, I think it'd be helpful to
*automatically* generate proofs with a variety of terms to help the system
learn the underlying rule. For example, set.mm's ax-mp says:
min ⊢ 휑
maj ⊢ (휑 → 휓)
ax-mp   ⊢ 휓
... but it would be easy to generate examples that use the general assertion.
If you don't care exactly what you're proving, as long as it's true, you can 
generate
lots of true statements :-). But this would give the systems more to work with.

Databricks says that their work "suggests that much of the qualitative gains in 
state-of-the-art models like ChatGPT may owe to focused corpuses of 
instruction-following training data, rather than larger or better-tuned base 
models."
<https://www.databricks.com/blog/2023/03/24/hello-dolly-democratizing-magic-chatgpt-open-models.html>

3. Critical reasoning lacks an “inner dialogue”. Newer models *are* able to 
create
models to answer questions to a limited extent, but they're not great at it, 
and this
really hurts their mathematical capabilities. See the Bubeck paper for more.

I think this can be helped by training the system on *not*
just the sequence of steps, but by training it in a way that shows the 
*results* of the
each intermediate step (the text after "|-" in set.mm and iset.mm). This 
provides the
models with more information on the internal state, instead of having to figure 
it out.

4. Starting with existing models is probably the better step forward.
Instead of starting from scratch, I'd start with a pre-trained model.
Those seem to have worked out broader concepts of locality that make results
more likely to be good.

5. Supporting tool use might be helpful.
It might be helpful to have pre-created "tools" that automatically prove common 
cases.
One of the more remarkable capabilities of GPT-4 & friends is that they can 
invoke
*other* tools. Just like tool use by humans, tool use by LLMs makes them able 
to handle
far more complex problems than they could otherwise. Being able to invoke 
something
that can generate solutions for tasks it would otherwise struggle with (like a 
SAT solver
or numeric calculation proof) might make hard tasks trivial.

5. In the long run this may be completely doable on a single computer or even 
phone.
There are also many efforts to create open models that can be used for any 
purpose
(OpenAI doesn't create any open models, its name is rather misleading).
Really, there's 

Re: [Metamath] mmj2 error js does not exist

[David A. Wheeler]

> On Mar 6, 2023, at 4:07 PM, jannik vierling  wrote:
> 
> The pull request is now opened and waits to be merged :)
> Jannik.

Spectacular!

Those are curious can follow it here:
https://github.com/digama0/mmj2/pull/65

There's some tweaking under discussion, but I'm very happy to see this!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/89D49792-573F-441F-824A-534D8D5EFE7F%40dwheeler.com.

Re: [Metamath] mmj2 error js does not exist

[David A. Wheeler]

> On Mar 5, 2023, at 11:02 AM, Benoit  wrote:
> 
> Thanks for the modification, Jannik.  We won't have to downgrade Java 
> anymore.  Is it possible to merge it with the original repo, so that we do 
> not have multiple places to choose from ?

Indeed! Please post a pull request, this is definitely of interest :-).

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3B3E4320-278D-4852-94BF-B1152BC7E95E%40dwheeler.com.

Re: [Metamath] mmj2 error js does not exist

[David A. Wheeler]

> On Mar 2, 2023, at 4:36 PM, Mario Carneiro  wrote:
> 
> It sounds like the nashorn JS engine was removed from a later version of JDK, 
> and the empty list following the prompt suggests there is no replacement. 
> Without it you won't be able to run any macros, although you might be able to 
> install it manually? The easiest thing to do is probably just to downgrade to 
> JDK 9.

Ah, of course! I should have noticed the openjdk version more carefully.

Oracle has long warned that they'd stop supporting JavaScript from Java using 
the Nashorn JS engine, but mmj2 depends on it.

--- David A. Wheeler


> 
> On Thu, Mar 2, 2023 at 3:53 PM David A. Wheeler  wrote:
> 
> 
> > On Mar 2, 2023, at 3:23 AM, William Mitchell Jr  wrote:
> > 
> > running mmj2 in the mmj2jar directory produced this error:
> > 
> > mmj.pa.MMJException: E-UT-1502 You attempted to use a macro, but the 
> > default Macro language 'js' does not exist. Use 'MacroLanguage,xxx' with 
> > one of the following installed languages:
> > 
> > This is the git version (uncompiled) running on
> > arm64
> > Debian Linux
> > openjdk-18
> 
> Weird. I have no idea what's going on. Anyone else?
> 
> --- David A. Wheeler
> 
> -- 
> 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/metamath/CCC54F28-92E6-4C7D-B8EF-1A993DB50449%40dwheeler.com.
> 
> -- 
> 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/metamath/CAFXXJSsoTbBby4QCy6zh-JEF%2B3qM80bSASPLJ4zk9RkA4%2B1C%2Bw%40mail.gmail.com.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/E3147E7A-1887-4361-8E23-4A692B0A0615%40dwheeler.com.

Re: [Metamath] Future website directions

[David A. Wheeler]

> On Thu, Mar 2, 2023 at 12:53 PM David A. Wheeler  
> wrote:
> 2. The text just runs off to the right, instead of going over multiple lines, 
> making long ones unreadable. That's important but easy for the non-MathML 
> case (just a little CSS), though I don't know how hard that is for 
> MathML/MathJax.
> 
> On Mar 2, 2023, at 4:33 PM, Mario Carneiro  wrote:
> This is a pretty fundamental problem with MathJax style displays, and I don't 
> have a good solution. LaTeX generally isn't great about automatic line 
> breaking inside mathematics, but metamath routinely involves very large 
> formulas, so although this looks good for the mid-sized examples the large 
> ones really suffer. A related issue is that mathjax isn't really able to cope 
> with having thousands of large and complex formulas on a page and the CPU 
> time / draw time really spikes on some of the examples. For MM0 I'm planning 
> to mostly just sidestep this issue by using ASCII-first displays, perhaps 
> using unicode or programming fonts with ligatures but not much more. That way 
> line breaking is limited to just pretty printing which can feasibly be 
> written with a handcrafted JS library.

That makes sense. I don't *object* to beautiful presentations, but if that's 
unsolved, we could generally prefer pointing to the Unicode versions (where 
long formulas are easily handled).

MathJax is well aware of the need for automatic line breaking. They hope to 
have s version 3 that resolves it:
https://docs.mathjax.org/en/latest/output/linebreaks.html
https://stackoverflow.com/questions/40628064/mathjax-automatic-line-breaking-when-resizing
... I'm fine with letting them solve the problem & we use their solution. I 
don't know when they'll actually do that (if ever).

>  
> 3. I think it's important we support existing URLs. That's easy with 
> pregeneration, just rename to taste. If this is dynamically generated, that 
> would require some changes to support the .html endings *and* support 
> returning static pages.
> 
> I don't think this will be difficult no matter what we do, since we can set 
> up all the necessary routing in nginx.

Not *difficult*, but some are harder than others if we *dynamically* generate.
In nginx you would typically specify a location pattern as a parameter, and if 
it matches,
call a program (e.g., using fastcgi). Here's an example:
https://www.nginx.com/resources/wiki/start/topics/examples/fastcgiexample/

You'd *like* to have the web server directly serve static files (they're good 
at that!),
but currently directories like "mpeuni" have a lot of files, some of which 
might be dynamically generated
while others are probably statically generated. Typical websites put them in 
separate directories,
to make it easy to tell them apart.

If they're all dynamically generated via the same program, or all statically 
generated, then that's moot.

> I am not above potentially making mpegif redirect to mpeuni though (or a 
> future URL scheme), or serving only dynamic pages for deprecated formats. I 
> think we should try to make https://us.metamath.org/mpeuni/areacirc.html link 
> to a theorem about the area of a circle in perpetuity but not necessarily 
> serving exactly the same HTML as it does today.

Agreed. Heck, even if we stay with metamath-exe I would think we'd be open to 
improvements.
But since many people link to our pages, I want them to keep working to get 
"something interesting".


> 4. This one omits many of the capabilities of the metamath-exe generator, 
> e.g., compare with <https://us.metamath.org/mpeuni/areacirc.html>.
> By the way (and I realize this wasn't directed at both tools), mm-web-rs was 
> designed explicitly as a carbon copy replacement for metamath-exe generation, 
> and supports all of these things. (Thierry's generator as I understand it is 
> more of an exploration of what we could have if we break with the traditional 
> format.)

> IIRC if you open them in a browser side by side the result is identical 
> except for distinct variable groups, which use a different (arguably better) 
> heuristic for collecting $d pairs into cliques. (Exact clique cover is an NP 
> hard problem, though, so some amount of approximation is required.)

Better is better!

> I think the variable coloring heuristic uses some hard-coded typecode names 
> so it is not suitable for general databases; there are actually quite a few 
> aspects of the web site generator that are tailored for set.mm which should 
> probably use $t commands instead.

We could start with hard-coding, then move towards supporting a general form.
I agree that in the long term we want to be general.

I suspect type code coloring primarily useful to new users... but since we *do* 
want to new users/readers, that's still relevant. We could even add it late

Re: [Metamath] mmj2 error js does not exist

[David A. Wheeler]

> On Mar 2, 2023, at 3:23 AM, William Mitchell Jr  wrote:
> 
> running mmj2 in the mmj2jar directory produced this error:
> 
> mmj.pa.MMJException: E-UT-1502 You attempted to use a macro, but the default 
> Macro language 'js' does not exist. Use 'MacroLanguage,xxx' with one of the 
> following installed languages:
> 
> This is the git version (uncompiled) running on
> arm64
> Debian Linux
> openjdk-18

Weird. I have no idea what's going on. Anyone else?

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CCC54F28-92E6-4C7D-B8EF-1A993DB50449%40dwheeler.com.

Re: [Metamath] Future website directions

[David A. Wheeler]

> On Feb 27, 2023, at 5:27 PM, Thierry Arnoux  wrote:
> 
> And since we're there, I'd also like to recall this other live site:
> 
> http://metamath.tirix.org:3030/mpests/toc
> 
> All pages are rendered dynamically, there are 3 modes:
> 
> - ASCII - http://metamath.tirix.org:3030/mpeascii/areacirc
> - Unicode - http://metamath.tirix.org:3030/mpeuni/areacirc
> - MathML - http://metamath.tirix.org:3030/mpests/areacirc
> 
> Source code here. https://github.com/tirix/metamath-web

That *is* nice. The MathML in particular is nice.

Is there a list of Metamath database view generation tools? I can think of:
- https://github.com/digama0/mm-web-rs
- https://github.com/tirix/metamath-web
I know there are others. At least, there was one that let you expand/contract 
proof steps, which one was that?

So clearly we should talk about options to completely replace the current
process. Obviously we *could* replacing pre-generation with generating them 
dynamically;
alternatively we run these other tools as pre-generators.
I really *do* want it to be possible to view the key results without 
client-side JavaScript,
but this code & Mario's can clearly meet that need. In the case of tirix's code,
just view ASCII and/or Unicode and you're fine.

I do have a few specific comments on tirix's tool. They're all fixable of 
course:

1. I can't read most of the text because most of the text has low contrast. 
That includes description, step numbers, hyp refs, ref blue boxes, text 
expressions in mpascii, & navigators.  Can you please change its CSS to have 
strong text contrast? It should be readable by color-blind people on a phone in 
sunlight. Creating strong text contrast *important" but also *easy* - it's just 
some CSS tweaks.
2. The text just runs off to the right, instead of going over multiple lines, 
making long ones unreadable. That's important but easy for the non-MathML case 
(just a little CSS), though I don't know how hard that is for MathML/MathJax.
3. I think it's important we support existing URLs. That's easy with 
pregeneration, just rename to taste. If this is dynamically generated, that 
would require some changes to support the .html endings *and* support returning 
static pages.
4. This one omits many of the capabilities of the metamath-exe generator, e.g., 
compare with <https://us.metamath.org/mpeuni/areacirc.html>. That includes:
  Distinct variable group:   푥,푦,푅
  Allowed substitution hints:   푆(푥,푦)
  Colors of variables (off, setvar, class) ... this one isn't as important to 
me & would be a lot of work, so I'm not fussy there.
  Syntax hints (with links to them)
  List of axioms used (with links)
  List of definitions used (with links)
  List of theorems that reference it (with links)


--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/508D4E31-7626-4F3F-A0DA-F78E5B2FAFF1%40dwheeler.com.

[Metamath] Metamath website - current status

[David A. Wheeler]

All, FYI, here's the current status of the main Metamath website metamath.org & 
us.metamath.org.

First: a few days ago I finally got the metamath.org DNS registration 
officially transferred from Norman Megill to me. My thanks to his partner, 
Susan Cass, who helped me work through the process. Norm & I had talked about 
what would happen when he died, and we had *started* to prepare for that 
eventuality. However, we had expected that he had much more time than he did, 
so we weren't fully prepared. I miss him, as I know many of you do. That said, 
we're moving forward. I've put Susan Cass on the "bcc:" of this message, 
because I want her to know that we are working to keep Norm's passion project 
moving forward.

Since that DNS transition is official, I thought now would be a good time to 
tell everyone the current state of the metamath.org website. In short: 
everything seems to be working & under control. Here are the key points:

* I have control over the DNS name metamath.org. Should I unexpectedly die (and 
that's not my preference), I intend for Mario Carneiro to immediately take 
over. Registration is currently with domainmonger & automatically renews. Fees 
aren't due until 2030, and the current price there is $18/year. Its 
configuration redirects requests of "metamath.org" to  
<https://us.metamath.org/mm.html>.
* The website itself is running on linode. Up to this point that's cost me 
$5/month, but they've just been bought out, and I was informed today that 
they're adding 20% to their fee on April 1. So it'll be $6/month ($72/year). At 
the moment I plan to just leave it on linode (as it takes effort to move), but 
I want to ensure we *can* move. As you know, the website has https:// (TLS) 
running, has various security countermeasures enabled (such as package 
auto-updates & HTTPS headers), and updates the proofs & such daily. The update 
scripts are horrendously messy, but they work & the plan is to clean them up 
over time. More generally, my intent is to enable people to continuously 
improve things.

If you're in good financial shape & want to chip in to help fund it, send me an 
email; I'll send my home address & you can send me a check. However, do *NOT* 
feel obligated to send any money, especially if you are (for example) a 
recently-minted PhD in mathematics who is working for a university :-). While 
I'm not made of money, that's not much money, and many of you have incredible 
gifts in mathematics & related fields. I'd rather people spent their resources 
on other stuff like new/improved proofs, improved tools, and better 
documentation. I can afford a few dollars to keep a website up, and 
improvements in those areas are more important to me.

In the longer term I'd like to create a nonprofit association to manage these 
things. The goal would be to set up something that could outlive us all. Its 
notional purpose would be something like "Enable and encourage 
computer-verified formalization of mathematics.". The association would control 
the domain name, GitHub account, and so on, and would have board members & such 
to make decisions. Setting up an association takes time & money, though, so I 
haven't done anything serious about it yet. For the moment, the key is to keep 
improving so that there's something worth creating an association for.

My thanks to everyone who's ever contributed in any way. You are appreciated.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2350B41E-1B76-42D6-A709-635889B5FC26%40dwheeler.com.

Re: [Metamath] Future website directions

[David A. Wheeler]

> On Feb 26, 2023, at 11:04 PM, Mario Carneiro  wrote:
> 
> FYI I did a fairly comprehensive HTML modernization in mm-web-rs 
> [https://github.com/digama0/mm-web-rs/blob/master/src/render.rs] (which is 
> basically a clone of the metamath-exe theorem page generator), which among 
> other things lowercased all the tags and made it pass the w3c validator again 
> (there is a link at the bottom of most pages but they don't pass more modern 
> HTML standards and still use things like ).

Awesome!

When I spoke I was thinking more about the static HTML files in:
https://github.com/metamath/set.mm
https://github.com/metamath/metamath-website-seed

... but yes, we want to modernize those as well.

--- David A. Wheeler

> 
> On Sun, Feb 26, 2023 at 11:52 AM David A. Wheeler  
> wrote:
> I completely agree, a page on AI/ML would be great. The pages could do with a 
> refresh anyway, many places suggest contacting Norm.
> 
> Norm used an HTML 1.0 convention of using uppercase tags. I suggest that new 
> text use lowercase tags as a style choice
> It doesn't matter technically, but it is the current convention, and it would 
> make it easier to see which parts are unchanged.
> 
> On February 25, 2023 5:33:02 PM EST, Mario Carneiro  wrote:
> A page with short descriptions of papers and projects using Metamath for AI 
> would be great to put on the website. I think it would be good publicity for 
> both metamath and the AI systems, and maybe we can solicit the paper authors 
> to write the descriptions and provide related links as well.
> 
> On Sat, Feb 25, 2023 at 5:27 PM Jon P  wrote:
> Re the subject of LLMs being trained on metamath this new model called LLama 
> from facebook is interesting. It seems to be smaller than other systems and 
> it looks like they're already training on metamath.
> 
> https://ai.facebook.com/blog/large-language-model-llama-meta-ai/
> 
> It links to this page and this paper which talk about the matheamtical aspects
> 
> https://ai.facebook.com/blog/ai-math-theorem-proving/
> 
> https://arxiv.org/abs/2205.11491
> 
> It's interesting they talk about the "metamath benchmark". Maybe one approach 
> is to take that and have a page which presents the metamath database for 
> training (kind of like the .txt files or json or whatever is preferred) and 
> then has some notes about the papers that have already been published about 
> it (gpt-f, LLama) and their results. Might be interesting.
> 
> On Sunday, February 19, 2023 at 10:39:55 PM UTC David A. Wheeler wrote:
> 
> > On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler  
> > wrote: 
> > My first choice when building a website, where it's easily achieved, is 
> > static rendering (statically-generated pages) where the most important data 
> > is visible without client-side JavaScript. Those are easily understood, 
> > incredibly hard to attack, trivial to configure, trivial to mirror, support 
> > security/privacy-conscious users, etc. Some sites *cannot* be developed 
> > this way, of course!! But using that as the "starting point" helps clarify 
> > "what else do you need?" - that is, it forces a discussion of "what are the 
> > unspoken requirements?". It's also where we are in the metamath site. 
> > 
> > With pre-rendering as a replacement for dynamic server side stuff, we can 
> > still do most of the things. For example we could prerender all the json 
> > queries and use client side JS to request them when doing cross linking 
> > stuff. This is only made difficult if the set of all queries is infinite, 
> > for example if we can do a search query. 
> 
> 
> > On Feb 19, 2023, at 3:13 PM, Mario Carneiro  wrote: 
> > The main advantages of dynamic rendering are: 
> > (1) quicker turnaround time, e.g. if we want to hastily put up a mm100 
> > theorem on the website; 
> > (2) faster iteration - it is possible to make changes to the server and see 
> > the results ~immediately; 
> > (3) lower storage cost, since we won't have to generate all the HTML for 
> > the web site in advance and just cache important stuff (I assume that most 
> > of the work going into the website build is wasted, since no one looks at 
> > that page before it is next regenerated); 
> > (4) the ability to have many more rendering styles (unicode, gif, text, 
> > latex, mathml, json have all been considered and more are possible) and 
> > more databases, which is a combinatorial problem for the website build 
> > limited by storage space and generation time. 
> 
> Sure. As always, it's all about trade-offs :-). 
> 
> I don't know if quicker turnaround time & such is all that im

Re: [Metamath] Metamatix

[David A. Wheeler]

We have a list of Metamath tools on the website pages. Will you add it? If not, 
let me know and I will add it, I just don't want to duplicate effort.

On February 25, 2023 3:26:02 PM EST, Thierry Arnoux  
wrote:
>Hi all,
>
>FYI, I recently found out about Metamatix
>, a verified implementation of
>a metamath proof checker, written in Coq.
>
>I'm not sure how far the project goes, but it's probably of interest for
>people in this group.
>
>BR,
>_
>Thierry
>
>-- 
>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+unsubscr...@googlegroups.com.
>To view this discussion on the web visit 
>https://groups.google.com/d/msgid/metamath/afe05c58-2988-3f65-89f5-4569b6d507e7%40gmx.net.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/5DBFBC50-D236-4A71-9F55-82392C457A1A%40dwheeler.com.

Re: [Metamath] Future website directions

[David A. Wheeler]

I completely agree, a page on AI/ML would be great. The pages could do with a 
refresh anyway, many places suggest contacting Norm.

Norm used an HTML 1.0 convention of using uppercase tags. I suggest that new 
text use lowercase tags as a style choice
It doesn't matter technically, but it is the current convention, and it would 
make it easier to see which parts are unchanged.

On February 25, 2023 5:33:02 PM EST, Mario Carneiro  wrote:
>A page with short descriptions of papers and projects using Metamath for AI
>would be great to put on the website. I think it would be good publicity
>for both metamath and the AI systems, and maybe we can solicit the paper
>authors to write the descriptions and provide related links as well.
>
>On Sat, Feb 25, 2023 at 5:27 PM Jon P  wrote:
>
>> Re the subject of LLMs being trained on metamath this new model called
>> LLama from facebook is interesting. It seems to be smaller than other
>> systems and it looks like they're already training on metamath.
>>
>> https://ai.facebook.com/blog/large-language-model-llama-meta-ai/
>>
>> It links to this page and this paper which talk about the matheamtical
>> aspects
>>
>> https://ai.facebook.com/blog/ai-math-theorem-proving/
>>
>> https://arxiv.org/abs/2205.11491
>>
>> It's interesting they talk about the "metamath benchmark". Maybe one
>> approach is to take that and have a page which presents the metamath
>> database for training (kind of like the .txt files or json or whatever is
>> preferred) and then has some notes about the papers that have already been
>> published about it (gpt-f, LLama) and their results. Might be interesting.
>>
>> On Sunday, February 19, 2023 at 10:39:55 PM UTC David A. Wheeler wrote:
>>
>>>
>>> > On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler 
>>> wrote:
>>> > My first choice when building a website, where it's easily achieved, is
>>> static rendering (statically-generated pages) where the most important data
>>> is visible without client-side JavaScript. Those are easily understood,
>>> incredibly hard to attack, trivial to configure, trivial to mirror, support
>>> security/privacy-conscious users, etc. Some sites *cannot* be developed
>>> this way, of course!! But using that as the "starting point" helps clarify
>>> "what else do you need?" - that is, it forces a discussion of "what are the
>>> unspoken requirements?". It's also where we are in the metamath site.
>>> >
>>> > With pre-rendering as a replacement for dynamic server side stuff, we
>>> can still do most of the things. For example we could prerender all the
>>> json queries and use client side JS to request them when doing cross
>>> linking stuff. This is only made difficult if the set of all queries is
>>> infinite, for example if we can do a search query.
>>>
>>>
>>> > On Feb 19, 2023, at 3:13 PM, Mario Carneiro  wrote:
>>> > The main advantages of dynamic rendering are:
>>> > (1) quicker turnaround time, e.g. if we want to hastily put up a mm100
>>> theorem on the website;
>>> > (2) faster iteration - it is possible to make changes to the server and
>>> see the results ~immediately;
>>> > (3) lower storage cost, since we won't have to generate all the HTML
>>> for the web site in advance and just cache important stuff (I assume that
>>> most of the work going into the website build is wasted, since no one looks
>>> at that page before it is next regenerated);
>>> > (4) the ability to have many more rendering styles (unicode, gif, text,
>>> latex, mathml, json have all been considered and more are possible) and
>>> more databases, which is a combinatorial problem for the website build
>>> limited by storage space and generation time.
>>>
>>> Sure. As always, it's all about trade-offs :-).
>>>
>>> I don't know if quicker turnaround time & such is all that important.
>>> A "local" server run (by, say, a tool that called metamath-knife) would
>>> have the same
>>> tooling problems: You'd need to set up additional tools to run the tool
>>> locally.
>>>
>>> Of that list, the ability to have more rendering styles is possibly the
>>> most compelling of that list.
>>> But exactly what rendering styles?
>>>
>>>
>>> > > We can obviously use a program to dynamically generate many of the
>>> pages instead, but what would it need to do?
>>> >
>>> > For 

Re: [Metamath] Future website directions

[David A. Wheeler]

> On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler  
> wrote:
> My first choice when building a website, where it's easily achieved, is 
> static rendering (statically-generated pages) where the most important data 
> is visible without client-side JavaScript. Those are easily understood, 
> incredibly hard to attack, trivial to configure, trivial to mirror, support 
> security/privacy-conscious users, etc. Some sites *cannot* be developed this 
> way, of course!! But using that as the "starting point" helps clarify "what 
> else do you need?" - that is, it forces a discussion of "what are the 
> unspoken requirements?". It's also where we are in the metamath site.
> 
> With pre-rendering as a replacement for dynamic server side stuff, we can 
> still do most of the things. For example we could prerender all the json 
> queries and use client side JS to request them when doing cross linking 
> stuff. This is only made difficult if the set of all queries is infinite, for 
> example if we can do a search query.


> On Feb 19, 2023, at 3:13 PM, Mario Carneiro  wrote:
> The main advantages of dynamic rendering are:
> (1) quicker turnaround time, e.g. if we want to hastily put up a mm100 
> theorem on the website; 
> (2) faster iteration - it is possible to make changes to the server and see 
> the results ~immediately;
> (3) lower storage cost, since we won't have to generate all the HTML for the 
> web site in advance and just cache important stuff (I assume that most of the 
> work going into the website build is wasted, since no one looks at that page 
> before it is next regenerated); 
> (4) the ability to have many more rendering styles (unicode, gif, text, 
> latex, mathml, json have all been considered and more are possible) and more 
> databases, which is a combinatorial problem for the website build limited by 
> storage space and generation time.

Sure. As always, it's all about trade-offs :-).

I don't know if quicker turnaround time & such is all that important.
A "local" server run (by, say, a tool that called metamath-knife) would have 
the same
tooling problems: You'd need to set up additional tools to run the tool locally.

Of that list, the ability to have more rendering styles is possibly the most 
compelling of that list.
But exactly what rendering styles?


> > We can obviously use a program to dynamically generate many of the pages 
> > instead, but what would it need to do?
> 
> For the first version, I would aim simply to replicate the behavior / look 
> and feel of the current metamath web pages. That's what I implemented in 
> https://github.com/digama0/mm-web-rs . Once we have something that can 
> potentially replace the functionality of metamath-exe it will be easier to 
> consider incremental improvements, in an architecture where we can do fancy 
> things if we want.

Okay, but what is desirable that is *different* long term? I think there are 
plausible good answers,
but it'd be good to have some idea about them.

> One technique that I use in the MM0 web pages is to use the HTML as the data 
> source: put all the proofs in a table like they would be normally, but 
> perhaps not as marked up as they should be. Then postprocess it with JS to 
> add all the markup and make additional server requests if needed. That solves 
> the "make the JS-disabled experience palatable" problem, since you just get 
> the basic version of the page if no JS is running.

Yup! Sounds like a great approach.

> The sort of thing that might require additional data is parsing support; for 
> example with MM0 pages the formulas are printed in ascii but ideally they 
> would reflow using the layout algorithm, using correct indentation. Metamath 
> web pages are horrible at this; they get good per-token rendering but 
> reflowing is garbage so hopefully you just don't have too-long lines. mmj2 
> has a nice indenting formatter (actually there are several algorithms 
> available); wouldn't it be nice if that could be done in-browser so that it 
> adapts to the viewport width? If the lines are sent in HTML as token strings, 
> then that means that the JS has to do the parsing itself so it needs to know 
> the signatures of declarations like 'wi'.

An alternative is to provide HTML in a table (or some other grid), along with 
something that's simpler to parse but not shown to someone just looking at the 
HTML. It could be in an attribute, something with "display: none", whatever. If 
there's a client-side renderer being used, I would want it to be *easy* to 
write, not make it parse complex HTML. The individual theorems aren't big, so 
it'd be pretty easy to include both in one file.

> Also expensive queries can be hidden behind an expandable drop-down and a 
> se

[Metamath] Future website directions

[David A. Wheeler]

e 
already compress the .mm file because they've gotten big. One possible use 
would be training AI systems, but they'd need to do post-processing of that to 
make it useful for them anyway. My earlier proposal involved trying to create a 
format pre-processed to make it easier for them to read, because if they're 
specially training an ML system, some preprocessing usually gets better results.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/726640EF-94CA-4BD8-A52A-E7238C2331F2%40dwheeler.com.

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

> On Feb 18, 2023, at 4:08 PM, Mario Carneiro  wrote:
> In case it wasn't clear (and it probably wasn't), in a future world in which 
> the default mechanism is some super fancy client side renderer it is still 
> possible to offer a fallback "static site" of HTML pages which is 
> nevertheless not generated in advance and is being served dynamically 
> server-side. This has a relatively small generation cost even if we don't 
> stick a CDN in front of it, but if we do then I think that's a viable 
> approach to having all the HTML pages with basically zero preprocessing, just 
> a smarter server. I would really love it if the only thing the site build 
> needs to do is download and load the latest set.mm .

I understand, that's just a typical dynamically-generated data file and/or HTML 
with possibly front-end JavaScript. Bog standard stuff. Of course, there are 
pluses & minuses with that approach. In the 2010s almost everyone switched to 
that model, today there's a big press back to statically-regenerated sites 
where practical (with Jekyll, etc.) because attackers routinely pop systems 
that do dynamic response.

There are big concerns if you hook up a program written in C to input sent by 
an attacker. Rigorous input filtering would definitely help, but using 
something like metamath-knife as a basis instead of metamath-exe might be 
better. So doing this would involve a nontrivial amount of software, *along* 
with analysis to ensure that it was unlikely to lead to a vulnerability. 
Statically generating files is a much simpler path from where we are. That's 
not to say we must go that way, but it'd take more effort to do full dynamic 
generation *with* confidence in its security.


> I don't think this is a very competitive option though, since you would have 
> to load all of set.mm.

It's more competitive than you might think. Igor's prover loads the whole 
database in a few seconds. That said, I agree with:

> The advantage of pre-processed json files is that when you have a single 
> theorem you want to look at you don't need to request everything and start up 
> a whole client-side MM verifier first.


> What started this thread was trying to see if we could get "free" training on 
> GPT-3 by presenting something easier for them to consume, *without* 
> controlling them. I don't think generating JSON will do that. The JSON 
> certainly could make it easier for organizations who want to specially train 
> ML systems on the existing databases, and are willing to do "a little 
> cleaning" by processing the JSON. If we pregenerate JSON from the .mm 
> databases, the most likely use cases would be to make it easier for rendering 
> tools & ML labs that want to do a little (but not a lot) of work.
> 
> Has anyone asked for this?

Absolutely not!! I was noticing that Microsoft & Google are really doubling 
down on web scanning into GPTs, and trying to see if we could take advantage of 
that.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3E04D159-5A99-485B-8B1E-4C8524CD5D0E%40dwheeler.com.

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

David A. Wheeler:
> I do see big downsides for the use cases listed here though:
> 1. For training a GPT, I fear that the system would focus on "it's a JSON 
> file!" 

> On Feb 17, 2023, at 12:49 PM, Mario Carneiro  wrote:
> I think this is looking at it the wrong way. Stuff trained on the entire 
> internet is going to have a clear upper bound on the precision of the answers 
> it can give. I'm not really interested in supplying a poor quality data 
> source just for the purpose of a speculative application like this. For 
> projects that are actually interested in doing ML specifically on metamath, 
> it is very normal to have some data wrangling by the researchers beforehand 
> to prepare things for the model. This kind of glue code is usually some 
> ad-hoc python script so it helps if we are providing a data source that is 
> easily manipulable.

Sure, ML training normally does a lot of wrangling to make clean data,. I've 
done some ML work myself (not on Metamath, sadly). But since my wallet isn't 
deep, I was speculating that by providing easier-to-train-on text we might get 
some more value out of the investments others are making. I think it'd be 
relatively easy to do, and then we could see if it has a benefit.

> (I'm working on a paper with Josef Urban regarding ATP for metamath and it 
> benefits significantly from metamath-knife as a way of getting information 
> from mm files, but it's not always possible to use mm-knife and if we are 
> going for something more easily digestible from many languages without a 
> dedicated library JSON is a strong choice.)

David A. Wheeler:
> 2. For rendering on the client side, there are big advantages to showing 
> static data
> as straight HTML. For one, people who disable JavaScript can still see it 
> fine.
> Sure, sometimes it's useful to run arbitrary code sent by strangers, but 
> there are good
> reasons to minimize that as a requirement :-). It also means that search 
> engines see
> "what we actually have".
>  

> While I have some sympathy for this argument, I also think it is holding us 
> back a lot. Catering to the least common denominator of no-JS means that our 
> web pages are stuck permanently in web 1.0, with no search functionality, 
> intra-page links, subproof expansion, mathml rendering, go-to-definition for 
> symbols, or a laundry list of other features. Furthermore, doing the 
> rendering client-side means that the cost of transmission is lower which 
> means shorter load times and no need for a two-hour processing phase.

What I want is for *a* way for people to access the basic information without 
*requiring* client-side JavaScript. I see no reason that it be the *only* way 
we provide the information, we already provide it in multiple forms. I just 
want to retain that capability. So you don't need to feel held back :-).

Indeed, you can implement rendering with client-side JavaScript today, just 
download the .mm files. The current CORS setting means that any client-side 
JavaScript program can do that, it doesn't even need to be hosted on 
us.metamath.org. So technically people today can view the generated HTML on the 
website, *or* use any client-side JavaScript/WebAssembly. We "just" need 
someone to write the client-side renderer.

Also, almost everything you listed doesn't require client-side JavaScript. 
Intra-page links work (they're just hyperlinks), subproof expansion works (use 
HTML ), MathML ships in Chromium & Chrome & Firefox (Firefox's support 
is only partial but it's probably more than enough for us) per 
<https://developer.mozilla.org/en-US/docs/Web/MathML>, go-to-definition is just 
another hyperlink, and so on. Basic searches can be supported via a form that 
queries a search engine (e.g., Google).

As far as speed goes, JavaScript is often slower than HTML where both can be 
used. In practice JavaScript files are often quite large, and JavaScript has to 
be parsed, examined, executed, and then its execution must cause document tree 
changes which finally get rendered. Web browsers are *really* good at rapidly & 
progressively rendering HTML. On systems I've worked with, HTML (even with 
server roundtrips) is often *MUCH* faster when measuring paint-to-screen times. 
JavaScript *has* gotten faster over the years, thankfully, but the gap is still 
large. Of course, when you need functionalities only provided by JavaScript 
then you need it. Like all technologies there are tradeoffs.

> On Feb 17, 2023, at 3:52 PM, Cris Perdue  wrote:

> It is a tiny percentage of users who turn off JavaScript. 


I'm one of those people who sometimes turns off JavaScript, and many sites work 
fine. The more you learn about security, the more worrying it gets to "run all 
code sent to your web browser from attackers", especially since all browsers' 

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

> On Feb 16, 2023, at 6:36 PM, Jon P  wrote:
> 
> Mmm yeah interesting, I agree $2600 and then more for inference is quite a 
> lot. I think your original plan might be quite a good one as if multiple 
> groups are going to scrape the web for training data then we might be able to 
> get into a bunch of different models.
> 
> This is an interesting conversation with chatGPT. Seems it already knows 
> quite a lot.

That is *utterly* fascinating. Especially since we certainly didn't present 
data in a format that's easy to train on.
Many of its general-purpose text answers are right, too.

> ChatGPT:
> 6 1,5 eqtrans $p |- TarskiG = TarskiGC $
> 7 subst $e |- ( ( ph -> G e. TarskiGC ) -> ( ph -> G e. TarskiG ) ) $
> 8 hyp $e, ph |- ph $
> 9, 10 mp $e |- ( ph -> G e. TarskiG ) $
> 11 7, 9 mp $e |- ( ph -> G e. TarskiGC ) $
> 12 eqtrans $p |- ( ph -> G e. TarskiGC ) = ( ph -> G e. ( ( TarskiGC i^i 
> TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base f ) / p ]. [. ( Itv f ) / i ]. 
> ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) 
> / x e. ( z i y ) / y e. ( x i z ) ) } ) } ) ) ) $
> 13 6, 11, 12 impbii $p |- ( ph -> ( X .- Y ) = ( Y .- X ) ) $

I compared that to the actual continuation of axtgcgrrflx (below). ChatGPT does 
manage to look similar in terms for format. It doesn't manage to figure out 
much in the way of the actual steps (either statement to use nor resulting 
statement), which is too bad, because that makes not useful even as a proof 
hinting assistant.

That said, it's not particularly trained on it, and the public-available data 
certainly doesn't make it easy to train on. It's possible a tool specifically 
trained on the dataset would do much better.


> Me:
> how many theorems are proven in the metamath database
> 
> ChatGPT:
> As of the latest update to the Metamath database on January 24, 2022, there 
> are a total of 272,443 theorems that have been proven. However, it's worth 
> noting that this number may change as new theorems are added to the database 
> over time.

Looking at just set.mm, it has 203588 statements; 2716 are $a and 40627 are $p.
Once you add the other databases (especially iset.mm), maybe there are around 
270,000 statements
across all metamath databases. So perhaps it's confusing "theorem" with 
"statement".

--- David A. Wheeler



Here's the actual current proof (ChatGPT was given 1-5):
 1 df-trkg   $a |- TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB 
i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p 
, y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. 
( x i z ) ) } ) } ) )
 2 inss1 $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. 
( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ 
{ x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } 
) } ) ) C_ ( TarskiGC i^i TarskiGB )
 3 inss1 $p |- ( TarskiGC i^i TarskiGB ) C_ TarskiGC
 4 2,3 sstri $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. 
( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ 
{ x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } 
) } ) ) C_ TarskiGC
 5 1,4 eqsstri   $p |- TarskiG C_ TarskiGC
 6 axtrkg.g  $e |- ( ph -> G e. TarskiG )
 7 5,6 sseldi$p |- ( ph -> G e. TarskiGC )
 8 axtrkg.p  $e |- P = ( Base ` G )
 9 axtrkg.d  $e |- .- = ( dist ` G )
10 axtrkg.i  $e |- I = ( Itv ` G )
11 8,9,10 istrkgc  $p |- ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. P A. y e. P 
( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- 
z ) -> x = y ) ) ) )
12 11 simprbi$p |- ( G e. TarskiGC -> ( A. x e. P A. y e. P ( x .- y ) = ( 
y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) 
) )
13 12 simpld $p |- ( G e. TarskiGC -> A. x e. P A. y e. P ( x .- y ) = ( y 
.- x ) )
14 7,13 syl  $p |- ( ph -> A. x e. P A. y e. P ( x .- y ) = ( y .- x ) )
15 axtgcgrrflx.1  $e |- ( ph -> X e. P )
16 axtgcgrrflx.2  $e |- ( ph -> Y e. P )
17 oveq1 $p |- ( x = X -> ( x .- y ) = ( X .- y ) )
18 oveq2 $p |- ( x = X -> ( y .- x ) = ( y .- X ) )
19 17,18 eqeq12d  $p |- ( x = X -> ( ( x .- y ) = ( y .- x ) <-> ( X .- y ) = ( 
y .- X ) ) )
20 oveq2 $p |- ( y = Y -> ( X .- y ) = ( X .- Y ) )
21 oveq1 $p |- ( y = Y -> ( y .- X ) = ( Y .- X ) )
22 20,21 eqeq12d  $p |- ( y = Y -> ( ( X .- y ) = ( y .- X ) <-> ( X .- Y ) = ( 
Y .- X ) ) )
23 19,22 rspc2v  $p |- ( ( X e. P /\ Y e. P ) -> ( A. x e. P A. y e. P ( x .- y 
) = ( y .- x ) -> ( X .- Y ) = ( Y .- X ) ) )
24 15,16,23 syl2anc  $p |- ( ph -> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x 
) -> ( X .- Y ) = 

Re: [Metamath] shorter proofs for some theorems in set.mm

[David A. Wheeler]

> On Feb 16, 2023, at 4:14 PM, Igor Ieskov  wrote:
> 
> >  Would you mind taking some steps so we can more easily review & add them?
> 
> Sure. I've just created a pull request. I will gradually update proofs from 
> the main part. I will not touch proofs from mathboxes.

I suggest creating multiple pull requests. That way we can easily accept some & 
not others.


> Below I am providing a list of owners of mathboxes for which I found shorter 
> proofs in order others not to download the file I attached (not sure if 
> posting full names is a good idea):
> AS
> AV
> GS
> JB
> NM
> RP
> TA
> WL

That's fine, we know who they are. To be fair,
their public names are a terribly-kept secret, since they're posted in
<https://us.metamath.org/metamath/set.mm>.
If someone doesn't want to give their real name they can just give their
pseudonym (e.g., Mel L. O'Cat, Drahflow) or abbreviation (KP, ML),
though real names are great because I expect this database to outlive all of us.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/280338AA-0B0B-446C-BCA1-30FE76710954%40dwheeler.com.

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

> On Feb 14, 2023, at 1:46 PM, Jon P  wrote:
> 
> I think that's a great idea David! Seems like very low downside and it would 
> be interesting to see if language models could train on the datasets. 
> 
> There's already an option to Customise GPT3 with additional datasets so once 
> this is ready it could be an interesting experiment to try.
> 
> https://openai.com/blog/customized-gpt-3/

Thanks so much for that link. So I looked into creating a specially-trained 
model
to create metamath proofs. that page points to this pricing model for GPT-3:
https://openai.com/api/pricing/#faq-token

I did a quick estimate of training costs for the top GPT-3 model on
all of set.mm. It comes out to about $2600.
That's less than I expected, and that's easily affordable in a grant (you could 
train multiple times),
but it's not an amount I have pocket change for :-(.
Inference isn't expensive; trying to generate axtgcgrrflx is $0.15 (15 cents).
See below for how I created the quick estimate.
We could do a subset of set.mm (e.g., skip mathboxes, etc.), though fewer 
training examples
would typically produce less-good results.

I can't possibly afford that myself. That said, there are alternatives. There 
are many other
Generative Pre-trained Transformer (GPT) models that are less capable but
also less expensive. My current personal computer is useless
for ML training, but Kaggle.com provides a nice Jupyter notebook interface for 
AI/ML
work that's free to use. Here are some pages that discuss using GPT-2 and 
Kaggle:
https://www.kaggle.com/code/changyeop/how-to-fine-tune-gpt-2-for-beginners
https://www.kaggle.com/code/nulldata/fine-tuning-gpt-2-to-generate-netlfix-descriptions/notebook
https://www.kaggle.com/general/116387

I had also been looking at adding definition checks to metamath-knife, and 
maybe trying to
help this new JavaScript metamath proof assistant. Sigh, not enough time in the 
day :-).

--- David A. Wheeler



=== Cost estimate ===

Here's. cost estimate using https://openai.com/api/pricing/

OpenAI's most powerful GPT-3 model is Davinci. Their charges are:
* Fine-tuned training: $0.0300 / 1K tokens,
* Usage: $0.1200 / 1K tokens.

I did a quick estimate of tokens in the entirety of set.mm using:
metamath 'set scroll continuous' 'set width ' 'read set.mm' 'show statement 
*' 'show proof * /lemmon /renumber' 'quit' | grep -v -- '---' | wc
That yielded 64218080 words. A token is about 4 characters or 0.75 words, so 
for a quick estimate, tokens = 64218080/0.75 = 85624107 tokens.
Fine-tuned training of this entire set = (85624106/1000)*$0.03 = $2569.

Theorem axtgcgrrflx : 942 words, tokens = 942/0.75 = 1256, cost = 
(1256/1000)*$0.12 = $0.15

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/00F786DE-04C9-49B6-B070-365827D5DDD1%40dwheeler.com.

Re: [Metamath] shorter proofs for some theorems in set.mm

[David A. Wheeler]

> On Feb 16, 2023, at 3:12 AM, Igor Ieskov  wrote:
> 
> Hi all,
> 
> I found shorter proofs for some theorems in set.mm. They are listed in the 
> attached file shorter-proofs.zip. There are 108 theorems, 47 in the main part 
> of set.mm, the rest in mathboxes. Some of them are marked as OLD or "proof 
> modification is discouraged", but I included such theorems into that file 
> anyway. Since I am not sure how useful this result is and because of big 
> number of theorems, I verified only the first 5 theorems by metamath.exe. I 
> hope new shorter proofs for remaining theorems are also valid, but there is a 
> chance that some of them are not.

That's awesome!

Would you mind taking some steps so we can more easily review & add them?

We normally accept changes using git & GitHub. That process will automatically
check the validity of the proofs in a variety of ways. I suggest breaking your 
changes
into multiple changes, so that we can easily accept some while considering 
others.
If you don't know how, we can try to help!!

We generally don't change "proof modification is discouraged" so you'll need to 
justify
those changes (or drop them). I don't think we officially reject them for 
"OLD", but I
wouldn't focus your time on them.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3FF44152-DEB1-478F-B0DE-5A1D66A00712%40dwheeler.com.

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

On Wednesday, February 15, 2023 at 8:56:36 PM UTC-5 wrote:
"If anyone has thoughts about applying ML generative text models to 
Metamath proofs
I'd love to hear them."

Hi David et al, 
I'm completing a CS PhD and my dissertation is on neural language models 
and automated/interactive theorem proving. I thought the mm community had 
already worked closely with OpenAI (see papers below) on GPT-f?

We worked with them, but the work was their own, and there's no reason we 
can't do more :-).

What I have in mind is a little different - using a large GPT directly. 
Also, I'm not worried if some of the answers are wrong; they wanted to see 
if it could generate *entire* proofs entirely automatically. I think it'd 
be perfectly reasonable to have a system that *tried* to create a proof, 
and even if it fails, provide some insight that would help a human create 
the proof.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/1e6fa09d-eeec-4311-bda7-190cc0ac6aaan%40googlegroups.com.

Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

> On Feb 14, 2023, at 1:46 PM, Jon P  wrote:
> 
> I think that's a great idea David! Seems like very low downside and it would 
> be interesting to see if language models could train on the datasets. 
> 
> There's already an option to Customise GPT3 with additional datasets so once 
> this is ready it could be an interesting experiment to try.
> 
> https://openai.com/blog/customized-gpt-3/

Thanks so much for the link! That *is* interesting. That links to some tips:
https://platform.openai.com/docs/guides/fine-tuning/preparing-your-dataset
Among their tips:
• "Aim for at least ~500 examples".
We certainly have that!!
• "Ensure that the prompt + completion doesn't exceed 2048 tokens, including 
the separator".
That will exclude some of our proofs. However, if I use axtgcgrrflx as an 
example,
its goal (with 6 hypotheses) and 25-step proof only needs 942 words if I filter
it the way I proposed (and I could shave off a few more words).

So I guess we don't need to wait for someone to scan the web.
We will still need to figure out how to rig the examples to maximize the 
training.
That's way more black art than science. A few links:
https://www.leewayhertz.com/build-a-gpt-model/
https://research.aimultiple.com/large-language-model-training/
https://www.datacamp.com/blog/a-beginners-guide-to-gpt-3

If you're not familiar with large language models (LLMs), a helpful explanation 
is
"Talking About Large Language Models" <https://arxiv.org/abs/2212.03551>.
Fundamentally, these systems look at previous words & statistically
predict likely continuations; with large datasets & parameters, sometimes they 
can do that well.

OpenAI makes it easy to start with their huge GPT-3 model, though it costs money
(I can't get any free credits because I already used some for work).
Kaggle.com lets you run smaller models for free, but smaller models tend to be 
much less capable.

If anyone has thoughts about applying ML generative text models to Metamath 
proofs
I'd love to hear them.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/962ADA90-5DBE-40BD-BEC5-F38C00369E17%40dwheeler.com.

[Metamath] Fyi: Linode rebrand

[David A. Wheeler]

Fyi:

Aa you may know, the us.metamath.org site runs on Linode, a well-respected 
cloud service.

However, Akamai acquired Linode in early 2022.  It's just been announced that 
Linode’s services will now be renamed to Akamai’s cloud computing services:
https://www.linode.com/blog/linode/a-bold-new-approach-to-the-cloud/

As long as this is just a name change, that's fine. However, there are 
definitely some concerned that this will lead to changes that would 
dramatically increase costs and make it a poor match for our purposes, because 
Akamai is kmown for enterprise services that make no sense for: 
https://news.ycombinator.com/item?id=34799273

Should they change things to make them a bad fit, I'll post about the problem 
and look at options. There are some plausible alternatives I've heard of. They 
include Digital Ocean,  Vultr, Hetzner,   Vultr, Hetzner, mnx.io, Vercel, 
Netlify, Heroku, and of course the big ones (Amazon Web Services, Microsoft 
Azure, Google Cloud).

Anyway, I just wanted everyone to know that I am aware of this business 
announcement and I am monitoring it.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/AAA6CA44-AB37-4169-95AF-483626A55F1E%40dwheeler.com.

[Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs)

[David A. Wheeler]

All: I'm thinking it might be a good idea to create a new "database area",
"mpetxt" (to match "mpeuni"/"mpegif"), with many simple text files - 1 per 
proof.
The goal would be to make it easier for AI/ML tools to learn from them
so they perhaps could generate potential proofs.

Current AI (specifically machine learning) tools have made a lot of progress.
In particular Generative Pre-trained Transformers (GPTs) like GPT-3 have managed
to generate remarkably good or at least useful answers in many cases.
However, they aren't magic. Our compressed database files are hard for them to 
learn
from, and the HTML tables we show are human-readable but also
challenging for a computer to learn from. On the other hand, once presented as 
typical text,
they have internal structures that are similar enough to text and code that it's
plausible similar solutions could also work for them.

It appears that Microsoft is going to invest LOTS of money in scraping the web 
to
learn from, using that to train & generate better results. Google appears to be 
rushing
to do the same, as a countermeasure. They can already generate passable code
from prompts in many situations; even when they get it wrong, people report the
results are often helpful as ideas & information for helping to solve the real 
problem.

So I propose generating text files (1/proof) that would make it easier for these
tools to potentially learn how to generate Metamath proofs. Even when they get 
it wrong,
they *might* provide useful tips when trying to create a proof. It's not clear 
to me that
the 140K samples from MPE are enough for them to learn... but they *might* be, 
and the
only way to know is to let them try. The idea is that you'd ask one of these 
tools
"Please complete the following: Metamath proof of NAME in database set.mm NAME 
$p "
and it would complete it with an answer.

Below is an example of what those files might look like. I'd basically exploit
Metamath's "show statement" and "show proof" and try to strip out distractors
that could interfere with machine learning.
It might be wise to make the hypotheses & goal a single long sentence, since 
it's not clear if
users can enter embedded newlines in their prompts, but I haven't done that 
here.
I think it's important that each proof be in its own file, so the ML algorithm 
knows
exactly where they begin and end.

There are currently 40627 $p statements in set.mm. I'm guessing that most will 
fit within
one 4KiB blocks (storage is allocated by blocks), so this would require ~162 
MiB of space.
The us.metamath.org website isn't brimming with space, but we can do that.

--- David A. Wheeler


Metamath proof of pm5.74 in database set.mm
pm5.74 $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> ( ph -> ch ) ) ) 
$= ... $.

PROOF:
 1 biimp $p |- ( ( ps <-> ch ) -> ( ps -> ch ) )
 2 1 imim3i  $p |- ( ( ph -> ( ps <-> ch ) ) -> ( ( ph -> ps ) -> ( ph -> 
ch ) ) )
 3 biimpr$p |- ( ( ps <-> ch ) -> ( ch -> ps ) )
 4 3 imim3i  $p |- ( ( ph -> ( ps <-> ch ) ) -> ( ( ph -> ch ) -> ( ph -> 
ps ) ) )
 5 2,4 impbid$p |- ( ( ph -> ( ps <-> ch ) ) -> ( ( ph -> ps ) <-> ( ph -> 
ch ) ) )
 6 biimp $p |- ( ( ( ph -> ps ) <-> ( ph -> ch ) ) -> ( ( ph -> ps ) -> 
( ph -> ch ) ) )
 7 6 pm2.86d $p |- ( ( ( ph -> ps ) <-> ( ph -> ch ) ) -> ( ph -> ( ps -> 
ch ) ) )
 8 biimpr$p |- ( ( ( ph -> ps ) <-> ( ph -> ch ) ) -> ( ( ph -> ch ) -> 
( ph -> ps ) ) )
 9 8 pm2.86d $p |- ( ( ( ph -> ps ) <-> ( ph -> ch ) ) -> ( ph -> ( ch -> 
ps ) ) )
10 7,9 impbidd   $p |- ( ( ( ph -> ps ) <-> ( ph -> ch ) ) -> ( ph -> ( ps <-> 
ch ) ) )
11 5,10 impbii   $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> ( ph -> 
ch ) ) )


Metamath proof of axtgcgrrflx in database set.mm
axtrkg.p $e |- P = ( Base ` G ) $.
axtrkg.d $e |- .- = ( dist ` G ) $.
axtrkg.i $e |- I = ( Itv ` G ) $.
axtrkg.g $e |- ( ph -> G e. TarskiG ) $.
axtgcgrrflx.1 $e |- ( ph -> X e. P ) $.
axtgcgrrflx.2 $e |- ( ph -> Y e. P ) $.
axtgcgrrflx $p |- ( ph -> ( X .- Y ) = ( Y .- X ) ) $= ... $.

PROOF:
 1 df-trkg   $a |- TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB 
i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p 
, y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. 
( x i z ) ) } ) } ) )
 2 inss1 $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. 
( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ 
{ x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } 
) } ) ) C

Re: [Metamath] Hardened us.metamath.org

[David A. Wheeler]

> On Feb 13, 2023, at 2:00 AM, Mázsa Péter  wrote:
> 
> Thank you David!
> (Have we found a source to at least finance Linode? What about our
> plan to make donations possible?)

The source currently is me.

I'm intentionally doing things to keep the costs low ($60/year website + a few 
dollars for registration).
For the moment I view this as a way for me to contribute to the group.

In the longer term I'd like to set up a "Metamath Association" so things can 
continue
without being dependent on any one person. But let's worry about that later.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/162618C3-7992-44F0-8ED5-7D62C9F3C394%40dwheeler.com.

[Metamath] Hardened us.metamath.org

[David A. Wheeler]

FYI: I've made some tweaks to the website us.metamath.org to harden it further 
against attacks. We formerly had a "D" grade, now it is "A", on this site:
https://securityheaders.com/?q=us.metamath.org=on

To be fair, some of the hardening changes aren't relevant to our current 
configuration, because of other hardening steps I took earlier. Still,  they 
don't hurt, and I'm trying to make the site a challenge to subvert.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/741AB93C-E353-4AC6-A604-FD506DE30A92%40dwheeler.com.

[Metamath] Thanks for being a vibrant & active community

[David A. Wheeler]

All:

I just wanted to thank everyone for helping Metamath be a vibrant & active 
community.

On 2021-12-09, Metamath creator Noman Megill died unexpectedly, and that could 
have been the end. Instead, there have been continuous improvements and 
refinements to the Metamath databases (primarily set.mm and iset.mm). The 
combination of all those improvements is quite heartening. In addition, various 
tools have been created or improved. There's lots to do, no doubt, but there's 
also much to be happy about.

Thanks again.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3C078403-B268-432B-ACE3-D03086B94EB8%40dwheeler.com.

[Metamath] us.metamath.org now has CORS headers, so web client-side applications can access its public data

[David A. Wheeler]

I've modified the us.metamath.org website to have CORS headers.
This will enable web client-side applications can access its public data.
Details below.

--- David A. Wheeler



For security reasons, normally applications that are run on a web browser
(in JavaScript and/or Web Assembly)
have very specific limitations on what they're allowed to do.
In particular, they normally can only contact the site they came from
(this is the "same-origin policy").

However, some JavaScript applications might want to, say,
download the current set.mm database, even if they aren't
being distributed from the us.metamath.org website.

So I've tweaked the us.metamath.org website configuration to add
Cross-Origin Resource Sharing (CORS) headers. These new headers
allow *any* client-side web app to download the pages we publicly serve.
E.g., to get the current version of set.mm, they can download:
https://us.metamath.org/metamath/set.mm
If you think they should be served from a different URL, please discuss!

You can verify this change using:
curl -i https://us.metamath.org/metamath/set.mm 
which will show these new HTTP headers:
Access-Control-Allow-Origin: *
Access-Control-Allow-Methods: GET, HEAD, OPTIONS
Access-Control-Allow-Headers: 
DNT,User-Agent,X-Requested-With,If-Modified-Since,Cache-Control,Content-Type,Range

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C17B7D28-2AA9-45C0-83A1-74B7844E4211%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

(Replying to myself)

Nevermind, I see you can already rename statements in
<https://github.com/expln/metamath-proof-assistant> /
<https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html>!
You clearly demo'ed it too.

When renaming, I *do* wish that either RETURN or ESCAPE would save the name.
I'd prefer shorter default statement names, because I hope to eventually see 
them &
their justification names on screen, but clearly the functionality is there 
already.

I don't see how to create hypothesis statements in the tool, that's probably 
more important
if it's not already there (I didn't see how to do that).
I recommend not using "h" as a prefix to indicate that (mmj2 does that,
but I don't think that should be repeated). I think a button that sets/unsets
a statement's "hypothesis" flag would be great, and then just have a special
onscreen marker for hypotheses.

--- David A. Wheeler


> On Feb 11, 2023, at 10:39 AM, David A. Wheeler  wrote:
> 
>> 
>> On Feb 11, 2023, at 5:00 AM, Igor Ieskov  wrote:
>> 
>> Thanks David!
> 
> You're very welcome! This version really has come a long way:
> https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html 
> 
> One broad suggestion: Could you give it a short & less generic name,
> since there are other Metamath proof assistants?
> Naming is hard, but a short unique name will make it easier to discuss & find.
> And I think this is *very* worthy of discussion & being found.
> 
> You might want to include, on the screen or an "about" option, a link to the
> GitHub repo for the code (so people can review/contribute). I understand that 
> is currently:
> https://github.com/expln/metamath-proof-assistant (MIT license).
> 
> 
>>>>> What are the "key" things you think it's missing, especially in 
>>>>> comparison to mmj2?
>> 
>> 1) I think one of the "key" missing things is ability to help a user to 
>> understand why a statement doesn't unify. As also Thierry noted earlier, 
>> currently the app shows only this message "Justification cannot be 
>> determined automatically".  Or another message is possible too 
>> "Justification for this statement is incorrect". But the app doesn't explain 
>> what is the reason. That's my next goal. I don't see any trivial or simple 
>> solution, so it may take some time to implement.
> 
> Whoa, that's a very high bar.
> 
> I suggest working on other things first & getting back to that later (if 
> ever). In particular, if you add tactics & some automation, the reason for 
> that answer will change, so I suggest working on some predefined 
> tactics/heuristics first.
> 
> If your intent is to just determine why "this statement doesn't unify with 
> this other specific statement", you could try to find the longest match & 
> identify where it finally fails. That seems doable. You could even walk 
> across the database & report the longest incomplete match, but I don't know 
> if it'd be helpful; it'd probably report some very general but unrelated 
> theorems. But I think trying to answer "why can't I automate this in general" 
> is best delayed for a long time. I can be wrong, of course :-).
> 
> 
>> 2) Another, although maybe not a "key" thing, is to have predefined 
>> "tactics" to prove some common cases, for example, prove by induction or 
>> prove by case analysis. This not necessarily has to result in complete ready 
>> proofs, but it may create another new statements which help a user to move 
>> in the desired direction (similar to what I saw in Coq proof assistant). 
>> 
>> 3) As you mentioned mmj2 uses some useful heuristics. I also would like to 
>> add heuristics to improve automatic proof search.
> 
> You could easily combine 2 & 3. Just create a first tactic called "auto" or 
> similar that tries to apply a few simple rules to automatically prove a few 
> simple/common cases. I would devise them so that eventually tactics could be 
> called internally (e.g., by other tactics & maybe even a scripting language). 
> Then make it so a user can select a tactic to a selected set of statements, 
> and you're off.
> 
> mmj2 has a few simple heuristics that it applies automatically its default 
> configuration.
> You could make them either fully automatic or the basis for an "auto" tactic. 
> Code here
> (I think Mario wrote more or all of this):
>> https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js
> Don't feel you have to use it exactly, and it might be better split into 
> different
> tactics (mmj2 doesn't re

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

 final proof, but it might make proving things easier.

> d) proof explorer for the loaded *.mm file

A nice-to-have, but I think you can delay that. The metamath website already 
provides a proof explorer that people can use.
You could provide a link that opens a new tab to us.metamath.org and get a lot 
of the way there.

> e) sharing proofs via URLs (as you suggested and I find this very useful for 
> collaboration). I want to implement this after some time, because when I 
> implement it, I will have to support backward compatibility between different 
> versions, so I want to wait when internal representation of the editor state 
> becomes stable (no frequent changes in the code).

Cool, glad you liked the idea. The rationale for delay makes sense, though I 
can't wait to use it :-). Once you implement 4(e), undo/redo becomes trivial 
(you can let the browser do it!). I suspect there's no need to compress it, and 
you'll get decent results from 
encodeURIComponent(JSON.stringify(your_representation_here)). Of course, 
there's the question of what your_representation_here is :-). Just don't stick 
the whole MM database in there :-).

> Currently my plan is to work on the 1st and 4th items.

As I said, I'd delay #1 (that is likely to be *hard* unless you really back off 
on your plans).
I'd love to see small increments on #4, and a little automation (#2/3).

Regarding user improvements, most people will want to load the current set.mm & 
iset.mm,
so making that easier would be helpful. If there was an easy way to download it 
straight
from the web, that might make getting started easier. I could easily configure
us.metamath.org's CORS settings so the script could always download .mm files 
from us.metamath.org
no matter where it started from.

You might want to walk through the mmj2 tutorial to see what ideas are
worth stealing. I recorded it on Youtube here:
https://www.youtube.com/watch?v=87mnU1ckbI0
The text is here:
https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial

Once you're further along, I'd be happy to work with you to create a tutorial
if you'd like. I'd probably want to build on the same examples from the mmj2 
tutorial.

It's your project, so take my comments with a bucket of salt.
I really do think this is neat though!

--- David A. Wheeler


-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C2593B77-C1F2-45F5-8523-E347EEF5C569%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

> On Feb 10, 2023, at 4:56 PM, Igor Ieskov  wrote:
> 
> Hi all,
> 
> I implemented bottom-up proofs in v5. In order to start proving bottom-up it 
> is necessary to select one statement and click "unify" button. It is not very 
> fast, but for not big statements it works well.
> 
> Demo video - 
> https://drive.google.com/file/d/1cjJnvlNGACAmlEnlvxzInqmIqE5dl-0Z/view?usp=sharing
>   
> In the demo video I am trying to repeat (as close as possible) proof steps 
> from this mmj2 tutorial https://www.youtube.com/watch?v=vE3v175cMKM=217s
> 
> https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html

WOW! That is *so* cool. That looks like enough functionality that it could be 
seriously used,
though I'm sure there are many things that could be added.

The fact that there's no "install" step required for this prover is especially 
neat.
That does reduce a barrier to getting started.
The unification may not be fast, but the demo suggests it's okay.
I suspect there are easy tricks that could make it faster in JavaScript,
and a WebAssembly routine could eventually be added if that becomes a true 
bottleneck.

What are the "key" things you think it's missing, especially in comparison to 
mmj2?

--- David A. Wheeler


> 
> Best regards,
> Igor
> 
> On Monday, January 23, 2023 at 9:51:41 AM UTC+1 Igor Ieskov wrote:
> Hi all,
> 
> I made few changes in v4:
> - short names for work variables (, , ...);
> - variables are highlighted with different colors depending on their types 
> (only in the editor tab);
> - automatic detection of missing disjoint variable groups when applying a 
> substitution (so now substitutions are easier to do for users in the cases 
> like the one with spcgv described earlier in this thread);
> 
> Work variable names and colors are configurable on the settings tab.
> 
> https://igorocky.github.io/mm-proof-assistant/demo/v4/index.html
> 
> Best regards,
> Igor
> 
> On Friday, January 13, 2023 at 10:59:53 AM UTC+1 Igor Ieskov wrote:
> >>> However It looks like for the former, in the example we use, an 
> >>> additional burden is placed on the user to manually add new DV for UI 
> >>> substitutions.
> 
> That's nice to know that my implementation of disjoint checks in the proof 
> assistant is not wrong. Yes, my intent was to not allow (at least to decrease 
> possibility of) creating valid proofs which will fail in metamath.exe because 
> of disjoints or similar kind of issues (my experience in creating MM proofs 
> is very small, so I cannot imagine what kind of issues may arise). So as the 
> very first version I implemented it in the strictest way I could. Now, having 
> your feedback, I will think on how to make it more user friendly. My current 
> ideas what I want to try: 
> 
> a) in the substitution dialog, allow users to temporarily disable disjoints 
> (all at once or only some of them) to see how this affects results;
> b) add missing disjoints automatically if this helps to make substitution 
> valid (once a user permits this);
> c) try to handle automatically simple use cases as in the example with 
> class1->x;
> d) something similar to temporarily disabling disjoints but in cases when 
> "justification cannot be found automatically" to make it easier to understand 
> how disjoints affect unification;
> 
> 
> 
> 
> Best regards,
> Igor
> 
> On Friday, January 13, 2023 at 12:08:31 AM UTC+1 Thierry Arnoux wrote:
> Ok, one more quick remark (now that I know how to use substitutions!):
> 
> Currently, the tool blocks if two steps are the same. One has to manually 
> remove the step, and update any justification using that step.
> 
> MMJ2 automatically merged them, IIRC. It would be very nice to have the same 
> mechanism (automatically updating corresponding justifications too, of 
> course!)
> 
> 
> 
> On 12/01/2023 22:58, Thierry Arnoux wrote:
>> Hi Igor,
>> 
>> Thanks for all answers, and especially the change for the single click!
>> 
>> I understand very well not everything is simple, and you have to move on 
>> step by step.
>> 
>> Concerning the substitution function: thanks to your explanations, I could 
>> make it work in cases which previously blocked!
>> 
>> 
>> 
>> I think here I would make a difference between the UI substitution function, 
>> which is here to help the user, and the substitutions checked when applying 
>> theorems.
>> 
>> The later requires to follow distinct variables requirement, and it's very 
>> nice that your proof assistants follows with that along the way (that is a 
>> weak point of MMJ2 in my opinion, as it seems t

Re: [Metamath] Trouble running mmj2

[David A. Wheeler]

You need to use an older version of the Java Virtual Machine (JVM) to run mmj2.
That may be the problem. I believe that's documented, but maybe that's not 
sufficiently obviously.



> On Jan 23, 2023, at 3:51 PM, M Malik  wrote:
> 
> Hello Metamath people,
> 
> I am sorry if this has been answered before. I installed mmj2 through Github, 
> but I am receiving this error when I attempt to open "mmj2-java8.jar" file.
> 
> Error: mmj.pa.ErrorCode@61e717c2A-UT-0007 RunParmFile not found or Security 
> Exception. Input file name = null System message follows: null
> 
> Any thoughts?
> -Malik.
> 
> -- 
> 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+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/metamath/57c0eb95-db89-4cb8-9a04-66262c2dfadbn%40googlegroups.com.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/D8F12035-0E0A-45A6-AD23-586494C47810%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

On January 11, 2023 2:42:10 PM CST, Igor Ieskov  wrote:
>
>
>Hi Thierry,
>
>*>>> It's possible to edit a step's formula using ALT-left click, why not a 
>simple click? (that's why I naturally tried first, then I saw the 
>tooltip...)*
>
>I reserved a simple click for future - I am planning to implement a feature 
>when a simple click on any symbol will highlight the smallest syntax 
>subtree the symbol is included into. I hope this feature will simplify 
>exploring long statements and also it should make it easier to copy 
>subexpressions.

I like that featurevidea, but I think "normal left click" to edit the box, vs.  
Although left click to do a special selection, would be much more intuitive.

In particular, if you never discovered the special selection option bur can 
edit, you can get things done. The reverse isn't true.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3E0625AB-2D26-4ED1-8124-EFB021136040%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

> On Jan 10, 2023, at 4:06 PM, Igor Ieskov  wrote:
> 
> >>> I suggest adding tooltips to every icon
> 
> It is already implemented. The software I used to record the video didn’t 
> capture tooltips. But they are present on all icons and other ui elements 
> (like texts and text fields to show what hot keys may be used). If it is not 
> working in your browser, could you please write what browser you use and its 
> version?

I see, it *does* work, but I had to wait longer than expected before they 
appeared. Perhaps I'm just too impatient :-).

> >>> mmj2 does have mechanisms to prove specific patterns, but those are 
> >>> written in JavaScript and might be easily to copy over to a tool already 
> >>> written in JavaScript.
> 
> My tool is actually written in ReScript (which gets compiled to JavaScript). 
> But anyway I don’t think I could easily copy-paste the code even if the tool 
> was written in JavaScript, because most probably we use different data 
> structures and different algorithms. However, the idea of mechanisms to prove 
> specific patterns is interesting to me. I had an idea to add numerous tactics 
> to automate common proof steps, but I need to gain more experience in 
> creating proofs to understand what common patterns exist. And if there are 
> already some mechanisms, I would like to take a look. Could you send a link 
> to the code in mmj2 sources, or documentation, or just write what is the core 
> idea (whatever is easier)?

The main mmj2 repo is:
https://github.com/digama0/mmj2

mmj2's algorithms aren't sophisticated. Here's a key file for its automation 
capability:
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js


> >>> mmj2's ability to check definitions is awesome, but probably not critical 
> >>> for a proof assistant.
> 
> I’ll remember that there is such area like definitions check and will return 
> to it when I am done with the most important features. However, if you have 
> on hand some links with description of what this is, then could you please 
> send it as well, I will take a look.

The definitions check algorithm is probably best understood by viewing the
"conventions" page section "Additional rules for definitions". Go here:
  https://us.metamath.org/mpeuni/conventions.html
The metamath language itself doesn't distinguish between axioms and 
definitions, but
in practice we *do* maintain such a distinction as explained there.
The mmj2 code for the definition check is here:
  https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/definitionCheck.js

By the way, there's a trick you could use in your JavaScript proof assistant:
encode the current proof-in-development in the hashcode ('"#" and text after 
the URL).
Every time there's an edit, update the hashcode. That will give you undo/redo
for free, make it trivial to save/load proofs, and it would also make it trivial
for people to share proofs with others (just share a URL).
I recommend you not store the entire program state (the .mm files would be 
enormous),
though the names of the databases might be helpful. See:
https://www.scottantipa.com/store-app-state-in-urls
https://news.ycombinator.com/item?id=34312546
I'm sure there are pros and cons, but I thought I should mention it.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/A6951314-469D-42E2-9536-D457207C456F%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

> On Jan 5, 2023, at 7:07 PM, Igor Ieskov  wrote:
> 
> "it might be good to provide a README.md (and a repository with a sensible 
> name)"
> 
> I moved the code to a new repository and provided a README file with 
> instructions. Please let me know if there are any issues with running the 
> project locally.
> 
> The new repo - https://github.com/expln/metamath-proof-assistant

Excellent!

I've added an entry that links to your new tool from our list of "other tools" 
for Metamath. The change is here:
- 
https://github.com/metamath/metamath-website-seed/commit/7225664b017c800033511abdcff22f390005da34
I linked to the redirecting web page, the repo, and the video.

We regenerate the website daily, so that will be visible tomorrow at this 
location:
https://us.metamath.org/other.html#mmtools

I have a few quick comments about your tool:
* I suggest adding tooltips to every icon, at least with a short name. Then 
people can hover over an icon & learn what it does. I would never guess that 
then 5-points-star is "unify" :-).
* Currently it uses "class1" etc. as a working variable, but these are easily 
confused with specific names. I suggest using mmj2's convention that  is a 
working variable. Those are easier to distinguish, and it'd look more like mmj2 
as well.
* Once proving in the bottom-up direction is added, for many this will begin to 
be be comparable to mmj2's functionality, while being a LOT easier to install. 
mmj2 has a number of specialized tricks, but I don't know if they're as 
commonly used.
  - mmj2 does have mechanisms to prove specific patterns, but those are written 
in JavaScript and might be easily to copy over to a tool already written in 
JavaScript.
  - mmj2's ability to check definitions is awesome, but probably not critical 
for a proof assistant.

I hope you'll be willing to continue work on it, it looks promising.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/0F0468AD-B017-4E6D-AC72-8ED81DC99A88%40dwheeler.com.

[Metamath] FYI: Google Lens works really well with Schwabhauser

[David A. Wheeler]

FYI:

Wolfram Schwabhauser wrote an amazing rigorous book on geometry
that is the basis of much of the geometry work in set.mm.
However, as suggested by its title "Metamathematische Methoden
in der Geometrie", it's in German, and many of us
(including me!) don't speak German.

I've recently discovered that the Google Lens mobile application is
an *amazingly* good solution to being able to read the book.
Point the camera at a page, and it shows the translation superimposed on the 
text.
It's awesome when you want to see the original images and just the
translated text superimposed. I'm sure there are problems, but I recently
had a question about page 109 and some of its preceding pages, and
Google Lens made the text far easier to use.

I thought others might want to know!

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C816E396-FEC1-4B01-9131-B7C036D37ACA%40dwheeler.com.

Re: [Metamath] Web-based mmj2-like proof assistant

[David A. Wheeler]

> On Jan 3, 2023, at 4:51 PM, Igor Ieskov  wrote:
> 
> Hi all,
> 
> I am developing a web-based proof assistant and would like to share current 
> results. The proof assistant is written in ReScript programming language and 
> React UI library. It runs completely in the browser. It uses the same 
> approach for building proofs as mmj2 (but at the moment it doesn’t have all 
> the features mmj2 has). I recorded a video (without verbal explanations) 
> similar to one of the mmj2 tutorial videos in order to demonstrate its 
> features. Any feedback is appreciated.
> 
> 
> 
> The demo video (if it is not opening, try to download; and sorry for low 
> quality of the video):
> 
> https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view?usp=share_link
>  
> 
> 
> The proof assistant:
> 
> https://igorocky.github.io/mm-proof-assistant/demo/v1/index.html
> 
> 
> The source code is stored in two repositories. And there is mess with it. I 
> started writing it inside of another project, put some logic into a second 
> repo. Because of that it is not easy to run it locally. But I am going to 
> improve this soon.
> 
> 
> The source code:
> 
> https://github.com/Igorocky/learn-js-react-app/tree/master/src/metamath 
> 
> https://github.com/Igorocky/js-common-functions/tree/master/src/main

That's awesome!

I notice that you don't have a license included - please add one!
If you're going to release as open source software, then you need an OSS 
license.
MIT is especially common:
https://github.com/IQAndreas/markdown-licenses/blob/master/mit.md
The Apache-2.0 and GPL-2.0+ licenses are also widely used.

A way to "get started" with proofs without any installation steps at all has 
its appeal!

Sadly, the mmj2 tool has become harder to install and maintain.
One problem: it's in Java, but it calls out to JavaScript code, and the
mechanism it uses for calling JavaScript has been dropped from more-recent 
versions of Java.
Specifically, mmj2 uses Nashorn. My understanding is that Nashorn's intended 
replacement is GraalVM.
I don't think this is *unsurmountable*.
Mario looked into this briefly & expected that it wouldn't be hard to switch to 
GraalVM
<https://github.com/digama0/mmj2/issues/7#issuecomment-428404641>,
but no one has (as of yet) picked up this work.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/6D20B2AC-F550-4598-A5E9-6E0985549BD0%40dwheeler.com.

Re: [Metamath] Should eliminate the GIF directories & just use Unicode?

[David A. Wheeler]

> On Jan 2, 2023, at 11:26 PM, Mario Carneiro  wrote:
> 
> I don't think the redirect would be that difficult, it is a one time apache 
> configuration thing, possibly plus updates to the mirrors.

Correct. On the main website we actually use the nginx web server, not the 
Apache web server,
but the basic principle is the same. We would just need to edit this file on 
GitHub:
https://raw.githubusercontent.com/metamath/metamath-website-scripts/main/us.metamath.org

A quick intro to nginx rewrite rules is here: 
<https://www.nginx.com/blog/creating-nginx-rewrite-rules/>
So we'd add a line like this:
   rewrite ^/(...)gif/$ /$1uni last;

Then on the main website we'd log in and run "git pull; ./build-system.sh" to 
do the update.

The mirrors would have to do their own config changes, we don't really control 
that. Hopefully it wouldn't matter much.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/B09D37E8-03F0-4C60-841B-9A791D16C171%40dwheeler.com.

Re: [Metamath] Should eliminate the GIF directories & just use Unicode?

[David A. Wheeler]

> On Jan 2, 2023, at 2:47 PM, Glauco  wrote:
> 
> The gif version has a useful feature: when you hover on a symbol, the ascii 
> string for the symbol is shown.
> 
> Would it be possible to have the same behavior in the Unicode version?

Yes. Any HTML element can have a "global attribute", and one of them is "title":
https://www.w3.org/TR/2016/REC-html51-20161101/dom.html#the-title-attribute

If we create a span and use a "title" element we could do the same thing.

I tried out both Firefox and Chrome (on MacOS) and after having for just a 
moment I saw the tooltip.
My demo HTML is below, in case anyone else wants to try the experiment.

--- David A. Wheeler

===





This is a tooltip demo for althtmldef "->" as "  ";



A  B.




-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/FF0A4BFB-8BAC-4482-83ED-E409B453552F%40dwheeler.com.

[Metamath] Should eliminate the GIF directories & just use Unicode?

[David A. Wheeler]

Should eliminate the GIF directories & just use Unicode? That is, for example,
redirect all uses of <https://us.metamath.org/mpegif/> to
<https://us.metamath.org/mpeuni/> ?

I welcome comments/thoughts. A few notes are below.

--- David A. Wheeler

===

The Metamath project has, for many years, generated HTML pages with embedded 
GIF images.
For a very long time this was the only practical way for most people to read 
the results.
However, today practically all web browsing systems support Unicode.
We switched to Unicode as the default years ago. Many
people's fonts didn't cover math symbols, but when we posted web fonts (my 
fault :-) )
that problem was basically solved.

At this point I think the primary reason to keep GIF directories is to make 
copying text easier:
https://us.metamath.org/mpeuni/mmset.html#textonly
That's a perfectly valid use case, as long as people are actually doing it.
I don't know how many people find that useful.

Generating everything twice takes time, but that's not a big deal.
It does create more opportunities for error & complicates our scripts.
The big advantage of eliminating the GIF generation would be to save disk space.
Because we generate everything twice, we use about double the disk space.
Anyone can see our current disk space status by viewing this page:
https://us.metamath.org/status.txt
The main drive /dev/sda has 26G, with 1.3G available (95% used).
We can pay for more space, but there's a jump in price.
We should be fine for a long time as long as we keep log files limited in size,
but any error in its configuration can cause problems (as illustrated recently).

There may be other issues I'm not aware of.

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CBC0AA4D-F5ED-406C-A8B4-6E871072E1AA%40dwheeler.com.

Re: [Metamath] Yamma

[David A. Wheeler]

Weird, I never had a problem with LOC_AFTER in mmj2.

A quick workaround in another prover is, if you're trying to prove something,
don't reuse its proof in the database - instead stop reading at that point.
After all, if you're trying to prove "foo", then reusing "foo" seems 
counterproductive :-).

--- David A. Wheeler


> On Dec 23, 2022, at 6:55 PM, Glauco  wrote:
> 
> 
> 
> I've got it working, thanks :-)
> 
> This is cool! (I've never even tried it myself, to clone the repository in a 
> new folder)
> Unfortunately, I still feel I'm a newbie about the npm / package.json / 
> tsconfig.json / launch.json architecture, so your support is really welcome.
> Please, let me know if / how I could rewrite the installation instructions so 
> that a TS developer would be able to "compile" the "project" :-)
>  
> The biggest obstacle to me following David's video in yamma is that the 
> LOC_AFTER feature of a .mmp file doesn't seem to be working yet.  So it keeps 
> trying to unify and prove reccot from reccot, which is cute and amusing but 
> not very practical.  I assume you would have fixed this by now if it was easy
> 
> I've never been able to make LOC_AFTER to work in mmj2 (but for years I've 
> been using a "custom" version, that Mel wrote / maintained for a limited 
> period of time; does LOC_AFTER work in your mmj2 installation?).
> I've simplified (I believe) the header structure of .mmp files:
> Yamma expects a
> $theorem 
> as a first statement (in the next few days, I plan to feat code to add this 
> line automatically when a ctrl+u is performed; it needs to match the .mmp 
> file name, otherwise a diagnostic / quickFix is displayed)
> Now, it is used to check that your theorem is consistent with the database 
> version (if you are refactoring an already existing theorem).
> And it will be used to check that the eHyps labels are coherent (.xxx 
> format), otherwise a warning / quickFix is risen (the quickFix can be to 
> either change the label or to add a statement $allowanyhyplabel , that 
> suppresses this kind of warning, for this .mmp file)
> 
> Since there's interest, I will add a new statement
> $locateafter 
> (it shouldn't be hard to implement; but it has to be handled both in 
> StepDerivation, in Search statements, and in StepSuggestions)
> 
> If you've not tried a Search yet, you can simply invoke it with ctrl + h 
> (same as in mmj2); yamma will analyze the statement under the cursor and 
> populate the search with the most "relevant" symbols (the 3 least frequent 
> ones, if I remember correctly). The "Search Comment:" part is not 
> implemented, yet. And a semantic tokenization for the keywords, is 
> deserved... (near to the top of my current TODO list)
>  
> Generating a .mmp file from a .mm file is another possible task for me once I 
> am properly armed with a parser.
> 
> Absolutely (the same as ctrl+g in mmj2). Thierry already had this feature 
> with its rust language server, metamath-vspa
> https://github.com/tirix/metamath-vspa
> (Thierry has written a number of impressive theorems and tools!)
> This feature is really important, I use it a lot with mmj2, both to refactor 
> proofs for existing theorems, and to write proofs for new, but "similar", 
> theorems.
> But I was planning to leave this feature for the second release of yamma (I'm 
> still working on the first one...)
> The other "popular" feature that I was planning to leave for the second 
> release, is "renumbering" ( alt + u + r in mmj2)
> I understand one expects these features to be there, but I cannot keep adding 
> stuff, otherwise I will never be able to publish something for metamathicians 
> to play with (and give some feedback)
>  
> Finally, one smaller matter, I notice your unifier puts long terms on a 
> single line (unlike mmj2)
> 
> If I'm not mistaken, mmj2 has two/three modes
> 1. all statements in single line
> 2. all statements in multiple lines (with standard formatting)
> 3. "some" statements in multiple lines (with standard formatting)
> 
> You can toggle between 1. and 2. using ctrl + o
> I'm always in mode 1. (single line) and then, selectively, reformat the 
> single statement I'm focusing on (with right click > "Reformat Step: Swap 
> Alt" ; sometimes, you have to do it twice, to actually work)
> 
> Of course, the plan is to port these 3 modes to yamma, too (only mode 1. is 
> available, now)
> 
> But now I see what you mean: if you break a statement on multiple lines "by 
> hand", mmj2 keeps your formatting, after a unification. In mmj2 I'm 
> constantly typing ctrl + r to get the "standard" formatting,

Re: [Metamath] Having trouble understanding (sqrt2irr)

[David A. Wheeler]

> On Nov 22, 2022, at 5:48 PM, Mario Carneiro  wrote:
> 
> I don't think the book needs to stay rigidly in sync at all. It's only had 
> two editions in how many years? In any case, while it is undoubtedly more 
> work to have to manage parallel PRs, it is definitely more scalable than 
> assuming that everything lives in the same repo. If set.mm is to be a 
> monorepo it should probably be renamed to reflect that.

I don't mean the "Metamath book" - that's already in a separate repo, and I 
think that's sensible. I don't propose changing that.

I'm thinking about a *different* book that is essentially a gentle 
introduction/walkthrough of set.mm as it currently exists, and is updated 
simultaneously as set.mm is updated. Think of it as set.mm documentation for 
those new to formal mathematics.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/1ECB3EDD-4C56-44E0-B6E2-23771ED8D63B%40dwheeler.com.

Re: [Metamath] Having trouble understanding (sqrt2irr)

[David A. Wheeler]

> On Nov 22, 2022, at 3:59 PM, Mario Carneiro  wrote:
> 
> I think we should not put everything in set.mm repo, or if we do, we clearly 
> separate set.mm from the rest of it. I think there is already too much stuff 
> in the repo that isn't about set.mm itself. What you have described clearly 
> sounds like a separate project, like a blog post series or something, and as 
> such it wouldn't need to stay rigidly in sync and could just pin a version of 
> set.mm to work with.

I agree with your general point of "don't put everything in the set.mm repo".

However, I have in mind a book that syncs with set.mm, that is, the book is 
updated as set.mm changes, that is, it *DOES* stay rigidly in sync. The easiest 
way to simultaneously edit them is to put them in the same repo :-).

 David A. Wheeler


-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/067489BC-395A-4AC3-AB27-5D632D09B4DE%40dwheeler.com.

Re: [Metamath] Having trouble understanding (sqrt2irr)

[David A. Wheeler]

> I am trying to learn advanced math with assistance of Metamath.

Cool!

> I understand a lot of elementary theorems that are in the database. However, 
> I thought I would jump to (sqrt2irr -Irrationality of square root of 2), but 
> its proof isn't really making sense to me.

I've toyed with the idea of creating an "Introduction to Formalized Mathematics 
Using the Metamath Proof Explorer (MPE)".
It would highlight the key axioms, definitions, and proofs (with links), with 
an idea of creating a simple
introduction to the idea & how it's done in MPE.  It might be gentler "way to 
start"
instead of reading MPE directly. It could be done in a different repository, but
if it was in the same repository it'd be easier to keep consistent.

I'd be curious if anyone else thought it'd be a good idea.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/46339806-74AD-42C1-B8C3-787454AB0708%40dwheeler.com.

Re: [Metamath] Buiding on metamath-knife

[David A. Wheeler]

> On Nov 11, 2022, at 2:38 PM, Zheng Fan  wrote:
> 
> These days I am looking at the code of metamth-knife, hoping to do some more 
> data processing based on the existing functions. But as a newbie in rust, I 
> found the code a little bit hard to grasp, mainly because the database is 
> stored in a fancy data structure (to improve performance, as far as I can 
> see), and it is not immediate clear how to process it further. Is there 
> somewhere I can find a detailed description of the data structure being used? 
> Thanks in advance.

Sadly, no.

Pull requests to fix that would be welcome. I think it might be best to put 
them in the code itself
(to increase the likelihood that the code would be updated when the data 
structures are modified).

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2CF94F5C-2D99-4793-956B-E54C487D8C81%40dwheeler.com.

Re: [Metamath] My contribution to Metamath's mmsolitaire project

[David A. Wheeler]

> On Oct 11, 2022, at 8:16 AM, 'Dragorion' via Metamath 
>  wrote:
> 
> > PPS: Is there a way I can add a non-Google mail address to this mailing 
> > list?
> I tried to send an email to metamath+subscribe at googlegroups dot com, but 
> got a response "Your request to join metamath failed because you are already 
> a member." which is not true (at least I receive nothing from this mailing 
> list at that address and cannot find it in the list of members).
> Maybe some people have permission to invite arbitrary addresses into the list?

I checked the Google Groups settings. You're already listed as a member who 
receives each email as:
Samiro Discher
samirodischer AT googlemail.com
(Replace "AT" with "@").
... so you SHOULD be receiving the emails, presuming you can read that account.
Have you checked your Junk folder?

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CCE41937-2E62-44A3-B3DD-526C73527CC7%40dwheeler.com.

Re: [Metamath] My contribution to Metamath's mmsolitaire project

[David A. Wheeler]

> On Oct 9, 2022, at 3:05 PM, 'Samiro Discher' via Metamath 
>  wrote:
> I hope this is somewhat readable, if something is still unclear, feel free to 
> ask. And let's hope at least David is still alive .. (´ ∀ ` *)

Me too :-).

Mario can certainly accept changes to it. Changes in the "seed" are rare, but I 
think we should use the same process: someone proposes it, someone else reviews 
& approves it, then it can be merged (accepted).

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/7A642A67-E123-4824-B5E4-6DA398978F54%40dwheeler.com.

Re: [Metamath] Metamath mirrors: Current state & proposed plan

[David A. Wheeler]

I've started implementing mirroring here:
https://github.com/metamath/metamath-website-scripts/pull/1
Click on the "Files Changed" tab for all the details.

I'll need *real* public keys from the mirror maintainers for this to be useful.
For the moment I've stubbed that out.
It's possible this won't work at first, even with real public keys,
but if so we'll work out the bugs until it does. I don't expect any serious 
problems.

I still haven't heard from:
- at.metamath.org - Austria [courtesy of Digital Solutions Marco Kriegner]  
- de.metamath.org - Germany.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/89504F86-1D12-48B9-A559-7783EF99F51E%40dwheeler.com.

Re: [Metamath] Metamath mirrors: Current state & proposed plan

[David A. Wheeler]

> On Sep 14, 2022, at 8:55 PM, heiphohmia via Metamath 
>  wrote:
> It mostly boils down to an experiential difference---"live" updated page vs
> "static" site with periodic updates. I'm clearly biased to thinking the former
> is way cooler.

That doesn't seem important to me. After all,
we don't create new theorems THAT quickly :-).
Rsync is *remarkably* efficient in the "no change" case. Mirrors could poll 
hourly
(or even more often) with no problem.


>> We really *can't* handle such errors. If the other side is inaccessible, or
>> can't write an update, there's little we can do about it.
> 
> SMTP might like to have a word about that :D
> Transient network errors have to be handled or ignored by *someone*, be that
> us.metamath.org or the mirrors.

Sure, but the mirror admin will have to fix the problem. If there's a network 
problem
that doesn't affect us.metamath.org but DOES affect the mirror, the mirror will 
be in a
better position to do something about it. A more likely problem is 
out-of-storage at the mirror site;
again, we can't solve that, only the mirror can.


> Anyway, security-wise, the pull model implicitly delegates trust out to each 
> of
> the mirrors. If any of them are compromised, then up to any (not unheard of)
> rrsync bug, us.metamath.org is hosed.

No, we have other lines of defenses even in that case:
(1) The login shell is still disabled, making "use login shell" tricks not work
(2) Even if rrsync sandbox is escaped and the account is fully taken over,
the attacker only gets a separate user account created for that mirror with no
special privileges. It's *not* a privileged account. The mirror account
can't modify the files being served by the webserver (owned by user 
"generator"),
and it can't see private keys (owned by user "root").
The attacker would have to use yet another vulnerability (e.g., a kernel 
exploit) to get real privileges.
To make that harder, I've hardened the system & the system auto-installs 
security updates.

That's on top of the other defenses to *get* to that point:
a) The mirror system has to be taken over and/or have its private key 
exfiltrated
b) ssh and/or rrsync are subverted. But both are relatively small, widely used, 
and
   specifically intended to be securely usable for these purposes.

Sure, an attacker *might* get through all that. Worse comes to worse, we trash 
the
virtual machine, create another, and re-run the script to recreate the site.

> Anyway, modulo other constraints, in my "make everything stateless containers"
> world, the default tends to be to avoid polling as much as possible, so adjust
> priors accordingly.

I don't have any allergy to polling, and a web server necessarily has state
(that's what we're serving!).

I think the key is that we can always revisit this stuff later.
My goal is to "make it work reasonably well" for now, so that everything is 
automated.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/F2ED7D9C-0D8B-49E5-9138-0936C446B866%40dwheeler.com.

Re: [Metamath] Metamath mirrors: Current state & proposed plan

[David A. Wheeler]

> On Sep 14, 2022, at 2:46 PM, Cris Perdue  wrote:
> 
> Hi David,
> 
> Your plan looks quite good to me, especially given that you prefer to only 
> permit authorized mirroring, not just anyone who chooses to set up a mirror.
> 
> My one small suggestion would be to check that mirror servers can run rsync 
> like this:
> 
> $ rsync -e ssh -a mirror...@us.metamath.org: /var/www/cn.metamath.org/
> 
>  -- in other words, omitting the path to the source area to be mirrored.

That's a new syntax for me, but sure, we can try it.

> https://dev-notes.eu/2015/06/secure-rsync-between-servers/ indicates that 
> this should work (OK, they add a trailing "/"),

Interesting. I note that they do the same thing - the mirrors initiate the 
rsyncs (not the other way around).

> and you really don't want the mirrors to even be able to copy over other 
> parts of your source filesystem, so the
> full source path ought to be ignored if given.

I agree that mirrors shouldn't have access to everything on the server.
That said, leaking the name of the path is okay. The configuration is publicly 
visible after all.

The overall goal is to minimize privilege to make an attacker's job harder.
That also makes my life easier; if the system isn't 0wned, then I don't have to
spend my time fixing it :-). Determined & clever attackers can get into all 
sorts of
systems, but if we make it a pain, the attackers are likely to attack
a different system that's more valuable to them.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C105BC6E-5030-4176-8422-3193FE9AF233%40dwheeler.com.

Re: [Metamath] Metamath mirrors: Current state & proposed plan

[David A. Wheeler]

> On Sep 14, 2022, at 12:05 AM, heiphohmia via Metamath 
>  wrote:
> 
> Nice work modernizing and hardening the infra. These days what's considered 
> the
> "bare minimum" has a lot of moving pieces.

It really isn't bad. There are more pieces, but the tools to manage it are 
better,
and many things "just work". Trivial example: historically you had to take extra
steps to install rrsync, now it's just another program you install & manage 
with the
package manager.


> Anyway, please permit me to butt in with a small idea. The mirror setup you
> propose has each mirror polling the source server for changes. What about a
> push-centered architecture?
> 
> Since rsync is equally capable of pushing changes, I'm imagining a reversal of
> roles in your ssh setup and having some post-update hook that rsyncs the
> changes to each mirror.

Like everything, there are pros & cons :-).


> Off the top of my head, pros:
> 
> - Tighter sync between mirrors and us.metamath.org

I don't think that's critical. We update 1/day, and it's not a crisis if
the mirror update is delayed. Also, rsync is *really* fast at determining
"there is nothing to do".

> - Less network noise
> - Slight reduction in attack surface area on us.metamath.org
> 
> cons:
> 
> - Error handling becomes responsibility of the post-update hook

We really *can't* handle such errors. If the other side is inaccessible, or
can't write an update, there's little we can do about it.

> - Might require updates to Firewall settings

Not really, and we control our firewall settings anyway.

There's a bigger "con": the mirrors would need to allow
someone from the outside (specifically us.metamath.org) to log in
*to* their system & write to it. I don't know if they're willing to do that.
They may not even have the rights necessary to do it.
That's not a technical issue, but it certainly might matter :-).

Another con: It'd mean that the us.metamath.org site would have to
store the private keys for logging in to those other sites.
Doable, but an extra step.

Mirror folks: Comments?

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/09EA8375-D8B7-4684-823F-7E6DF62B912E%40dwheeler.com.

[Metamath] Metamath mirrors: Current state & proposed plan

[David A. Wheeler]

We currently have a few mirrors of the Metamath website (e.g., 
cn.metamath.org). Their purpose
is to provide access Metamath information even if the "main" site 
us.metamath.org is down.

If you manage a Metamath mirror, please contact me! If you have an opinion 
about handling mirrors,
please let me know (or post here for discussion).

The main question is: Do we want to continue to support Metamath mirrors at all?
Mirrors made more sense when websites were less reliable and CDNs didn't exist.
If we stop supporting mirrors, that's one less complication.
The mirror in the Chinese mainland has the strongest case to continue, due to 
the
Great Firewall of China.

If we *do* want to support mirrors, we need to change things, as mirrors no 
longer work.
Historically these copied data from "rsync.metamath.org", which was really
Norm's "us2.metamath.org" site in his house. Unfortunately, us2.metamath.org
has stopped working & it's not clear if we can get it working again.
(We managed to get off us2.metamath.org just in time!!).
In addition, the old system used an unsecured rsync connection, so we need to 
change it anyway.
I want to lock it down to make it unlikely to be a serious vulnerability.

If we *stop* supporting mirrors that'd be one less complication & effort. But 
if we
want to continue supporting mirrors, then we need to make them actually work 
:-).

Below is the current state & my proposed plan *if* we want to continue to have 
mirrors.

--- David A. Wheeler

=

First, the current state. The *working* metamath mirror sites are
(not counting us.metamath.org and us2.metamath.org):
 - at.metamath.org   Secondary mirror (Austria) [courtesy of Digital Solutions 
Marco Kriegner]  
 - cn.metamath.org   Secondary mirror (China) [courtesy of caiyunapp.com]
 - de.metamath.org

They use rsync to synchronize their data. Rsync is a great protocol when 
combined
with ssh, but using it *without* ssh over the public internet is a terrible 
idea.

If we continue to support mirrors, I propose configuring a special account for
synchronization. Mirrors would each log in using ssh and their specific private 
SSH key.
They'd log into a restricted account specific to that mirror
via ssh in a way that provides read-only access to only the
mirrored public files (the program "rrsync" can restrict what access is allowed 
to rsync).

Here are my proposed configuration:

* Every mirror would create a public/private keypair & send the public key to 
me.
* For each mirror we'd create a new account on us.metamath.org (e.g., 
"mirror.cn")
* That account's /home/mirror.cn/.ssh/authorized_key would be modified to this:
  command="/usr/bin/rrsync -ro /var/www/us.metamath.org/",restrict ssh-rsa 
{PUBLIC_KEY}
  .. .this forces ssh logins to run the restricted rsync to read-only mode for 
JUST the mirror directory,
  restricts (eliminates) all other ssh access, and uses ssh-rsa for login.
  We could use a different key pair algorithm. Note that the PUBLIC_KEY will be 
public,
  but that's fine!!
* Ensure nothing in its .ssh dir can be easily changed: chmod -R a-w 
/home/mirror.cn/.ssh
* Disable any other kind of login with: chsh mirror.cn -s /bin/nologin
* Note: The "rsync" daemon will *not* be enabled; the only way to access this 
is to
  log in via ssh. It's not wise to run a bare rsync nowadays.
* The mirrors would periodically run an "rsync -e ssh -a 
mirror...@us.metamath.org:/var/www/us.metamath.org/ /var/www/cn.metamath.org/".
  Rsync is clever about updates, so this would typically be extremely fast 
unless the internet link is bad.

This would make mirrors log in - mirrors can make us do "extra work" so we 
don't want just anyone
to be able to mirror. However, these steps will mean that the only thing the 
mirrors can do is make us
do extra work to serve public info... making the accounts not-very-interesting.

I haven't actually tried to *implement* this configuration, so there may need 
to be some tweaks & changes,
but that's the general idea.

Some info sources:
* 
https://serverfault.com/questions/965053/restricting-a-ssh-key-to-only-allow-rsync-file-transfer
* https://www.whatsdoom.com/posts/2017/11/07/restricting-rsync-access-with-ssh/
* http://gergap.de/restrict-ssh-to-rsync.html

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/94157C87-67F2-492F-B6B6-A98BEDE5D45C%40dwheeler.com.

Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org

[David A. Wheeler]

> On Sep 8, 2022, at 4:57 PM, Benoit  wrote:
> 
> Now that "us" is favored over "us2" and that there is no longer the notion 
> that "us2" is fresher than "us", we should also "decouple" both sites by 
> removing some hyperlinks between them (e.g., us.metamath.org currently has a 
> link to "http://us2.metamath.org:88/mpeuni/mmrecent.html; for "Recent proofs" 
> near the top of the page, and a few other instances).

Agreed. I've hesitated because I wanted to make sure that the site kept working 
day-by-day.

Has anyone had any problems with us.metamath.org?

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/E9C15FF9-F9BD-4AE7-B59A-4A372710E034%40dwheeler.com.

Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org

[David A. Wheeler]

Note: I'm automatically notified via email
if us.metamath.org ever goes down for more than 5 minutes.
That said, I might miss the alert, or perhaps the monitoring system might fail 
to
notify me, so if it's down for a while it's fine to let me know.

Hopefully us.metamath.org going down will be a rare occurrence:
* The us.metamath.org site is hosted by
  Linode, who generally have a good reputation, so the virtual machine should
  generally keep running.
* The web server (nginx) is generally pretty reliable, and
  is auto-restarted if it crashes.
* The system automatically installs security updates,
  which will hopefully update the system faster than attackers exploit known 
vulnerabilities.
* I've taken some hardening steps to make the system harder to take down.
* We're simply serving static HTML pages and many server functions are
  intentionally disabled, which hardens it further.

Nothing is unbreakable, but I'm trying to increase the likelihood that
the system will just keep running.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/C8DA8C7B-201F-4087-ABA4-9BAACC53F346%40dwheeler.com.

Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org

[David A. Wheeler]

> On Sep 6, 2022, at 12:51 AM, 'Alexander van der Vekens' via Metamath 
>  wrote:
> 
> Currently, us2.metamath.org is not reachable anymore - is this intended?

I recommend normally using us.metamath.org (main site), not us2.metamath.org 
(Norm's old computer).

As far as I can tell, us.metamath.org is working normally. If it *ever* goes 
down for
a nontrivial amount of time, let me know.

Unfortunately mirrors are currently running off rsync.metamath.org, and that's 
really us2.metamath.org
instead of us.metamath.org. I intend to eventually move rsync to refer to 
us.metamath.org, but
we're having trouble with a DNS transfer and that is temporarily halting things.

I'll ask Susan's partner to reboot Norm's old computer, that may help.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2FDD4D1D-A8E4-40EB-877E-5805D35CB4E8%40dwheeler.com.

Re: [Metamath] checkmm ported to TypeScript

[David A. Wheeler]

> On Aug 31, 2022, at 5:01 AM, Antony Bartlett  wrote:
> 
> On Monday, August 29, 2022 at 9:07:53 PM UTC+2 David A. Wheeler wrote:
> Let me know of any objections to adding it to our test suite. 
>  
> Well I'd love to see this, but of course I'm biased ;-). I don't think it 
> adds much value because it's a port, and any errors in the original program 
> are likely to have been faithfully reproduced.
> 
> Is it possible to get run time statistics from the test suite? - i.e. see how 
> long each validator is taking to run in the CI environment.  That's 
> definitely something I'd like to see, as at the moment you only have my word 
> for it that checkmm-ts is fast (but nowhere near metamath-knife's league).

Take a look at any pull request, and click on the checks.
For example, if you go here:
  https://github.com/metamath/set.mm/pull/2803
Click on any of the green checkmarks, which will show you the list of checks.
You can then see their times.

That only shows the times for that case; if you were serious you'd take a 
sample.
But we aren't in *that* much of a rush that running some tests hampers anything.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/AF4C1042-9517-4BD6-A8F5-C129441B5340%40dwheeler.com.

[Metamath] Main metamath website generates its own web pages - needs a little slimming

[David A. Wheeler]

Progress! We're one step closer to not using us2.metamath.org.

The main metamath website, "metamath.org / us.metamath.org",
now *generates* its own web pages as well as serving them. So it
*no longer* pulls files from Norm's computer us2.metamath.org.

Please let me/us know of any problems you find.
This *should* be a silent change, that is, there shouldn't be anything to 
notice.
But of course, I'm doing things in stages in case there *is* a problem.
Eventually we'll want the mirrors to stop using us2.metamath.org too,
but that's a different step.

Currently I've set website regeneration to occur daily at 4am UTC.
That time is arbitrary and can be changed.

The site is currently at 98% disk use, which is WAY too much & begging
for problems. I'd like to fix that quickly.
There are a few mega-large files we create in "downloads/",
and I don't think we need ALL of them:
276136805 Aug 30 09:52 metamathsite.zip
273985535 Aug 30 09:51 metamathsite.tar.gz
269798481 Aug 30 09:51 metamathsite.tar.bz2
268443892 Aug 30 09:47 mpeuni.zip
206535792 Aug 30 09:45 mpeuni.tar.gz
98907939 Aug 30 09:43 mpeuni.tar.bz2

Can we drop the '.tar.gz' files in these cases?
I think the .tar.bz2 and .zip formats should be plenty.

Also, we might also want to remove some metamath.exe
stuff & point people to GitHub, e.g., removing:
downloads/metamath.zip
downloads/metamath.tar.gz
downloads/metamath.tar.bz2

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/183B1ADB-F5FB-4D0A-96F3-AE520BDAA753%40dwheeler.com.

Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org

[David A. Wheeler]

> On Aug 30, 2022, at 11:22 AM, Benoit  wrote:
> 
> Thanks David.  To clarify: I'm not pushing towards faster or more frequent 
> updates.  Even if it's only every other day or less, I'd be fine.  What's 
> important is that this information is known (maybe we could indicate it on 
> mmrecent.html or somewhere else).

Good point. We can put it somewhere on the website (once we know what it is :-) 
).

>   So, if I understand, a refresh cannot be triggered by a merge on github: 
> the website script has to download the databases periodically in order to 
> check whether they were modified ?

Correct. There are many things that influence the results of generation, in 
particular, updating a database OR updating the metamath.exe tool OR the 
underlying seed website OR the scripts used to create the website.

It takes long enough to regenerate that it's better to generate periodically, 
and NOT regenerate on each change.

> (And then, I guess the regeneration happens only if a change is noticed in 
> the associated database ?).

Actually, no, it currently just regenerates every day.

I hope to add that optimization later. If someone else wants to do it, GREAT! 
It would save a few pennies. However, currently my goal is make it work *NOW*. 
We can optimize later. It's not *hard* really, but to truly ensure that 
generation occurs when something HAS changed, you need to ensure you capture 
all the possible cases. It's easier to just "always regenerate periodically".

Context: originally these were jury-rigged scripts that Norm only ran every 
once in a while. For many years  changes occurred only infrequently, so that 
was fine. But the Metamath community has greatly grown since then, and I do 
*not* want to have to have anyone figure out "when to update the website". 
Periodic updates of whatever has been approved means one less 
discussion/decision we need to make. If it's been accepted, then let's show it. 
If we make a change/improvement later, then let's show that too.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/012EFD1C-2A34-4E4E-973F-52D408ECC42D%40dwheeler.com.

Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org

[David A. Wheeler]

On Aug 30, 2022, at 11:02 AM, David A. Wheeler  wrote:
> 
> We can choose *when* it runs. I'm expecting to run it daily, as that is 
> easily understood. We could to it 2/day (that would double the CPU costs), or 
> only some days (but I think daily is easier to understand).

Quick clarification: I intend to set a specific time for the website 
regeneration to start every day. Say, 2am Eastern Time. The regeneration would 
download the current versions of the databases, run to completion, and then 
update the website all at once. So the website update would currently occur 
about 6.5 hours after the regeneration begins.

--- David A. Wheeler

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/BBA5A704-9A7A-4724-ABA8-F7FB70F885C8%40dwheeler.com.