[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 intent

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 t

Re: [Metamath] Handling "undefined terms"

lowing 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: &

[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

[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 Sar

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

as long as you carefully inspect what it did. On Sunday, January 12, 2020 at 9:15:44 PM UTC-5, David A. Wheeler wrote: > > On Sun, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill wrote: > > > > > Alan Sare's tool "completeusersproof" appears to make use o

[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 the

[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 inconsis

[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: 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 if

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

ot;flyspeck" (Kepler conjecture) type project, 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 no

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

On Saturday, January 25, 2020 at 5:10:21 PM UTC-5, Alexander van der Vekens wrote: > > On Saturday, January 25, 2020 at 3:12:17 PM UTC+1, David A. Wheeler wrote: >> >> Giovanni Mascellani: >> > To me MM100 is a an interesting goal, but definitely an intermediate >> > one. The (admittedly, very a

[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

Your counterexamples to show non-membership are interesting. I appreciate your work dong this, and certainly it would accompany the magma and semigroup structures should we decide to import them. However, showing the proper subset relationship in and of itself still doesn't quite yet show us

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

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 ha

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

Nothing was changed inside the zip file between the dates you mention. The zip file is recreated from source about once a day from the command: zip -9 downloads/metamath-program.zip metamath/*.c metamath/*.h \ metamath/metamath.exe metamath/configure.ac metamath/Makefile.am \ metamath/met

[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 you

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 introductio

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.) > Th

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 tar.g

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

Thanks. I did get trrntzip to work yesterday from the source files, although there was a lot of trial and error that I'm not sure I can reproduce. :) (SourceForge doesn't like wget, so I ended up downloading through a browser in Windows.) So I'll keep your instructions for the next time I ha

[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

[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,

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 is

[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 https://groups.google.com/d/msg/metamath/djIdTu2Wq-I/mgs4MD7Y

[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, job102-jo

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 obviously

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

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 > Vekens wrote:

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

On Wednesday, February 12, 2020 at 5:10:34 PM UTC-5, David A. Wheeler wrote: > > While we're waiting for the tweaks to metamath.exe to fix the > minimize bug, below is a quick shell script I wrote to do this for > Linux/Unix. > > If you store this as file "jobs" and make it executable ("chmod a+

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

econd and later matches, if any, would not bring in new axioms. So if, for example, 'minimize' 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

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

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 The instructions at the beginning of this thread ( https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/1lURYnVcFwAJ) still apply, except that you should use

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

Interesting. BTW the run time for 3atlem4 in your log was 67 sec, compared to 31 sec in Alexander's log. So your 15 hours would likely correspond to about 7 hours on Alexander's computer. (I chose 3atlem4 arbitrarily as a reference was because it was the first one I saw that was neither too f

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 little

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 tha

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.

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): > > http://us.metamath.org/m

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

Here are the current commitments: 101 Alexander 102 heiphohmia 103-111 David Starner 125-132 David A. Wheeler 135-143 David Starner 144-151 David A. Wheeler Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and st

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 see

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 star

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

On Thursday, February 13, 2020 at 7:27:44 PM UTC-5, heiphohmia wrote: > I will take the 12 jobs 113-124, anticipating it to take about 2 weeks in > total > given my hardware. > Well, the way things are going we may be able to complete this before 2 weeks. If you are running 1 job at a time @

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

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 co

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 progress

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

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: https://groups.google.com/d/msg

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 "c

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 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 the &g

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 preliminar

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

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 Norman Megill wrote: >> > ... > Does that mean that 125-132 are open a

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

:14:42 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

On Friday, February 14, 2020 at 8:30:51 PM UTC-5, David A. Wheeler wrote: > I've already restarted my assigned jobs: > scripts/jobs 112 125-132 144-151 You didn't have to restart 144-151. Jobs 133 and above are not affected. If any of 144-151 had already finished, do you have the logs for them? T

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 del

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 > https://dwheeler.com

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

On Saturday, February 15, 2020 at 2:56:18 PM UTC-5, David A. Wheeler wrote: > > An update: Now I've also finished job 132, available here: > https://dwheeler.com/temp/job132.log > Thanks. The status is updated. https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ > > My compute

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 r

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 me

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 mi

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] Full 'minimize' run on set.mm

UQ5pJp8/odjUQM6nBAAJ 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 Norm

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

[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: http://us2.metamath.org/down

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 5.68s

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

rom 9585 to 9567 bytes using "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 Thursda

[Metamath] Re: Where is the fashionable mathematics?

I'll recall that vvs mentioned this on Feb. 10: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/h9PRflr9FgAJ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/: "What if an undergraduate wants to try formalising the Hilbert basis theorem? What do they do

[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: 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: 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&#

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 only

[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 that

[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] 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 discouragements on

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 >

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 us

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 would

NN vs. NN0 again Was: Re: [Metamath] Re: Formalizing IMO B2.1972

On Wednesday, March 4, 2020 at 10:36:50 AM UTC-5, Benoit wrote: ... > Beware that in set.mm, the symbol NN does not denote the natural numbers, >> but only the nonzero natural numbers. Therefore, stating ~ inductionexd >> with " N e. NN0 " is more... natural. (And its proof might be shorter

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 > n

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 t

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

And thanks to Saveliy Skresanov for providing the script preparejobs.sh that made the process of creating the jobs much easier, and to David A. Wheeler for writing the jobs script to automate the process of launching the jobs. Norm On Thursday, March 5, 2020 at 9:07:14 PM UTC-5, Norman Megill

[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 logi

[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 variables,

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 firs

[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] 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 mi

[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

[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 o

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

ling to reconsider 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

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: >> >> $\overset{\sim}{\

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 no

[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 difficul

[Metamath] Re: Can a floating hypothesis become essential?

It looks like this check has been done in metamath.exe all the way back to 1997 (the oldest I have, barring some miracle that allows me to read the ancient TK50 backup tapes in my closet). Right now I can't remember the reasoning behind it, if there was one (other than it is not something one

[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 exactly

[Metamath] Re: Can a floating hypothesis become essential?

OK, I'll turn it into a warning. If in the future we determine that it has a legitimate use, we can easily turn off the warning. But the warning will at least notify the user that something very unusual is being done. Norm On Saturday, April 18, 2020 at 10:47:30 AM UTC-4, savask wrote: > > I

Re: [Metamath] Re: Denoting morphisms in set.mm

A scan is attached. On Saturday, April 18, 2020 at 10:56:23 AM UTC-4, David Starner wrote: > > On Sat, Apr 18, 2020 at 7:14 AM Norman Megill wrote: > > > > Regarding: > > > > F : A -1-1-> > F : A >--> B > > F : A -onto->

[Metamath] FL: ++; binary connectives

FL asked me to post these. Forwarded Message Subject:++ Date: Fri, 24 Apr 2020 21:33:34 +0200 (CEST) From: fl To: Megill Norman Hi Norm, can you post this? I suggest that ++ replace concat. Currently ++ is used for a concept rarely if ever used. On the contr

[Metamath] Re: FL: ++; binary connectives

> 1. I have no strong opinion on ++ vs. concat, except that "concat" seems > more self-explanatory. "concat" occurs 373 times in set.mm, so ++ would > save 1492 bytes in set.mm size. > > I'll also mention that Tarski used a frown symbol for concatenation in his 1965 paper. His notation is re

Re: [Metamath] Re: FL: ++; binary connectives

>From FL: Forwarded Message Subject: ++, indices and Commons Date: Sat, 25 Apr 2020 11:53:57 +0200 (CEST) From: fl To: Megill Norman Hi Norm, could you post this: Yes I made a mistake. Scott Fenton uses (++) and not ++. So the symbol ++ is available. I would also appreciat

Re: [Metamath] Re: FL: ++; binary connectives

On Saturday, April 25, 2020 at 1:33:20 PM UTC-4, Jim Kingdon wrote: > > With respect to exclusive or, there are a lot of theorems in set.mm which > use ?? <-> -. ?? (examples: sotric , posn , nneo , nltpnft ). At least some > of these can be productively thought of as exclusive or and may benefit

[Metamath] Re: FL: ++; binary connectives

Posted per request of FL. Forwarded Message Subject: Operators Date: Sat, 25 Apr 2020 21:21:07 +0200 (CEST) From: fl To: Megill Norman Let's agree: of course the opinion that we should confine ourselvesto the 5 classical operators for the formulation of the theorems. The study

  1   2   3   >