[Metamath] Re: Denoting morphisms in set.mm

Regarding: F : A -1-1-> > F : A >--> B F : A -onto-> > F : A -->> B F : A -1-1-onto-> > F : A >-->> B Do you have a textbook reference for the new symbols you propose? The current symbols we use are from Takeuti & Zaring. The are rendered

[Metamath] Re: Denoting morphisms in set.mm

FL asked me to post this. Forwarded Message Subject: Arrows Date: Fri, 17 Apr 2020 13:56:36 +0200 (CEST) From:FL Hi Norm, I Hope you are fine. Can you post that I like Benoît's arrows annotated with a subscript (Grp etc.) but that the semantics of arrows like >-> is

Re: [Metamath] Stacking symbols in html / unicode

On Monday, April 13, 2020 at 10:30:05 AM UTC-4, Benoit wrote: > > By the way, Norm: is upgrading to HTML 5 among your plans ? I can't > estimate how much work it would be (both for the pages generated by the > metamath program and for the other pages, which can be done > independently). I'm

Re: [Metamath] Stacking symbols in html / unicode

On Monday, April 13, 2020 at 9:32:36 AM UTC-4, andrebacci.listas wrote: > > On Mon, Apr 13, 2020 at 10:52 AM Benoit wrote: > >> Many symbols used in math are obtained by stacking symbols. For >> instance, an isomorphism is often denoted by an arrow with a tilde above it: >> >>

Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ?

consider that. (The algorithm scans backwards from the [author] tag until a keyword is found.) On Sunday, April 5, 2020 at 2:09:21 PM UTC-4, David A. Wheeler wrote: > > On Sun, 5 Apr 2020 08:10:56 -0700 (PDT), Norman Megill wrote: > > That's a good idea. Give me about a week to re

[Metamath] Fwd: AI and lemmas

Posted as requested. Forwarded Message Subject: AI and lemmas Resent-From: nm Date: Wed, 8 Apr 2020 20:39:33 +0200 (CEST) From:fl Reply-To: fl To: nm Hi Norm, could you post this? If we have the intent of minimizing a proof with the AI engine, is it better to keep it in

[Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ?

That's a good idea. Give me about a week to release a new version with this keyword. If you think of any others that would be useful let me know. Norm On Sunday, April 5, 2020 at 10:10:12 AM UTC-4, Glauco wrote: > > The command > > HELP WRITE BIBLIOGRAPHY > > doesn't list "claim" as a keyword

Re: [Metamath] Re: Deep Learning powered proof shortening

Posted per FL's request. - Norm Forwarded Message Subject: Stanislas' engine Resent-From: nm Date: Sat, 28 Mar 2020 14:53:18 +0100 (CET) From: fl To: Megill, Norman Hi Norm, Could you ask Stanislas how long dors it take to minimize a proof and would it be possible to launcher

[Metamath] Re: Why would proof shortening be useful?

People will probably have different answers, but from my own perspective: 1. Simple shortenings with 'minimize_with' almost always make the proof cleaner and more readable by eliminating redundant bicomd's etc. that happen when the proof is written "sloppily" to save time (as I tend to do). 2.

Re: [Metamath] Second-order theory

On Monday, March 16, 2020 at 1:06:17 PM UTC-4, Ken Kubota wrote: > > In terms of expressiveness, schemes are another way of expressing what > usually requires a higher order. > If you want to determine the order of a logic, it doesn't make sense to > allow schemes. > What can be expressed in

[Metamath] Re: e. in the context of fol or sol + Peano

I'm explorating the Peano axioms > in the context of first or second order logic. > > Peano uses a "e." symbol > to express phrases like "x e. NN", > "x is a number". There was no set theory > intent in his m'indiquer. So I'd like to reuse the > material in set.mm related to > e., class

[Metamath] e. in the context of fol or sol + Peano

fl requested that I post this. Norm Forwarded Message Subject: e. un the contexr of fol or sol + Peano Resent-From: nm Date: Sun, 15 Mar 2020 16:27:03 +0100 (CET) From: fl To: Megill, Norman Hi Norm, I'm explorating the Peano axioms in the context of first or second order

Re: [Metamath] Re: Analysis of full 'minimize' run on set.mm

All minimization runs are now incorporated into set.mm. The total size reduction of set.mm was 217484 bytes. set.mm now contains 2684 fewer lines. Notes: (1) The byte count above is for set.mm on Linux. On Windows, the reduction was 220168 bytes because of the extra byte in the CR/LF line

Re: [Metamath] Re: Deprecated sections of set.mm

On Wednesday, March 4, 2020 at 5:46:58 AM UTC-5, Jon P wrote: > > ... > > I think I might narrow my efforts down a bit just to doing theorem pairing > (finding the new theorem which is the equivalent to the old). This is a > task that needs to be done for all of parts 18, 19 and 20 and is >

Re: [Metamath] Re: Deprecated sections of set.mm

I agree with Alexander's comments, and if you want to create a PR for this (renaming the to-be-deleted theorems as *OLD) it is fine. It is preferable for the comment in *OLD to be e.g. "Obsolete version of ~ sgrpmgm as of 3-Mar-2020. " because when I look for expired theorems to delete, I

Re: [Metamath] Re: Deprecated sections of set.mm

While my style is not the same as everyone's, it is rare that I go into set.mm in a text editor without knowing more or less what I plan to do (add a new theorem to prove, edit a comment, etc.). I use the web pages to study proofs when I know the label but rarely search with e.g. google. I

Re: [Metamath] Re: Deprecated sections of set.mm

On Sunday, March 1, 2020 at 5:38:45 AM UTC-5, Jon P wrote: > > So I tried a little with trying to find candidates for deletion from the > deprecated sections by finding theorems which weren't referenced and then > finding new theorems to pair them up with. I managed to do 9 here >

[Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT?

On Tuesday, February 25, 2020 at 1:40:54 PM UTC-5, Alexander van der Vekens wrote: > > On Tuesday, February 25, 2020 at 7:00:48 PM UTC+1, Norman Megill wrote: >> >> Since there were no other replies, unfortunately I just updated set.mm >> with both discourageme

[Metamath] Re: Should we make both discouragement tags mandatory in *OLD and *ALT?

Since there were no other replies, unfortunately I just updated set.mm with both discouragements on every ALT because of the problems they were creating. I suppose I could revert and do the analysis all over, but I want to get the minimizations applied soon without unwanted side effects. How

[Metamath] Should we make both discouragement tags mandatory in *OLD and *ALT?

On 2/13/20 9:25 AM EST, Benoit wrote [in the "Full 'minimize' run on set.mm" thread]: > > Actually, most *OLD and *ALT should probably have both discouragement > tags as well, it seems ? > > Thanks, > Benoît *ALT theorems in the full job logs (not just the suspicious proof size decreases

Re: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening?

On Sunday, February 23, 2020 at 10:24:59 AM UTC-5, Ken Kubota wrote: ... > (Note that Metamath isn't really Hilbert-style, in my opinion, since it > can express metatheorems. It seems to start directly at a higher level, > like all logical frameworks. > A true Hilbert-style system consists

[Metamath] Re: Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.)

Please disregard this truncated message. Something screwy about Google. I'll repost soon. On Monday, February 24, 2020 at 2:07:51 PM UTC-5, Norman Megill wrote: > > On Monday, February 24, 2020 at 11:31:45 AM UTC-5, Ken Kubota wrote: >> >> My comment on Kevin Buzzard's inte

[Metamath] Re: Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.)

On Monday, February 24, 2020 at 11:31:45 AM UTC-5, Ken Kubota wrote: > > My comment on Kevin Buzzard's intervention: > https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ > (I don't know why Google doesn't let me respond to that post, so I'm responding here.) On Feb. 23 Ken Kubota

[Metamath] Re: Analysis of full 'minimize' run on set.mm

Thanks. I'll take care of adding the discouragement tags. I just wanted agreement that it is the correct thing to do. Norm On Saturday, February 22, 2020 at 8:30:30 PM UTC-5, Benoit wrote: > > I think that the *ALT and *OLD theorems appearing in the list (and those I > quoted earlier in this

[Metamath] Re: Analysis of full 'minimize' run on set.mm

ing "rexbidvALT". <- use rexbidv instead $ grep 'Proof of "ALT" decr' j*g job119.log:Proof of "ismgmALT" decreased from 199 to 151 bytes using "elab2g".<- Alexander: I assume this is ok to do? Norm On Thursday, February 20, 2020 at 10:28:24

Re: [Metamath] Analysis of full 'minimize' run on set.mm

Thanks. Looking at the end of the log file, it seems the job didn't complete. 99.7 hrs seems like an unusual number - could there have been a 100 hr timeout? Scanning forward through statements... Proof of "mideulem" decreased from 7532 to 7527 bytes using "ad2antrr". 359212.21user

[Metamath] Analysis of full 'minimize' run on set.mm

All jobs from 101 to 158 have completed. Many thanks to all who contributed CPU time! Jobs 159 and 160 are still running, but we will handle those manually later. Therefore we are ready to start the final analysis. I put all of the logs except 159 and 160 here:

Re: [Metamath] Full 'minimize' run on set.mm

All jobs are covered. There are 5 jobs left to finish (147, 155, 157, 159, 160). The first 4 are currently running on 4 cores on DAW's computer and the last on yours, so there is no need to run anything else at this point. My plan is to assemble what we have in a few days regardless of what's

Re: [Metamath] Full 'minimize' run on set.mm

jUQM6nBAAJ estimates: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ Norm On Tuesday, February 18, 2020 at 1:53:13 PM UTC-5, Mario Carneiro wrote: > > 158 is done (after 62.8 hours), starting 159. 160 is still running. > > On Sun, Feb 16, 2020 at 8:13 AM Norman Megill

Re: [Metamath] Breaking up ~ mideulem and ~ footex

I would suggest that you run the minimizations on your pieces (calling them say job160a, job160b, job160c for mideulem). Before my final minimize run I will use your logs from these 3 new jobs to extract the minimizations, after you do a PR for the break down. Since all other jobs are using a

Re: [Metamath] My latest minimize status

On Sunday, February 16, 2020 at 10:32:56 AM UTC-5, David A. Wheeler wrote: > > (Replying to myself) > > My job 145 just finished. It's posted as: > https://dwheeler.com/temp/job145.log > > I have a spare CPU available if it might be useful for another job. > heiphohmia's job115 died in the

Re: [Metamath] Full 'minimize' run on set.mm

Thanks. I updated the status: https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ with 158 assigned to you. On Saturday, February 15, 2020 at 10:41:17 PM UTC-5, Mario Carneiro wrote: > > 156 is done (after 31.8 hours), starting 158. 160 is still running. > -- You received this

Re: [Metamath] Full 'minimize' run on set.mm

On Saturday, February 15, 2020 at 9:35:05 PM UTC-5, David A. Wheeler wrote: ... > Jobs 157-159 are unassigned. If they're still unassigned, I could take one > (presumably 157) once 149 completes (presumably tomorrow AM). > Can I snag 157 as well? > OK, I'll assign 157 to you. Norm -- You

Re: [Metamath] Full 'minimize' run on set.mm

Thanks. I updated the status of your and Giovanni's runs. https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ Norm On Saturday, February 15, 2020 at 9:49:07 AM UTC-5, David A. Wheeler wrote: > > I have completed jobs 112 and 125-131. Their logs are posted in >

Re: [Metamath] Minimize using "dummylink" and "idi" in fourierdlem48?

The occasional temporary use of dummylink and idi during a 'minimize' run is normal, but they should always disappear from the proof by the end of the run. I just responded to this on the issue page, which breaks down step by step what is going on and shows how to debug this. Sorry for the

Re: [Metamath] Full 'minimize' run on set.mm

2 PM EST, Norman Megill wrote: > >On Friday, February 14, 2020 at 6:41:14 PM UTC-5, Norman Megill wrote: > >> > >> On Friday, February 14, 2020 at 6:28:58 PM UTC-5, David Starner > >wrote: > >>> > >>> On Fri, Feb 14, 2020 at 3:12 PM Nor

Re: [Metamath] Full 'minimize' run on set.mm

> > > Job 113 results attached. Runtime is about 18.2 hours. > Should I keep sending job results piecemeal like this, or would it make it > easier to just wait until my current batch is done and send them all at > once? > > I don't mind getting them one at a time since I can do some

Re: [Metamath] Full 'minimize' run on set.mm

On Friday, February 14, 2020 at 6:28:58 PM UTC-5, David Starner wrote: > > On Fri, Feb 14, 2020 at 3:12 PM Norman Megill wrote: > > A simple way to fix this is to add "(Proof modification is > discouraged.)" to dral1ALT, etc. as they should have anyway. Then th

Re: [Metamath] Full 'minimize' run on set.mm

On Friday, February 14, 2020 at 6:11:58 PM UTC-5, Norman Megill wrote: ... > > We have a more serious problem though. ~dral1ALT is not in job129.cmd, it > is in job124.cmd. When I checked, ~dral1ALT was in the old job129.cmd > before the bug fix. In my post > https://groups.g

Re: [Metamath] Full 'minimize' run on set.mm

On Friday, February 14, 2020 at 4:15:56 PM UTC-5, David A. Wheeler wrote: > > On Thu, 13 Feb 2020 06:25:42 -0800 (PST), Benoit wrote: > > Actually, most *OLD and *ALT should probably have both discouragement > tags > > as well, it seems ? > > I looked at the .log files I have so far. Once I

Re: [Metamath] Full 'minimize' run on set.mm

On Friday, February 14, 2020 at 12:45:53 PM UTC-5, Mario Carneiro wrote: > > 123 and 124 completed, in about 12 and 13 hours respectively. I'm running > 156 and 160 now. > Thanks. Rather than send a new email for every status update, I'm editing it directly here:

Re: [Metamath] Full 'minimize' run on set.mm

On Friday, February 14, 2020 at 8:01:47 AM UTC-5, Thierry Arnoux wrote: > > If ~ footex and ~ mideulem are too long, I may split them into smaller > lemmas, and then run minimize on the smaller lemmas. > That would be the preferred thing to do, because it means that we won't have the problem in

Re: [Metamath] Full 'minimize' run on set.mm

Here is the current status, Feb 14 7:25AM EST *101 Alexander (complete) *102 heiphohmia (complete) *103-111 David Starner (complete) 112 David A. Wheeler (in progress) 113-116 heiphohmia (in progress) 117-122 Giovanni (in progress) 123-124 Mario (in progress) 125-132 David A. Wheeler (in

Re: [Metamath] Full 'minimize' run on set.mm

I worked out an estimate (in hours) for jobs 133-160 based on the theory that the time to save a compressed proof is proportional to the run time of 'minimize'. Here's how it compares so far, assuming a CPU taking about 30 sec for the 3atlem4 minimization. I'll keep this updated as the logs

Re: [Metamath] Full 'minimize' run on set.mm

On Thursday, February 13, 2020 at 7:51:53 PM UTC-5, David Starner wrote: > > > I had a couple > unexplained segmentation faults, on job105 and job135. I restarted > job105 and it ran to completion; I haven't tried restarting 135 yet. > I'll restart 135 and actually start 137, and take 133, 134,

Re: [Metamath] Full 'minimize' run on set.mm

Here is an update of current commitments as of Feb. 13, 17:30 EST : 101 Alexander 102 heiphohmia 103-111 David Starner 112 David A. Wheeler 113-124 UNASSIGNED 125-132 David A. Wheeler 133-134 UNASSIGNED 135-143 David Starner 144-151 David A. Wheeler 152-160 UNASSIGNED Thierry has volunteered

Re: [Metamath] Full 'minimize' run on set.mm

On Thursday, February 13, 2020 at 9:25:42 AM UTC-5, Benoit wrote: > > David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement > tags. I'm away from my main computer... can you add them ? > > Actually, most *OLD and *ALT should probably have both discouragement tags > as well, it

Re: [Metamath] Full 'minimize' run on set.mm

On Thursday, February 13, 2020 at 12:14:44 AM UTC-5, Alexander van der Vekens wrote: > > I also tried several URLs, but always get Version 0.180 (and tested it > with minimizing axdc - the proof is always replaced by ax-dc, so the exe > does not contain the bug fix): > >

Re: [Metamath] Full 'minimize' run on set.mm

p reflect the executable update? I am getting the > same > hash as 0.180. > > Cheers, > > Norman Megill wrote: > > The job files have been updated for today's set.mm. The new job files > are > > available at http://us2.metamath.org/downloads/min2020-jobs.zip

Re: [Metamath] Full 'minimize' run on set.mm

On Wednesday, February 12, 2020 at 10:05:48 PM UTC-5, David Starner wrote: > > Given about 8 hours a run for me, I'll take two batches of 8; 103-111 and > 135 to 143. > That would be great. Just be aware that some or many of 133 and above (with 1 theorem each) are expected to take much more

Re: [Metamath] Full 'minimize' run on set.mm

On Wednesday, February 12, 2020 at 9:14:32 PM UTC-5, David A. Wheeler wrote: > > Note that I don't use the metamath "log" capability, and use the > Linux/Unix > built-in redirection mechanisms instead. If that's a problem of some kind, > let me know...! > The beginning and end will be a

Re: [Metamath] Full 'minimize' run on set.mm

' on axdc first matched syl5eq, it would then later correctly reject ax-dc. In other words, sometimes a new axiom would be accepted and other times it wouldn't, depending on the order in which the match occurred. Norm On Wednesday, February 12, 2020 at 12:52:38 PM UTC-5, Norman Megill wrote

Re: [Metamath] Full 'minimize' run on set.mm

for the work wasted and am very grateful to David Starner for finding this before we got too deep into the job runs. Norm On Wednesday, February 12, 2020 at 8:18:44 AM UTC-5, Norman Megill wrote: > > On Wednesday, February 12, 2020 at 5:53:59 AM UTC-5, Alexander van der > Vek

Re: [Metamath] Full 'minimize' run on set.mm

On Wednesday, February 12, 2020 at 5:53:59 AM UTC-5, Alexander van der Vekens wrote: > > On Wednesday, February 12, 2020 at 10:00:42 AM UTC+1, David Starner wrote: >> >> There might be an error in the minimize command; it found that axdc >> has a much shorter proof using ax-dc, which is

[Metamath] Re: Full 'minimize' run on set.mm

On Tuesday, February 11, 2020 at 4:20:57 PM UTC-5, Alexander van der Vekens wrote: > > Hi Norm, > I accidentally picked job101 and started it. It's (still) running. I'll > send you the job101.log file after the job has finished. > Thanks. That makes our status: job101 assigned to AV,

[Metamath] Full 'minimize' run on set.mm

We are ready to do a full 'minimize' run on set.mm. So you can fire up your high-end gaming rigs for some serious work and help make the world a better place through shorter proofs. :) With the help of Saveliy's script mentioned at

Re: [Metamath] Re: metamath-program.zip archive getting ninja edited

On Sunday, February 2, 2020 at 8:50:35 PM UTC-5, heiphohmia wrote: > > > I tested it, and tar.bz2 seems stable but tar.gz changes its md5sum each > > time I run tar -czf. > > Hrm. Both Nix and Guix rely on the fact that tar.bz2, tar.gz, and tar.xz > can be > made deterministic. However, this

[Metamath] metamath.org domain

See https://savedotorg.org/ A private equity firm called Ethos Capital is planning to buy the .org top-level domain from the non-profit Public Interest Registry (PIR), which manages .org (with 10.5 million domains), for $1.135 billion or about $108 per domain. With a monopoly on the .org TLD,

[Metamath] Re: Philosophy and goals for set.mm

@benoit and @alexander - Thank you for your comments. Go ahead and import semigroup (assuming no one else objects). Hopefully, though, I've communicated my point that we don't want this to lead to flurry of shallow definitions that people must learn, just to address a perceived difficulty in

Re: [Metamath] Re: metamath-program.zip archive getting ninja edited

On Saturday, February 1, 2020 at 11:49:53 PM UTC-5, heiphohmia wrote: > > > Could .gz or .bz2 be used instead? I think those are stable. I tested it, and tar.bz2 seems stable but tar.gz changes its md5sum each time I run tar -czf. That is very surprising because I'm almost positive that

Re: [Metamath] Re: Philosophy and goals for set.mm

On Saturday, February 1, 2020 at 8:53:26 PM UTC-5, David Starner wrote: ... I'm just > saying, if you want to learn group theory from Metamath, there's a lot > of stuff you're going to be fighting, and standard monoids, semigroups > and magmas are hardly going to be your breaking point.) >

Re: [Metamath] Re: Philosophy and goals for set.mm

On Saturday, February 1, 2020 at 10:54:31 AM UTC-5, Benoit wrote: > > On Saturday, February 1, 2020 at 3:37:57 AM UTC+1, Norman Megill wrote: >> >> On Friday, January 31, 2020 at 8:23:08 PM UTC-5, Benoit wrote: >>> >>> Regarding the possible introdu

[Metamath] Re: metamath-program.zip archive getting ninja edited

On Saturday, February 1, 2020 at 11:39:04 AM UTC-5, vvs wrote: > > So the zip command apparently does not produce an identical compressed >> file even if the contents are the same. >> > > They never meant to be reproducible. You should use something like > torrentzip for such purpose. > > Do

Re: [Metamath] Re: Philosophy and goals for set.mm

On Friday, January 31, 2020 at 8:23:08 PM UTC-5, Benoit wrote: > > Regarding the possible introduction in the main part of semigroups and > magmas: > When I look at the page http://us2.metamath.org/mpeuni/df-mnd.html I feel > a bit dizzy. The abundance of parentheses and conjunctions makes it

Re: [Metamath] Re: Philosophy and goals for set.mm

On Friday, January 31, 2020 at 8:19:00 PM UTC-5, Jim Kingdon wrote: > > > > On January 31, 2020 3:39:46 PM PST, Norman Megill wrote: > > >I would like to hear other opinions on whether "magma" and "semigroup" > >should become part of the main set

[Metamath] Re: Philosophy and goals for set.mm

On Tuesday, January 28, 2020 at 1:53:14 PM UTC-5, Alexander van der Vekens wrote: > > I want to come back to the first post of this topic, and I want to > concentrate on the "definition" parts (2 and 4): > Thanks for your comments! > > On Friday, January 24, 2020

[Metamath] Re: Philosophy and goals for set.mm

roject, but the huge amount of background material that would have to be developed would be amazing and probably useful for many other things long before the final goal is reached (if it ever is). What would other people like to see (magic genie or not)? Norm On Thursday, January 23, 2020 at

[Metamath] Re: Hiding lemmas on the website

On Friday, January 24, 2020 at 11:50:54 AM UTC-5, David Starner wrote: > > When digging through the website theorem list, there's a number of > times one comes upon one or more proofs just used that are just there > to be lemmas for other proofs and have cryptic names. Wouldn't it be > better

[Metamath] Philosophy and goals for set.mm

Tierry, Alexander, and Benoit have asked for clarification of the goals of set.mm. Here are some of my opinions. I am moving the discussion in https://github.com/metamath/set.mm/issues/1431 to here for wider readership. *1.* There is no "goal" per se for set.mm. People work on what they are

[Metamath] Re: AI

More AI "Calculemus!": Leibniz believed calculation would be the key to settling all human disagreements. A famous attempt was Godel's 1970 ontological argument, which was puzzled over and discussed by philosophers for decades, until 2013 when an AI-based theorem prover discovered an

[Metamath] Re: Proposal: Mark dummylink & idi with "(New usage is discouraged.)"

On Monday, January 13, 2020 at 5:51:18 AM UTC-5, Alexander van der Vekens wrote: > > As far as I can remember, idi was *inserted* by 'minimize' in some cases, > and I had to remove it manually. Unfortunately, I do not know when and in > which context this appeared, but I think the concerned

Re: [Metamath] Re: Proposal: Mark dummylink & idi with "(New usage is discouraged.)"

un, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill wrote: > > > > > Alan Sare's tool "completeusersproof" appears to make use of idi, at > least > > it appears in his C code and is referenced extensively in the program > > comments. Although this

[Metamath] Re: Proposal: Mark dummylink & idi with "(New usage is discouraged.)"

On Sunday, January 12, 2020 at 7:09:17 PM UTC-5, Norman Megill wrote: > > As for idi, I don't really care - mmj2 used to make use of it but I don't > think it does anymore. As far as I am concerned, we can delete idi unless > someone has a use for it. > > Alan Sare's tool &

[Metamath] Re: Proposal: Mark dummylink & idi with "(New usage is discouraged.)"

I don't think it's necessarily because both of these will automatically be removed with 'minimize'. While I may be the only one to do so, I have used dummylink to build proofs in MM-PA to work around the "backwards only" method it requires. Making it 'discouraged' will be a nuisance that I'll

Re: [Metamath] Handling "undefined terms"

the practice of at least one well-regarded authority. On Sunday, January 12, 2020 at 6:09:52 PM UTC-5, Norman Megill wrote: > > On Sunday, January 12, 2020 at 5:24:59 PM UTC-5, Benoit wrote: >> >> On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote: >> &g

Re: [Metamath] Handling "undefined terms"

On Sunday, January 12, 2020 at 5:24:59 PM UTC-5, Benoit wrote: > > On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote: > ... > > The key insight is that because this does not affect consistency (it's a > definition) > > I don't understand: definitions like this may lead

[Metamath] Re: Deprecated sections of set.mm

On Saturday, January 11, 2020 at 1:33:13 PM UTC-5, Jon P wrote: > > Quick question: Why are the following sections marked as depricated in > set.mm? > > PART 18 ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED) > > PART 19 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED) > The

Re: [Metamath] Re: Using underscores in labels

On Monday, January 6, 2020 at 1:03:23 AM UTC-5, Mario Carneiro wrote: ... > > I wish we would stop using the description comment for metadata like this. > This is the sort of thing that makes markup parsing the rats' nest that it > is. Just have a separate comment, with a sane computer-readable

[Metamath] Re: Using underscores in labels

On Sunday, January 5, 2020 at 1:42:44 PM UTC-5, Alexander van der Vekens wrote: > > Thanks, Norm, for these hints - it could have been expected that the > discussion about labels is not new... > > Your approach, which I like very much, goes in a similar direction as my > suggestion adding

Re: [Metamath] Re: Using underscores in labels

On Sunday, January 5, 2020 at 10:56:11 PM UTC-5, David A. Wheeler wrote: > > On Sun, 5 Jan 2020 09:23:21 -0800 (PST), Norman Megill wrote: > ... > > > > Basically we start with David's convention table to produce a table of > > acronyms and their expansions

[Metamath] Re: Abbreviation for square root

On Sunday, January 5, 2020 at 7:52:07 PM UTC-5, Norman Megill wrote: > > On Sunday, January 5, 2020 at 7:39:14 PM UTC-5, Benoit wrote: >> >> >> Is there any computer language anywhere that uses "sqr" for square? >>> >> >> Pascal is one of

[Metamath] Re: Abbreviation for square root

On Sunday, January 5, 2020 at 7:39:14 PM UTC-5, Benoit wrote: > > > Is there any computer language anywhere that uses "sqr" for square? >> > > Pascal is one of them: > http://xoomer.virgilio.it/gciabu/engl/pascal/pas038.htm > I understand the size concern with all the compound labels, but here

[Metamath] Re: Abbreviation for square root

On Sunday, January 5, 2020 at 4:22:13 PM UTC-5, Alexander van der Vekens wrote: > > Hi Benoît > > On Sunday, January 5, 2020 at 8:21:26 PM UTC+1, Benoit wrote: >> >> Indeed, I think that BASIC also uses "sqr" for "square root", but for >> most modern languages, this is "sqrt". Anyway, "sqr" is

[Metamath] Re: Using underscores in labels

I also dislike the idea of have to type 3_eq_tr_4_d instead of 3eqtr4d. I mentioned an idea here that in principle might appease everyone:: https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/q6P_IaKHBAAJ which links in particular to http://us.metamath.org/mpegif/mmnotes2004.txt (search for

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

On Friday, January 3, 2020 at 6:56:21 PM UTC-5, David A. Wheeler wrote: > > > > 2. Cryptic labels: He is ranting while faced with theorem names on the > HTML > > page of sqr2irr. No clue whatsoever what they mean. Compares this to > more > > explicit names found in competing products, and in

[Metamath] Re: A formula for 'minimize' run time or how to schedule minimization

On Tuesday, December 31, 2019 at 6:47:00 AM UTC-5, savask wrote: > > A few days ago I stumbled upon a topic "Formula wanted to estimate > 'minimize' run times > " by Norman > where he suggested an interesting problem of finding an

[Metamath] Re: Promoting to the main body Scott Fenton's theorems about finite and infinite products ?

I agree. You can move these into the main part of set.mm. On Sunday, December 29, 2019 at 9:59:24 AM UTC-5, Glauco wrote: > > I was checking if, recently, something similar to sum_ was added for > multiplication, and I found these sections in Scott Fenton's mathbox: > > 21.8.8 Complex products

[Metamath] Re: Labels in mathboxes and fostering collaborations

On Friday, December 27, 2019 at 5:23:37 PM UTC-5, Benoit wrote: > > Hi all, > > I found it convenient to label most of the theorems in my mathbox as > bj-xxx (my initials). This allows me to do things like "MM> verify proof > bj-*" and other things like bulk minimizations and potentially more

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

On Monday, December 23, 2019 at 3:58:12 AM UTC-5, Alexander van der Vekens wrote: > > On Sunday, December 22, 2019 at 4:34:17 PM UTC+1, Mario Carneiro wrote: >> >> ... set.mm would have been an optimal starting point, except it's HUGE, >> which makes introductory stuff harder. Even worse, it

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

Thanks for posting your impressions. I'm not quite sure what to make of it all yet, but it would be interesting to hear more of what people think. Looking at his YouTube home page, he posted 5 related videos about a month ago. His exploration of Metamath seems to start in the middle of the

[Metamath] TEST - please ignore

(I am having missing email problems. This is a test, please ignore.) -- 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

[Metamath] Re: 'minimize' runs

Yes, I forgot to include /time, which was also used in the runs 2 years ago. I had in mind finding a function that correlated proof size and set.mm position to run time (at least roughly) to help plan jobs with more predictable run times, but I never got around to it. I still have the data,

[Metamath] Re: 'minimize' runs

(Switching to the mininmize thread) On Tuesday, December 17, 2019 at 12:46:30 PM UTC-5, David A. Wheeler wrote: > > > >The last one I did myself was around 3 years ago, using a laptop with a > >powerful i7 processor maxed out with 8 threads. > > Can metamath automatically use all the CPUs

[Metamath] 'minimize' runs

if it seems safe I can let 'minimize' run in the background for several weeks. Norm > Mario > > On Mon, Dec 16, 2019 at 6:56 PM Norman Megill wrote: > >> On Monday, December 16, 2019 at 4:43:01 PM UTC-5, Benoit wrote: >> ... >> >>> >>>> > unf

[Metamath] Re: Proven: Fourier series convergence, #76

On Monday, December 16, 2019 at 4:43:01 PM UTC-5, Benoit wrote: ... > >> > unfortunately I miss some of the features of metamath.exe , because I >> use mmj2 only (but I'm really intrigued by Thierry's plugin for Eclipse, I >> hope I will soon have time to take a closer look at it). >> > If

Re: [Metamath] Packaging Metamath for Linux distros

On Monday, December 16, 2019 at 8:34:02 AM UTC-5, heiphohmia at wilsonb.com wrote: > > > And why not a special Linux source distribution... > > The URL that Norm shared pretty much ticks all the boxes you outline. The > only > substantive difference being that the metamath.exe is not excluded.

Re: [Metamath] Packaging Metamath for Linux distros

On Friday, December 13, 2019 at 3:30:53 AM UTC-5, heiphohmia wilsonb.com wrote: > > Thank you for the response. > > > Would it work for you to download the source? > > Unfortunately, no. Void Linux has a policy of only packing "stable" > releases, > which in practice means no builds off

[Metamath] Re: Removing dependencies on ax-13

I think that moving these to the main set.mm before ax-13 is introduced, and also moving up anything that no longer depends on ax-13 as a consequence, is a good idea. You can go ahead and do that. I am a little puzzled by "but it would add around a hundred more theorems to the FOL part of

[Metamath] Re: Is it possible for a constant to become inactive?

On Monday, November 25, 2019 at 11:33:33 AM UTC-5, Marko Grdinic wrote: > > As the language is simple enough, I've decided to try implementing it on > my own in F# in order to get a grasp on it. > > In the spec (page 132/247 of the Metamath book) it says that constants can > only be declared in

[Metamath] Re: Problem with us2 ?

Sorry, I encountered a problem testing a metamath.exe modification, so I abandoned the site build. The site is updated now. In general I do try to rebuild the site within 24 hours of a PR but occasionally there may be a delay. Norm On Thursday, November 21, 2019 at 6:42:38 AM UTC-5, Benoit

<    1   2   3   >