Re: [Metamath] Test if mailing list is working

I got this email. On May 22, 2024 12:31:03 AM PDT, 'asdf asdf' via Metamath wrote: >Hi guys, metakunt here, > >this is just a test to see if the mailing list works for me. Thank you very >much for support in getting this to work. > > > >Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe

Re: [Metamath] Feedback from metakunt, a recent contributor

On 5/16/24 04:02, 'ookami' via Metamath wrote: I hope it is as simple as writing an E-mail to metamath at googlegroups.com. As far as I know that works. Converting a theorem into deduction form with 5 or more conjuncts will amortize after 1 or 2 usages. Once you get up to 5 or more

Re: [Metamath] Re: The Ackermann function

On 4/28/24 06:29, 'Thierry Arnoux' via Metamath wrote: Maybe I would try as follows, using the seq operator instead of recs, and the definition as an iterated 1-ary function : I didn't try to check every

Re: [Metamath] Question abouot indistopon

On April 22, 2024 11:20:58 PM PDT, "'B. Wilson' via Metamath" wrote: >It looks suspiciously close to A e. _V which reas as "A is a set", but in this >case the V is just floating. What are the semantics here? > It functions much like A e. _V would. A proof using this theorem can always plug

Re: [Metamath] Results about ax-13 usage

On 3/11/24 04:32, Mario Carneiro wrote: Given a free choice I think that developing in the same database is better since then intuitionistic proofs can be used in classical theorems (and vice versa, when the classical theorem was not actually using classical logic on accident or because of a

Re: [Metamath] Prime Number Theorem

een people who know the >> math but don't do formalization, and people who like to do formalization >> but are maybe not so sure about the advanced math involved. >> >> I think it would be beneficial for the Metamath community to have such a >> tool, too. I've been th

[Metamath] Prime Number Theorem

Looks like Terrence Tao is planning [1] to follow in the footsteps of Mario Carneiro [2] and formalize the Prime Number Theorem. More seriously, it is really nice to see people getting excited about formalization. I figure this can only be a good thing. [1]

Re: [Metamath] Results about ax-13 usage

that had the greatest benefits, but since there was no clear criterion, this kind of stalled. Benoît On Tuesday, January 2, 2024 at 12:52:10 AM UTC+1 di@gmail.com wrote: On Mon, Jan 1, 2024 at 6:43 PM Jim Kingdon

Re: [Metamath] Results about ax-13 usage

This isn't something I'm likely to get hugely involved with myself, but it does intrigue me particularly from the point of iset.mm.  There right now we have both https://us.metamath.org/ileuni/ax-bndl.html and https://us.metamath.org/ileuni/ax-i12.html (stronger and weaker forms of what in

Re: [Metamath] German translation of the Metamath book

Wow. For those who haven't translated anything, it might sound easy ("oh I know both languages and the subject matter") but my experience is that translating a sentence or two is one thing, but translating a larger work (in this case, a 200 page book) is quite another. Thanks! Adding to

Re: [Metamath] Re: Yamma

Not that I'm discouraging you from making this better in Yamma but what I do in mmj2 is: 1. Load the file in mmj2 and save .mmp files for everything I want to work on. Quit mmj2. 2. Go to a text editor and make changes to hypotheses or whatever it is. 3. Load the .mmp files. Steps that don't

Re: [Metamath] Re: Yamma

On November 26, 2023 6:41:32 AM PST, Glauco wrote: >Yamma now builds a (partial) theory, even if some proofs are not valid. Ooh nice. I have my workarounds to handle these kinds of changes using mmj2 but having the tool understand it better sounds like it could be a significant help. --

[Metamath] renames of syl theorems

This discussion has been a bit spread across a few issues and pull requests, so it seems good to offer a message here about the rename underway to some of the theorems with "syl" in their names. There is a list of all the theorems affected here:

Re: [Metamath] Website is down

Clicking around now.. * https://us.metamath.org/ileuni/mmil.html is up to date (missing theorems list goes to dvcn) for the first time in over a year. https://us.metamath.org/ilegif/mmil.html too. * https://us.metamath.org/mpeuni/mmset.html and https://us.metamath.org/mpegif/mmset.html

[Metamath] naming of syl theorems

Most theorems which involve applying transitivity are named according to a pattern XXYYtr where XX and YY are abbreviations for what kind of theorem this is and then the usual suffixes apply. Examples: eqeltrd sseqtri And if XX and YY are the same the abbreviation is only listed once, for

Re: [Metamath] Update: website generation rewrite

On 9/30/23 04:27, Mario Carneiro wrote: Moreover, I am of the opinion that we should also move all the .html and .raw.html files from set.mm repo to the website repo, even though those files are more heavily trafficked than most other pages. When you want to add a new page,

Re: [Metamath] Update: website generation rewrite

On 9/29/23 21:52, Mario Carneiro wrote: in my test these are 4893.94 s and 5020.87 s respectively (that is, 2h45m total). I just got the new version working, and it takes 10.8 s and 11.1 s respectively Exciting stuff! This has me pondering various possibilities, such as generating the

Re: [Metamath] fnconstg

On 9/22/23 17:00, tbrend...@gmail.com wrote: I'm extremely hesitant to suggest changes to the main database, having flunked out of school now twice, but working on what I call "cmpcvxhmph" and "cmpcvxhmph0" (i.e., that any complex convex shape is homeomorphic to the unit ball), I'm finding

Re: [Metamath] Metamath Website not loading

On September 9, 2023 3:29:19 PM PDT, heiphohmia via Metamath wrote: > . FYI, the README >in metamath-website-scripts still mentions contacting Norm  If this is the mention I am thinking of, I'm way ahead of you: https://github.com/metamath/metamath-website-seed/pull/17 -- You received

Re: [Metamath] Metamath Website not loading

On 9/9/23 11:37, David A. Wheeler wrote: 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 :-). First of all, THANK YOU for all your efforts! Secondly, you have done a

Re: [Metamath] Metamath Website not loading

I am seeing this too (since some time yesterday). I haven't heard anything about causes or whether there is an effort underway to fix it. On September 5, 2023 3:11:31 AM PDT, Sophie wrote: >The main page gives a 403 Forbidden Error, whilst the subpages give a 404 >Not Found Error > >-- >You

[Metamath] Announcing an additional Metamath 100 Theorem for iset.mm

I am pleased to report the successful completion of the project to formalize the equinumerosity of the rationals and the natural numbers in iset.mm.[1]  This project was begun in earnest in May 2022 with the opening of a github issue[2] which quickly led to discussions and partial results

Re: [Metamath] Trouble understanding Deduction style

, 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

Re: [Metamath] Trouble understanding Deduction style

On 8/15/23 07:49, David A. Wheeler wrote: Maybe we should note something in trud. Ooh, good idea. I hadn't thought of that as a mitigation. Submitted as https://github.com/metamath/set.mm/pull/3388 -- You received this message because you are subscribed to the Google Groups "Metamath"

Re: [Metamath] Trouble understanding Deduction style

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

[Metamath] Proposed rename of mpt2 abbreviation to mpo

Since this is a somewhat large change (well in terms of the number of lines of set.mm/iset.mm affected anyway, if not conceptually), I should probably ask on the mailing list what people think of the proposed rename of all the labels now containing "mpt2" for maps-to-operation to "mpo".

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

First of all, welcome! Always good to have more people doing things with metamath. Various people would be glad to look at your submission but I think making it a pull request will be the easiest way to let them look at the change. I mean you could make it a Draft Pull Request if you really

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

On 7/14/23 17:48, David A. Wheeler wrote: No, we're not expecting anyone to do #33 (Fermat's Last Theorem) right now, but some of these seem relatively within our grasp. Maybe not, but we need proofs of Fermat's Last Theorem for n=3 and n=4 and that should be in the "within our grasp"

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

On 7/4/23 15:07, Marshall Stoner wrote: What I'm writing is not directly connected with meta-math, but something that I feel could help explain it better for novices I'd advise you to follow where the inspiration leads you. If you end up with something which has a lot of metamath notation

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

On 7/4/23 14:45, Marshall Stoner wrote: It seems like allowing bundled variables is what causes a lot of complexity in a few proofs.  My philosophy would be to keep variables distinct except for special cases where it might be necessary or helpul Specifying distinct variables most of the

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

On 7/3/23 15:56, Marshall Stoner wrote: have written up everything I considered prior to the definition of the biconditional and conjugation. . . . will attach and share what I have written so far as soon as I know that I am approved for the mailing list. . . . I'll be curious to see what

[Metamath] Metamath is famous! Tau Day famous that is

This year's State of the Tau includes the following item: "Aleksandr Alekseevich Adamov (who made the Russian translation of /The Tau Manifesto/) passed along a link to a formalized proof that τ = 2π" from tauday.com/state-of-the-tau and it links to

Re: [Metamath] Metamath-lamp video, part 1

I watched this and it looks good to me. On 6/24/23 11:31, David A. Wheeler wrote: 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

[Metamath] kids these days

I think this whole "formal proof software" thing just might work out: https://mathstodon.xyz/@MartinEscardo/110510148351643267 -- 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

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

I often discuss my math hobby with acquaintances and I usually lead with something like "I write math proofs that can be checked by a computer". Granted, that is as a conversation opener rather than a web site but perhaps something as brief as that could be a candidate for the one sentence

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

Oh cool. I was aware that equals and subset and df-br don't take parentheses but I hadn't quite thought of them as all examples of a "class thing class" (and produce a formula) pattern. I see we have this nicely documented in the "Infix and parentheses" section of conventions.html On June 5,

Re: [Metamath] How to Understand The "More Complicated" Expressions in Definitions

The specific question of what it means for two restricted quantifiers to be next to each other is perhaps best answered by pointing to a simpler example like https://us.metamath.org/mpeuni/r19.12.html - the ∀푦 ∈ 퐵 ∃푥 ∈ 퐴 휑 there has the same syntax as ∀푎 ∈ (Base‘푔)∃푚 ∈ (Base‘푔)(푚(+g‘푔)푎) =

Re: [Metamath] Is set.mm available in a more "machine-readable" format other than in html?

My mind went to metamath-exe commands like SHOW USAGE and SHOW TRACE_BACK and even SHOW PROOF. Agreed that the question will depend on what one is trying to find out, but parsing the HTML is probably more difficult than other approaches (at least for most information you'd want - there might

Re: [Metamath] how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style)

We already have the biconditionalized version of this at https://us.metamath.org/mpeuni/elnnz1.html There's a general rule here, which is written down in https://us.metamath.org/mpeuni/conventions.html in the paragraph starting "There are basically two ways to maximize the effectiveness of

Re: [Metamath] Negative use cases database?

When I wrote * https://github.com/metamath/metamath-exe/blob/master/tests/disjoint1.expected * https://github.com/metamath/metamath-exe/blob/master/tests/disjoint2.expected * https://github.com/metamath/metamath-exe/blob/master/tests/disjoint3.expected I thought there would be a lot

Re: [Metamath] Re: Formalizing Fermat's Last Theorem

Oooh, thanks. I've been thinking a bit about formalizing n=3 or n=4 in metamath (or perhaps more likely, encouraging others to do so) but I was just thinking in terms of something we could accomplish soon, I didn't realize that the proof via the Modularity Theorem also needed those cases to be

Re: [Metamath] Re: Formalizing Fermat's Last Theorem

Looks like http://www.ipam.ucla.edu/abstract/?tid=19347=MAP2023 has both an abstract (which goes into more detail about what the talk is about) and a video of the talk. Maybe you'd be able to figure out where this fits into your outline; I'm afraid I'm even less far up the learning curve than

[Metamath] Formalizing Fermat's Last Theorem

I know this is a bit of a white whale and there is a lot of mathematics to formalize before this is even in reach. But when the formal math community (taken as a whole) is at 99 out of 100 of the Top 100 list, of course it is easy to focus on the one. Anyway the news is that there was a recent

Re: [Metamath] Hardened us.metamath.org

Thank you! On February 12, 2023 5:58:14 PM PST, "David A. Wheeler" wrote: >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

Re: [Metamath] Thanks for being a vibrant & active community

Thank you too David for your significant contributions to making this happen. And also I'd like to express my appreciation that Norm did so much to welcome contributions and draw in people who might help. So many formal math projects never advance beyond the stage of one professor and their

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

On 2/11/23 07:39, David A. Wheeler wrote: 1) I think one of the "key" missing things is ability to help a user to understand why a statement doesn't unify. I have only an approximate idea of whether this is easy or hard, but I will say that even modest improvements here would be helpful. For

Re: [Metamath] Trouble running mmj2

I run it via the https://github.com/digama0/mmj2/blob/master/mmj2jar/mmj2 script which supplies many of the needed parameters. On January 23, 2023 12:51:43 PM PST, M Malik wrote: >Hello Metamath people, > >I am sorry if this has been answered before. I installed mmj2 through >Github, but I am

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

I think there is a certain amount of overlap between the Schwabhauser book and Tarski, Alfred; Givant, Steven (1999), "Tarski's system of geometry", The Bulletin of Symbolic Logic 5 (2): 175–214, [[doi:10.2307/421089]], MR1791303, ISSN 1079-8986 which is in English. I think there used to be a

Re: [Metamath] Is MPE really *just* first order?

I'm not sure I have more insight than anyone else about how to organize our documentation, but this text does look pretty good. I always read such things with an eye towards whether it makes sense to someone who doesn't already know the topic (this is especially a problem with proof system

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

There are a lot of ideas on this thread which might be worth doing, but the redirect from mpegif to mpeuni is the only which is in my mind a (likely) prerequisite for retiring mpegif. Most of the others we could do later if we find we wish we had them. On 1/2/23 07:49, Samiro Discher wrote:

[Metamath] website problem with symbols download

Although most files/downloads look OK, I'm getting zero bytes from http://us.metamath.org/downloads/symbols.tar.bz2 which is causing the tests at https://github.com/metamath/set.mm/actions/runs/3734891781/jobs/6337539307 to fail. I didn't see any recent changes to

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

Thanks for saying something. I don't seem to have the ability to merge this one either. Perhaps we can get some or all of the people who have write access to set.mm, metamath-exe, etc to have write access here too. I don't know whether merging the pull request is enough to get it on the web

[Metamath] pull request review

Can I get a review on https://github.com/metamath/set.mm/pull/2927 ? There's a moderately detailed comment there describing what this is about, but please do ask if you still have questions. It is quite similar to recently merged pull requests. (And while I'm at it

Re: [Metamath] Buiding on metamath-knife

It took me longer than I wanted to find the specification we wrote for the definition checker. It is in https://us.metamath.org/mpeuni/conventions.html towards the bottom (search for "additional rules for definitions"). As Mario said in this email thread it is not (at least currently) based on

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

Yeah, ideally we'd get all these files in git so we can use our regular process. But I don't want to too strongly push more work onto David and Mario (unless there is something I can do to help). On October 9, 2022 1:08:14 PM PDT, "David A. Wheeler" wrote: > > >> On Oct 9, 2022, at 3:05 PM,

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

On September 14, 2022 7:23:11 AM PDT, "David A. Wheeler" wrote: > >Mirror folks: Comments? For all the reasons you suggest, I'd pick the design where the mirrors pull from the central site. But I'm fine with whatever you and the mirror operators want to do. -- You received this message

Re: [Metamath] Need help reaching out to one of ypur members

In https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md there are names and GitHub handles for a few people who are willing to be contacted. Hopefully a GitHub private message is enough to get you started. On September 10, 2022 10:38:26 AM PDT, Federico Cretella wrote: >Hi all, >

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

On 8/30/22 16:18, David A. Wheeler wrote: Progress! We're one step closer to not using us2.metamath.org. Thank you again for all your work on this. Also send my thanks to Norm's partner who has been providing space and power for us2 during this transitional time. Can we drop the

Re: [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop"

Sounds good to me. I think requiring a pull request is uncontroversial. Requiring the tests to pass can sometimes seem like there should be exceptions when the tests fail for reasons which are perceived to not relate to the code being merged, but (1) fortunately our checks have been mostly

Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF)

/etc each of the proofs on the list depend on, so that's why I'm at least as worried about our own tracking as I am about how we are able to present it on that list. On August 23, 2022 7:52:08 AM PDT, "David A. Wheeler" wrote: > > >> On Aug 23, 2022, at 12:41

Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF)

On 8/22/22 07:33, David A. Wheeler wrote: This is really cool. I've alerted Freek & asked him to add a link to this in: https://www.cs.ru.nl/~freek/100#25 I have no idea how Freek will handle this. In this case we want *both* proofs to be cited. Also, this is a proof of unprovability, not a

[Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF)

Although it has long been known that the Schroeder-Bernstein theorem ( https://us.metamath.org/mpeuni/sbth.html in set.mm) is not provable in set theories such as IZF, it is only in the last decade or less that it has been known that Schroeder-Bernstein is equivalent to excluded middle (rather

Re: [Metamath] Re: Metamath site us.metamath.org status and plans

This part of the web page is in git at https://github.com/metamath/set.mm/blob/develop/mmset.raw.html#L468 so you can update it yourself via the normal pull request mechanism (can't remember whether you have been submitting pull requests, but if not there are lots of details at

Re: [Metamath] Symbol for ordinal number 0

Thank you. I'm pretty sure that was the message I was thinking of. It sounds like the separate symbols for ordinal less than and less than or equal were very early (well before anything which is in git, which starts with something Norm called set.mm.1998-03-16-from-vax). On 7/21/22 23:24,

Re: [Metamath] Symbol for ordinal number 0

I'm a bit skeptical. I remember Norm wrote a message to the mailing list (which I'm not sure how to find) about why we use e. and C_ for ordinal less than and ordinal no greater than, rather than having, say, even said we tried the latter for a while). I don't know if there was a similar

Re: [Metamath] Link to id1 on the metamath website

Thanks for reporting this! Here's a fix: https://github.com/metamath/set.mm/pull/2696 - assuming this is approved and merged it should be on the website a day or two after it is merged. On 7/19/22 07:43, Sophie wrote: The Law of identity link in

Re: [Metamath] Metamath website changes

Excellent news on the https . I clicked around for a while and didn't find any links which had broken in the process. And thank you for all your work on this. As usual, let me know if there is anything I can help with, or if moral support is needed, consider this email an expression of

Re: [Metamath] metamath GUI/Game in Smalltalk

Looks cool based on the screenshot and video. Given how popular colorful syntax highlighting has been for code, seems like there could well be an appeal to do something sort of similar in terms of the display here. On June 25, 2022 1:58:32 AM PDT, 'Peter Meadows' via Metamath wrote:

Re: [Metamath] Re: New verifiers/parsers/community projects

Seems sensible to me. I'm not sure I have any more insight than anyone else about whether it is a good idea, but I'm certainly in favor of encouraging new contributions as best we can. On June 6, 2022 3:00:56 PM PDT, Jon P wrote: >Yeah so this is the sort of thing I would imagine, for perhaps

Re: [Metamath] Re: New verifiers/parsers/community projects

On June 2, 2022 4:13:35 AM PDT, Jon P wrote: > >If that's helpful I don't mind doing the legwork of >writing the posts and finding appropriate places to put them (you have to >be sensitive to subreddit posting rules etc). Well I love the idea and it sounds like you have some ideas for how

Re: [Metamath] Re: New verifiers/parsers/community projects

On 5/31/22 17:34, Mario Carneiro wrote: I don't think proliferation of verifiers is a problem at all. I would like to see metamath verifiers on Rosetta Code and written in 200 languages. It's a weekend project so it doesn't have the same risks unless you want to start adding fancy features

Re: [Metamath] Re: mmverify.py bug

Thanks for asking about this. Here's a pull request to add this case to the metamath-exe testsuite: https://github.com/metamath/metamath-exe/pull/83 On 5/8/22 05:17, Glauco wrote: I can't find test.mm , but I'm using this old post to keep mmverify.py 'issues' in one place. I've written a

Re: [Metamath] Re: review on iset.mm seq theorems

Thanks! I have replied in github, hopefully we can figure out what to do about the issues raised there. Not too late if anyone else wants to take a look or ask any questions. I'm always game for talking about iset.mm and even though there might still be things to do with the recursion theorem

[Metamath] review on iset.mm seq theorems

Can I get a review on https://github.com/metamath/set.mm/pull/2584 ? I don't think there is anything especially controversial here (the funinsn part may or may not lead to anything else, but the rest is just the next step in the ongoing work to remove some of the conditions on seq theorems in

Re: [Metamath] Re: Suffix "t" for theorems in closed form.

I suppose we should document "t" as meaning closed form (although it is far less common than no suffix). We perhaps could get rid of "t" with a modest amount of renaming (as far as I could tell from "show label *t"), although when I look at something like all the *19.21* theorems, finding good

Re: [Metamath] Mapping Metamath predicate logic to traditional predicate logic

what you are thinking of. >Sorry for all the basic questions and thanks for the help! That's what this list is for. We've documented most of this stuff in various ways, but it can sometimes take a bit of help to find the relevant information and understand what you are reading. >On Fri,

Re: [Metamath] Mapping Metamath predicate logic to traditional predicate logic

Did you try going through http://us.metamath.org/mpeuni/mmset.html#traditional and http://us.metamath.org/mpeuni/mmset.html#distinct ? I suspect that might be closer to what you are looking for than those papers. As for the MM1 video, I totally agree. Although I've learned to do things in

Re: [Metamath] Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org?

Assuming we stick with the current linode set up, running us2 on the same linode is perhaps simplest. Whether that changes the cost, as far as I could tell from glancing at https://www.linode.com/pricing/ , depends on how close we are to the limits for RAM, storage, etc. Perhaps linode has an

Re: [Metamath] Re: How to express a quadratic form over a vector space

On 2/6/22 11:47, Mario Carneiro wrote: Two things: (1) it's been done, see hol.mm or dtt.mm . At least in my email cilent these got linked funny. The references are to http://us.metamath.org/holuni/mmhol.html and https://github.com/digama0/dtt.mm

[Metamath] Answer to "Why are my branches getting deleted when someone merges my pull request?"

Just wanted to let people know that Mario and I changed one of the github settings and so if you make a branch in the set.mm repository (as opposed to your own fork), make a pull request for it, and then that pull request gets merged, the branch will be automatically deleted. If you were still

Re: [Metamath] Re: Metamath vs Mizar for someone new to abstract math

You are probably ready to try out one or more prover systems (or keep trying out in the case of lean) rather than collect more opinions, but I'm pretty sure either Lean or methamath set.mm would be suitable in terms of being able to do things with functions, relations, integers, etc (and not

Re: [Metamath] CI Checks didn't kick in

I tried the old "close it and re-open" trick which didn't seem to help. Then I checked https://www.githubstatus.com/ and sure enough it says "GitHub Actions is experiencing degraded performance. We are still investigating and will provide an update when we have one. Feb 5, 22:25 UTC". This is

Re: [Metamath] Re: New markup checks

VERIFY MARKUP is being run on iset.mm and set.mm and is passing. Go to the latest entry in the Actions tab ( https://github.com/metamath/set.mm/runs/5038215989?check_suite_focus=true ), follow the link from the duplication check (takes you to

Re: [Metamath] Re: Proposal: Move metamath-knife into the "metamath" organization

Moving it to the metamath organization sounds good to me. Since it was always intended to be a community project, I've often thought that's the logical place for it, and all the more so if it already has multiple contributors as it seems that it does. I don't know if I have a grand theory for

Re: [Metamath] Big progress on metamath.org and us2.metamath.org

On 1/23/22 1:44 PM, David A. Wheeler wrote: I propose that we automatically update from us2.metamath.org to us.metamath, though perhaps not as often. E.g., maybe us2.metmath.org is updated every day, while us.metamath.org is updated only once a week (or on certain days of the week). That way,

Re: [Metamath] Big progress on metamath.org and us2.metamath.org

Thank you for putting in the time and effort. I knew that Norm's planning for this was nonzero but I'm not surprised that it didn't go as smoothly as hoped especially the first time. Let us know if there is anything we can help with (and if you just want encouragement and patience, I can do

Re: [Metamath] pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R `

Hey, thanks for sending those mathbox contributions. I see that you have been communicating with various people in the past so you are not a stranger to our community, but in case any of the following helps with how we generally manage mathboxes, I hope it is helpful. I don't know how

Re: [Metamath] Re: Metamath website

I've tried to write up the situation about Even and Odd at https://github.com/metamath/set.mm/issues/2433 . Hopefully it is helpful for me to summarize what was a rather long thread the last time this came up. Hopefully we can find a solution - it would be kind of silly if figuring out how

Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity

On 1/11/22 1:22 PM, Benoit wrote: It'll be easier when the website is updated (I guess the page you're talking about was locally generated on your computer, since I can't access http://us2.metamath.org/ileuni/bezout.html ?). Yeah, I ran SHOW STATEMENT bezout/ALT_HTML from within metamath.exe

Re: [Metamath] Re: Additional Metamath 100 proof in iset.mm: Bézout's identity

On January 11, 2022 8:11:02 AM PST, Benoit wrote: I think one can say without too much of a stretch that the proof is in Heyting arithmetic (Peano's axioms do not appear as axioms in iset.mm, but if one traces back your proofs, one can probably convince oneself that this is the case) so

[Metamath] Additional Metamath 100 proof in iset.mm: Bézout's identity

For those who have been keeping score, set.mm is up to 74 theorems from the Metamath 100 list. iset.mm on the other hand has been stuck at one (which is induction over natural numbers) for some time (despite much progress in constructing real numbers, sequence convergence, existence of square

Re: [Metamath] does "standard" theory assume |- -. +oo e. CC ?

On 1/5/22 11:54 AM, Glauco wrote: 1. the "standard" theory works perfectly fine without assuming plus infinity not being a complex number. Thus, |- -. +oo e. CC should NOT be a theorem in set.m As far as I could tell from a quick glance, everything would work if +oo is defined to be _i and

Re: [Metamath] Pull requests now check for rewrapping

er commits that calls scripts/rewrap and commits the result (with a bot credential, this requires some setup but it's not too hard last I checked). On Sun, Jan 2, 2022 at 3:22 PM Jim Kingdon <mailto:king...@panix.com>> wrote: Probably most people who have contributed to metamath have

[Metamath] Pull requests now check for rewrapping

Probably most people who have contributed to metamath have noticed the way that our rewrapping scripts and practices tend to lead to things like generating diffs in your pull request which are unrelated to the change you are making (because the last person didn't rewrap and you did,

Re: [Metamath] Re: Metamath distribution

No, because CI runs scripts/verify --top_date_skip which includes VERIFY MARKUP * / TOP_DATE_SKIP On 1/2/22 4:42 AM, Glauco wrote: Running a "verify markup" with a recent set.mm I'm getting a There is no "Version of " comment at the top of the file warning. It looks like the date is not at

Re: [Metamath] Updating the website

What part of the website? Some parts are definitely already open for pull request - for example https://github.com/metamath/set.mm/blob/develop/mmset.raw.html - but if you are thinking of something which isn't in git yet, I believe David Wheeler has access (and, I presume, a plan to get it

Re: [Metamath] Discussion: Approving changes to the set.mm database

On 12/14/21 9:47 AM, Mario Carneiro wrote: Of late I haven't had much time to devote to PR reviews though, so it will need more than just me if we want to keep the queue flowing. I think Jim Kingdon should take point on iset.mm <http://iset.mm> maintenance, and others should sp

Re: [Metamath] Re: Discussion: Approving changes to the set.mm database

It is a fair question and to a fair extent I think we can rely on the judgement of the person merging it about how long to wait (subject to the more black and white rules about passing the automated checks and - I suppose this is black and white except for mathboxes - having at least one

Re: [Metamath] Discussion: Approving changes to the set.mm database

Seems like a good place to start. The only real caveat I'd add is that one of the subtle things which Norm was doing which might not even have been fully noticeable is that he had a bias towards "merge this now" which I think generally served us well. Now sometimes that was combined with

Re: [Metamath] Congrats to Scott Fenton on surreal work

Oooh, awesome. For those who haven't been following, the result is "given two sets of surreals such that one comes completely before the other, there is a surreal lying strictly between the two. Furthermore, there is an upper bound on the birthday of that surreal." My mental model of the

  1   2   >