Re: [Metamath] Suffix d for theorems not in "deduction form"

On Mon, Nov 29, 2021 at 3:43 PM Benoit wrote: > As for the questions raised by David: in my opinion, the best term to > refer to hypotheses-free theorems is "hypotheses-free theorem", or "theorem > with no hypotheses" (in other words, no special term is needed; you can add > that it is also

Re: [Metamath] Suffix d for theorems not in "deduction form"

Late to the party, but I agree with Norm & Jim: Deductions can have 0 hypotheses, and while there is a naming conflict between whether the xxxd theorem is the result of "deductionizing" (add "ph ->" to all hyps and conclusion) the corresponding xxx or xxxi theorem, this is a rare situation. You

Re: [Metamath] StackExchange proposed site ProofAssistants

n't be too successful, but I'm signed up for the new site and we'll see how it goes. Mario Carneiro On Thu, Nov 25, 2021 at 11:24 PM Jim Kingdon wrote: > On 11/25/21 10:17 AM, EricGT wrote: > > Andrej Bauer has proposed the StackExchange site ProofAssistants > <https://area51.stackexch

Re: [Metamath] Excluding (/) from extensible structure to be a function

I want to add that df-struct is essentially a technical definition made so as to make efficient (linear time) the proofs of n-ary versions of strle3. It is not meant to stake any claim on what a structure "is", and for various reasons you might want to add or remove hypotheses relative to

Re: [Metamath] Excluding (/) from extensible structure to be a function

It's not excluding `(/)` from being an extensible structure, it is rather the opposite: it asserts that f with (/) removed is a function. It is impossible for any set containing (/) to be a function, because a function is a set of ordered pairs and (/) is not an ordered pair. So this is being

Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM)

on the web. On Sat, Nov 13, 2021 at 6:12 PM Mario Carneiro wrote: > > > On Sat, Nov 13, 2021 at 12:07 PM Antony Bartlett wrote: > >> Thanks to Github user @jcaesar, Metamath does now run in browser here >> >> https://d1mtql0za68dbm.cloudfront.net/ >> >> (o

Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM)

On Sat, Nov 13, 2021 at 12:07 PM Antony Bartlett wrote: > Thanks to Github user @jcaesar, Metamath does now run in browser here > > https://d1mtql0za68dbm.cloudfront.net/ > > (of the browsers I've tried, Chrome, Firefox, and Edge work fine, Safari > does not. Also wont work on the official

Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request?

In lean/mathlib, the solution used is to have a bot make and self-apply formatting PRs (well, actually it's more like updating the discouraged file but the concept applies to any automatic code change). I think this is friendlier for contributors than having a CI check flag your PR if it did not

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

v 1, 2021 at 11:55 AM Mario Carneiro wrote: > Regarding the new axioms: > > ax-abidc should be derivable from df-cleq (it should not be expressible > prior to this anyway, since A = B as a wff is not introduced until then). > Specifically: > > |- ( x = y -> ( y e.c A <->

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

Regarding the new axioms: ax-abidc should be derivable from df-cleq (it should not be expressible prior to this anyway, since A = B as a wff is not introduced until then). Specifically: |- ( x = y -> ( y e.c A <-> x e.c A ) ) |- ( y e.c A <-> [ y / x ] x e.c A ) |- ( y e.c A <-> y e.c { x | x

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Fri, Oct 29, 2021 at 2:30 PM Benoit wrote: > Mario: why, when you encounter a dummy class variable in the original > proof, don't you simply use a dummy setvar variable in place of it ? > That works too. Any expression that doesn't use class variables will work there. -- You received this

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

. On Fri, Oct 29, 2021 at 2:16 PM Mario Carneiro wrote: > > > On Fri, Oct 29, 2021 at 2:06 PM Norman Megill wrote: > >> What is ax-9c? It isn't an axiom in set.mm. > > > I've referenced it a few times in this conversation as a hypothetical > axiom extending ax-9 to cl

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Fri, Oct 29, 2021 at 2:06 PM Norman Megill wrote: > What is ax-9c? It isn't an axiom in set.mm. I've referenced it a few times in this conversation as a hypothetical axiom extending ax-9 to classes: x = y -> (x e. A -> y e. A). -- You received this message because you are subscribed to

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

Here's a sketch of the proof of conservativity of the class axioms. We remove them one at a time: first removing df-clel, then df-cleq, and finally ax-9c, df-clab and class all at once. Assume that the base theory S has enough to move equivalences through the logical connectives, and prove alpha

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Thu, Oct 28, 2021 at 7:19 PM Norman Megill wrote: > So the scheme x e. A is equivalent i.e. represents the same set of object > language wffs as the scheme [ x / y ] ph. > > ZFC+classes is exactly equivalent to ZFC in terms of the object-language > theorems it can prove. This is true, but a

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Wed, Oct 27, 2021 at 7:22 PM Norman Megill wrote: > In fact, ZFC + classes is a conservative extension in exactly the same way >> that NBG is, >> > > There is a fundamental difference. > > NBG has global choice, which has no ZFC equivalent. From the wikip page > on NBG, "the axiom of global

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Wed, Oct 27, 2021 at 11:40 AM Norman Megill wrote: > I discuss the issue of whether to call df-clab,cleq,clel axioms at the end > of the http://us.metamath.org/mpeuni/mmset.html#class section. Most > authors call them definitions, and my feeling is that calling them axioms > would be

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

Personally, I think the easiest way to address the issues is to make df-cleq, df-clab, df-clel axioms instead of "definitions". They are not definitions according to the definition checker algorithm, they are not conservative as observed in this thread, and they significantly complicate the

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

Well, like I said we first need to know that x e. A acts like a regular predicate, which in particular implies your theorem about the equivalence of the distinct and bundled cases. I believe that the strengthened ax-9 I mentioned (i.e. x = y -> (x e. A -> y e. A)) also implies this fact. set.mm is

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Wed, Oct 27, 2021 at 5:26 AM 'ookami' via Metamath < metamath@googlegroups.com> wrote: > I am not sure whether the complexity is a problem of operator overloading > only. Let me explain why: > > At the moment of df-cleq the term x e. A is still undefined, and can mean > anything. The term x

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

The stance I take in MM0 is that df-cleq is a definition, but it is defining class equality in terms of set equality. The suspicious thing that set.mm is doing is asserting that the two are the same by definition, implicitly by representing x = y as wceq (cv x) (cv y). If you have two equalities,

Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM)

Running in the browser is one of the goals for the (budding) metamath-knife community verifier / proof assistant: https://github.com/david-a-wheeler/metamath-knife/ . It's written in Rust, and I have had success in the past compiling Rust projects to WASM, but the web frontend for metamath-knife

Re: [Metamath] Reopen: How to define 'Not Free'

> (a) There is more friction in the transition between hb* and nf* style theorems Could you elaborate on this? I would assume that once you have nfi and nfri you can easily convert between the two styles. On Sun, Sep 12, 2021 at 9:16 AM 'ookami' via Metamath < metamath@googlegroups.com> wrote:

Re: [Metamath] New community verifier?

On Tue, Aug 17, 2021 at 4:46 AM Thierry Arnoux wrote: > Concerning the parsing of $j comments, I've implemented it in two steps: > >- a first step, which is completely agnostic of the usage, and for >which I've followed the Metamath book, chapter 4.4.3 : Additional >Information

Re: [Metamath] New community verifier?

On Mon, Aug 16, 2021 at 11:56 PM Thierry Arnoux wrote: > Hi Mario, > > Indeed set.mm's grammar is unambiguous, and as you write, these are not > true ambiguities, but just prefixes which my initial naive implementation > did not parse correctly. The concept of "garden-path" was new to me, but >

Re: [Metamath] New community verifier?

It sounds like the algorithm is quite similar to the LRParser implementation (that I have called "KLR" before on the list). It is almost an LR(0) parse, but then set.mm has certain "ambiguities" (not really the right word, more like a garden path sentence) that require the grammar to have some

Re: [Metamath] New community verifier?

Exciting news! Where did you get the grammar parsing algorithm from? Is it based on LRParser, a backtracking parser algorithm, or something tailored for set.mm? Regarding the questions, my own opinions are: (1) Lots of bits of a metamath proof assistant can be separated into crates and put on

Re: [Metamath] Wondering what is the minimum syntax needed for everything?

Yes, it suffices to have nand, forall and elementhood to get a complete set of term constructors for ZFC. However, you can ask the same question about the axiom systems and I think here the answer is less clear. For example, although the sheffer stroke is complete for propositional logic using a

Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory

On Mon, Jun 14, 2021 at 3:43 AM Kunhao Zheng wrote: > One more question somehow irrelevant: While I was jumping around > different pages of metamath, I found some of definitions (df-mulr) is like > .r = Slot 3, do you know what it means by Slot? > That has to do with the encoding of

Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :)

On Wed, Jun 9, 2021 at 11:21 AM Jon P wrote: > There have been a couple of AI systems, gpt-f > and Holophrasm > , built on metamath whose aim is to > generate proofs. Are there more I’m not aware of? > Not that I know of, at

Re: value of documenting error messages?

Rust error codes are not sequential, presumably because some old errors are no longer applicable and new errors get new numbers. It seems to me that it should be possible to just allocate numbers so that if the error changes more than cosmetically then it gets a new number, and thus the error code

Re: GHC and the future of Freenode

, but I thought I should balance out the Zulip downvotes with some positive experiences. (Also, I would definitely be more likely to participate on a haskell Zulip than an IRC or Matrix instance, FWIW.) Mario Carneiro On Wed, May 19, 2021 at 9:58 PM Carter Schonwald wrote: > I definitely f

Re: [Metamath] Re: Metamath verifier in Lean 4

On Sun, May 9, 2021 at 12:24 PM Benoit wrote: > On Friday, May 7, 2021 at 5:20:47 PM UTC+2 di@gmail.com wrote: > >> (and if it is to eventually be verified it is probably best to keep it >> bare bones) >> > > Isn't it possible to verify only the core of a given program ? > Yes, although you

Re: [Metamath] Re: Metamath verifier in Lean 4

On Sun, May 9, 2021 at 10:18 AM vvs wrote: > it has quite competitive performance. It's not quite as impressive as >> smm3, but it can compile set.mm in 10-12 seconds so I'm quite happy with >> it. >> > > Benchmarking is a murky business, it pretty much depends on the system. > I've got 39.5s

Re: [Metamath] Re: Metamath verifier in Lean 4

Could you update the name of the verifier to "mm-lean4"? "Metamath.lean" is a bit generic (file names in lean 4 have to follow some package-oriented naming conventions like in java). On Sat, May 8, 2021 at 7:38 PM Norman Megill wrote: > If what you mean is the link in the list of verifiers, I

Re: [Metamath] Re: Metamath verifier in Lean 4

It's still basically in one file, although now that file is https://github.com/digama0/mm-lean4/blob/master/Metamath/Verify.lean . Probably better for the metamath site to point to the repo https://github.com/digama0/mm-lean4/ instead though. The other file is WIP at the moment, but it now

[Metamath] Metamath verifier in Lean 4

handle compressed and normal proofs, and all the official MM stuff except for $[ $] import statements. https://github.com/digama0/mm-lean4/blob/master/Metamath.lean Mario Carneiro -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubs

Re: [Metamath] Metamath verifier in Zig

Exciting! How is the performance? I would guess that a Zig verifier could compete with the best. On Wed, May 5, 2021 at 10:51 AM Marnix Klooster wrote: > Hello all, > > In case anyone is interested, I'm not sure but I don't think I announced > this earlier: Since almost a year I've been working

Re: [Metamath] Re: [Question on Formalization] How can I write number in base other than 10

You can use `reverse` in order to reverse the word, by the way, rather than baking the index arithmetic into the `_b` function. On Sat, May 1, 2021 at 10:01 AM 'Alexander van der Vekens' via Metamath < metamath@googlegroups.com> wrote: > On Saturday, April 24, 2021 at 11:01:09 PM UTC+2 Glauco

Re: [Metamath] Re: [Question on Formalization] How can I write number in base other than 10

I also want to mention that Jim Kingdon's suggestion of simply using ((3 · ((3 · 2) + 1)) + 2) has official support in set.mm, in that for every dec* theorem there is a corresponding num* theorem about the generalized base representation of numbers. As Norm says, this suite of theorems was used

Re: [Metamath] How-Tos and best practices

I think such a page would fit best as an additional HTML page on the metamath web site, which could be developed on github next to the other web pages. (I don't have any particular suggestions for what to put on the page at the moment but I'd be happy to review or extend it if someone wants to

Re: [Metamath] The |`t operator could be used not only for topologies

On Sun, Apr 18, 2021 at 8:05 AM Benoit wrote: > Why not the hypothesis-free form > |- ( ( J e. V /\ A C_ U. J ) -> A = U. ( J |`t A ) ) > That is, you inline the definition of X. Theorems using this result might > be a bit longer, but the statement looks leaner. > That's a useful theorem,

Re: [Metamath] Informal proof of Weak Deduction Theorem vs dedt

F((A ∧ F) ∨ (B ∧ ¬ F)) The first two hypotheses are clearly instances of the substitution metatheorem, and the third assumption is a hypothesis: |- F(B) is provable by assumption, so |- F((A ∧ F) ∨ (B ∧ ¬ F)) and hence |- G((A ∧ F) ∨ (B ∧ ¬ F)) as desired. Mario Carneiro -- You received this m

Re: [Metamath] Translation to/from other languages

ter/mm0-lean/mm0/set/post.lean#L539-L540 . Mario Carneiro On Thu, Feb 11, 2021 at 11:53 PM mrper...@gmail.com wrote: > > I'm just curious: has there ever been any serious effort to make a > translator between Metamath and another unrelated proof language(such as > HOL Light,

Re: [Metamath] Recent partial unbundling of ax-7, ax-8, ax-9

Does this affect the statement of any axioms? This may affect the MM -> MM0 translation, which is assuming that ax-7 is stated with no DV conditions. On Wed, Dec 23, 2020 at 5:48 PM Benoit wrote: > Hi everyone, > I recently added to set.mm some weakenings of ax-7, ax-8, ax-9 in order > to

Re: [Metamath] Re: Recommending proof length limits

I also think that 200 is an okay "soft maximum". I've definitely got some theorems larger than that, some a lot larger, and the MM0 project is going to generate some really large proofs (the largest so far is 673 steps but that's still mostly handwritten; the autogenerated proofs are going to be

Re: [Metamath] Calling Stefan O'Rear: Are you still around? Are you maintaining smetamath-rs (smm3)?

On Tue, Dec 8, 2020 at 10:51 PM David A. Wheeler wrote: > For example, the current code uses the deprecated “try!” macro. Current > Rust compiler & documentation urge use of the easier “?” construct, and I > expect “try!” to stop being supported (“try” is becoming a keyword with > different

Re: [Metamath] Re: New community verifier?

On Sat, Nov 28, 2020 at 4:04 AM savask wrote: > I'm a bit late to the discussion, but do I understand correctly that this > new community verifier is supposed to be a spin-off to MM0/MM1 project? In > particular, MM1 code base will be the starting point, proofs won't look > like mmj2's proof

Re: [Metamath] Re: New community verifier?

It's certainly possible to have pages for terms and definitions, but I don't have much to show for them beyond what's already on the index page. If I can figure out how to do pretty printing with embedded links, I can also link all the uses of a symbol so that you can click on a "+" anywhere to go

Re: [Metamath] Re: New community verifier?

On Fri, Nov 27, 2020 at 1:17 AM David A. Wheeler wrote: > On November 27, 2020 12:14:09 AM EST, Mario Carneiro > wrote: > step folding is also an option although I don't know how to make > >that not annoying. > > If it can be done easily without JavaScript, you should do

Re: [Metamath] Re: New community verifier?

ssential components like a nav bar or something like it. The current design is pleasantly minimalistic but maybe some important elements are missing, so some votes on the most pressing issues would help. Mario On Wed, Nov 25, 2020 at 11:09 AM Mario Carneiro wrote: > > > On Wed, Nov 25,

Re: [Metamath] Re: New community verifier?

On Wed, Nov 25, 2020 at 8:58 AM Glauco wrote: > Hi Mario, > > here > https://groups.google.com/g/metamath/c/raGj9fO6U2I/m/2tQseJ3CBwAJ > you show peano.mm1 in VSCode and you write > "The basic idea is that MM1 is a scripting language for assembling MM0 > proofs and statements. It's untrusted,

Re: [Metamath] New community verifier?

On Sun, Nov 22, 2020 at 5:00 PM David A. Wheeler wrote: > > > On Nov 21, 2020, at 10:15 PM, Mario Carneiro wrote: > > > > On Sat, Nov 21, 2020 at 8:42 PM David A. Wheeler > wrote: > >> Providing a Scheme-like interface is a reasonable approach. It’s easy

Re: [Metamath] Re: New community verifier?

On Sun, Nov 22, 2020 at 12:39 PM Glauco wrote: > Please, let me know what's the best environment to set up to contribute to > the new tool: > > - VSCode + RUST seems to be the candidate, right? (if it were possible to > have a portable environment it would be a plus) > > - at least Windows +

Re: [Metamath] New community verifier?

On Sat, Nov 21, 2020 at 11:52 PM Jim Kingdon wrote: > Mario Carneiro wrote: > > > If there is enough interest from others that I'm not the only one on the > project, I don't mind taking the lead here. > > I suppose this is the time to express interest or lack of inter

Re: [Metamath] New community verifier?

On Sat, Nov 21, 2020 at 8:42 PM David A. Wheeler wrote: > Providing a Scheme-like interface is a reasonable approach. It’s easy to > implement & provides a lot of flexibility. The big problem is that MANY > people hate their syntax, e.g., “lots of irritating silly parentheses”. As > you know, I

Re: [Metamath] New community verifier?

On Sat, Nov 21, 2020 at 8:11 PM David A. Wheeler wrote: > > > > On Nov 21, 2020, at 6:22 PM, Mario Carneiro wrote: > > If there is enough interest from others that I'm not the only one on the > project, I don't mind taking the lead here. If it incorporates comm

Re: [Metamath] Re: New community verifier?

On Sat, Nov 21, 2020 at 7:10 PM vvs wrote: > Rust isn't a functional programming language, but the first implementation >> of MM1 was in Haskell and it had some memory usage and speed issues that >> would have required some significant concessions to imperative style to fix. >> > > Too bad for

Re: [Metamath] Re: New community verifier?

On Fri, Nov 20, 2020 at 10:22 PM Raph Levien wrote: > Regarding writing an editor. I agree it's a big task and hard to do right. > That said, it's also something I'm interested in. I know there's at least > one other editor project on Druid (not my own), and we also have interest > in unbundling

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

Mainly I would like to remove mmverify.py and mmj2 from the pipeline, which are far more expensive than the others for the same job. Currently we can't remove mmj2 because it's the only one with a definition checker but that does not cost 102 seconds to do by any stretch. And I notice that

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

Actually I've reposted this at https://groups.google.com/g/metamath/c/6fQ_GxnPAWI/m/wJ8wzDp3AQAJ; please direct future responses to that thread so we can keep this one to Travis -> GH Actions. On Fri, Nov 20, 2020 at 3:00 PM Mario Carneiro wrote: > The plan is to start a new "communi

[Metamath] New community verifier?

Relocated from https://groups.google.com/g/metamath/c/NMZA_JRkU4U/m/ccP9bXZlAQAJ: On Fri, Nov 20, 2020 at 9:37 AM Benoit wrote: > Mario, do you have some more detail about this project to write (I'm > quoting you from github) "a verifier that would satisfy all the constraints > of the CI system

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

I've been doing a significant amount of >> work on mm0-rs to turn it into just such a program for MM1, and it is nice >> to be able to have all the niceties of a normal programming language IDE >> like go to definition, find references and rename in addition to proof >>

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

not sure I want to go back to mmj2 at this rate. On Thu, Nov 19, 2020 at 3:46 PM Mario Carneiro wrote: > > > On Thu, Nov 19, 2020 at 3:41 PM David A. Wheeler > wrote: > >> >> > On Nov 19, 2020, at 3:26 PM, Mario Carneiro wrote: >> > This is why I say th

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

On Thu, Nov 19, 2020 at 3:41 PM David A. Wheeler wrote: > > > On Nov 19, 2020, at 3:26 PM, Mario Carneiro wrote: > > This is why I say that the nightlies are really a test case for the > verifiers - under no situation is the blame laid on the commit that pushed >

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

On Thu, Nov 19, 2020 at 1:47 AM Jim Kingdon wrote: > All sounds good, thanks for looking into this. > > I'd say that running everything on every pull request would be my > preference, and I don't think it takes that long to run (at least, it > hasn't on travis). Nightly is an option if we have

Re: [Metamath] Switching the set.mm repo from Travis CI to GitHub Actions (or something else)

> So I intend to move the Travis jobs to GitHub Actions *first*, while doing my best to isolate the jobs. We can then *separately* consider if we should split jobs into “nightly” and “per-commit” jobs, and how to split them, once we have confidence that the jobs have been correctly moved. It’ll be

Re: [Metamath] Relabeling ~dummylink

It is not hardcoded in mmj2, although it might be in the blacklist (which gets out of date relatively quickly anyway and knows how to handle it). Regarding the naming, I think it is a bit odd that a theorem called a1ii does not use ax-1. Then again, idi doesn't use id either. On Tue, Nov 10,

Re: [Metamath] Re: Verifying Disjoint Variable Restrictions

ables can map > to expressions both containing the same mandatory variable (see second > entry in this thread). > > On Thu, Oct 15, 2020 at 2:23 PM Mario Carneiro wrote: > >> Disjoint variables between dummy variables (variables that are used in >> the proof but not

Re: [Metamath] Re: Verifying Disjoint Variable Restrictions

ment nfdv /full > Statement 4708 is located on line 26073 of the file "set.mm". Its > statement > number for HTML pages is 1775. > "Apply the definition of not-free in a context. (Contributed by Mario >Carneiro, 11-Aug-2016.)" > 4708 nfdv $p |- (

Re: [Metamath] Simple substitution in Metamath

The theorem mp actually has 4 arguments. The first two are the substitutions, which are usually suppressed. That is, you first have to prove wff P, then wff Q, then |- P, then |- ( P -> Q ), and then theorem mp applies to derive |- Q. If you use metamath.exe, "show proof th1" will list only 5

Re: [Metamath] Re: Resources for newbies

On Thu, Sep 10, 2020 at 5:36 AM ginx wrote: > Also, thanks for the very detailed explanation Mario. After reading it, I > think I basically boiled it down to just two possibilities: Descartes Rule > of Signs, which as you stated should be doable, and the CS route. Though it > might require a lot

Re: [Metamath] Re: Resources for newbies

On Wed, Sep 9, 2020 at 5:58 PM Norman Megill wrote: > On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote: > >> Norm: >> >> Thanks for the reply, I’m definitely going to hang out around here more >> often. The 100 theorems is my ideal option, I was scheming the list >> provided and

Re: [Metamath] Going from AM-GM to AM-GM 3

On Tue, Sep 8, 2020 at 3:46 PM 'Stanislas Polu' via Metamath < metamath@googlegroups.com> wrote: > I was expecting to find something along the very broad lines of: > > ``` > ( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( ( CCfld gsum > { { 1 , A } , { 1 , B } } ) + ( CCfld gsum { { 1 ,

Re: [Metamath] Re: metamath.exe - added "/extract" to "write source"

The Metamath -> MM0 importer already contains a feature for selecting which target theorems you want, so it has the same effect as using /extract on the source database first and then importing it. I've been using numbers for example theorems like dirith or pnt in my talks. I wonder what is the

Re: [Metamath] Re: Matrix indexing start

Regarding the Laplace expansion more specifically: I assume that a determinant is defined over matrices M : A x A -> R, where A is a finite (unordered) set. Suppose we wish to perform cofactor expansion along row i e. A. The j'th cofactor (where j e. A) is given by the elements of M on (A\{i}) x

Re: [Metamath] Re: Matrix indexing start

I haven't stopped anything, but my time is finite, and I have a dissertation to finish. I'm pretty active on the Lean Zulip chat ( https://leanprover.zulipchat.com/) if you want to say hi or show support for metamath, since right now I'm the token representative. Mario On Thu, Sep 3, 2020 at

Re: [Metamath] Re: Matrix indexing start

Wikipedia has a list: https://en.wikipedia.org/wiki/Comparison_of_programming_languages_%28array%29#Array_system_cross-reference_list On Wed, Sep 2, 2020 at 11:53 PM Mario Carneiro wrote: > Don't forget Fortran arrays, which have user-configurable ordering (!) but > by default start

Re: [Metamath] Re: Matrix indexing start

Don't forget Fortran arrays, which have user-configurable ordering (!) but by default start with 1. On Wed, Sep 2, 2020 at 11:11 PM David A. Wheeler wrote: > I think there has been a slow march from one-based indexing to zero based > indexing in computing. > > Many systems designed two decades

Re: [Metamath] Re: Matrix indexing start

No, I'm not proposing a translation to or from lean. (Well, I am looking into it, but that's an entirely separate discussion.) My purpose was only to draw a parallel to another theorem prover library driven in large part by mathematicians, to send the message that this is a minor variation that is

Re: [Metamath] Re: Matrix indexing start

In Coq and Lean, the structure of inductive types, specifically the peano natural numbers starting at 0, *strongly* prefers 0-based indexing. The difference is stark enough that it's not really ever a discussion. You can do induction on nat, you can't do induction on positive nat (at least the

Re: [Metamath] Re: Matrix indexing start

e expansion of the determinant (just one level of expansion, not recursive) requires a choice of row to expand over (which is an element of the index set), and then it's an unordered finite sum. No integers needed. Mario > > Le 2 sept. 2020 à 18:54, Mario Carneiro a écrit : > >  >

Re: [Metamath] Re: Matrix indexing start

dentify with Words (` Word X `, which can be input as ` <" >> A B C "> ` ) if that set is of the form ` ( 0 ..^ N ) ` ... >> >> _ >> Thierry >> >> >> On 02/09/2020 15:15, Mario Carneiro wrote: >> >> I will reiterate my suggestion

Re: [Metamath] Re: Matrix indexing start

I will reiterate my suggestion to use finite sets for indexing when possible, which sidesteps the question, but while I would like to defer to Norm here, I really think a lack of consistency is going to cause actual problems in this area. What is the definition of a matrix multiplied by a vector?

Re: [Metamath] Re: Overloading symbol names

Well, those are counterexamples to the claim that every syntax constructor uses a unique symbol, but they are not counterexamples to the claim that the mapping from ascii token to HTML display is injective, and until now this property has been maintained, in some cases even when this goes against

Re: [Metamath] Re: Matrix indexing start

My vote is also in favor of starting with 0, or even better, doing everything over generic finite sets when possible and falling back on ( 0 ..^ N ). I realize that close correspondence with papers is considered important here but mathematicians write for their own ease. In a math paper, you can

Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements.

Found it: https://groups.google.com/g/metamath/c/2AW7T3d2YiQ/m/iSN7g87t3ikJ On Tue, Aug 11, 2020 at 3:48 PM Mario Carneiro wrote: > This fact was being deliberately not exploited, for reasons that I forget, > possibly involving type hygiene or something. I think Norm made the call on >

Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements.

This fact was being deliberately not exploited, for reasons that I forget, possibly involving type hygiene or something. I think Norm made the call on that so perhaps he can recall better. Mario On Tue, Aug 11, 2020 at 2:20 PM 'Alexander van der Vekens' via Metamath < metamath@googlegroups.com>

[isabelle-dev] Debugging help: Hacking the kernel for proof export

(I'm posting this to isabelle-dev since it's a very internal technical question that probably won't be of interest to end users.) So I've managed to successfully modify the kernel to support better proof traces, with ~0 performance impact, but while processing HOL I hit an error in Extraction.thy

Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI?

You don't need to call it a "conditional formal proof", it's a proof of the asymptotic ternary goldbach theorem, which is a famous result by Vinogradov (https://en.wikipedia.org/wiki/Vinogradov%27s_theorem). It is true that Helfgott improved this but it's essentially the same method, only with

Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI?

Helfgott's main paper says that the paper proof covers C >= 10^27, so numerical verification of ternary Goldbach is required up to 10^27. However, according to the first page of https://arxiv.org/pdf/1305.3062.pdf (the reference for the computation of the low part), to get this bound it suffices

Re: [Metamath] Re: CICM 2020: Metamath Zero talk

On Wed, Aug 5, 2020 at 4:09 AM Jon P wrote: > Awesome Mario, thanks for the response, it takes me a few days to respond > because I have to think a lot ha ha. > > I can see how fully symbolic proofs are better. I can also see how you > arrived at this place if separation logic has been

Re: [Metamath] Re: CICM 2020: Metamath Zero talk

On Sun, Aug 2, 2020 at 11:38 AM Jon P wrote: > Thanks so much for your nice response Mario. I think the work you’re doing > is really awesome and I’m very thankful that you would take your time to > explain things to me. I feel similarly with everyone else in this > community, I’m so impressed

Re: [Metamath] Re: CICM 2020: Metamath Zero talk

On Fri, Jul 31, 2020 at 3:55 PM Jon P wrote: > > Hi Mario, > > Very nice talk, thank you for posting it. > > Is it ok to ask some basic questions? It is a really nice project you are > doing and I would love to understand it, however I am afraid I am not so > strong in all this stuff. Feel free

Re: [Metamath] CICM 2020: Metamath Zero talk

Leaners are used to not thinking about axiom usage at all; basically all of mathlib uses all three axioms and this system is basically equivalent to ZFC + countable inaccessible cardinals, so it is quite compatible with set.mm foundations. Mario > > On Wed, Jul 29, 2020 at 10:11 AM Ma

[Metamath] CICM 2020: Metamath Zero talk

. You can still ask questions here if you want.) Mario Carneiro -- 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.co

Re: [Metamath] Introduction to Sophize

On Tue, Jul 14, 2020 at 11:20 AM Abhishek Chugh wrote: > > I believe the only reason it is traditionally lacking, compared to other > proof assistants, is lack of concerted effort in that direction. > I see. From what I understand, Metamath is run mostly by volunteers as a > hobby and perhaps

Re: [Metamath] Introduction to Sophize

On Tue, Jul 14, 2020 at 9:06 AM Abhishek Chugh wrote: > I would also like to understand how the community feels about automated > proof generation. From what I read in some academic papers - lack of > automation seems to be an often highlighted shortcoming of Metamath > compared to other proof

Re: [Metamath] OpenAI search tool for set.mm theorems

A minor recommendation, but perhaps instead of "." and ".*", you could use "?" and "$", which matches the use in the metamath search command? (Technically "?" only matches one character tokens in metamath search but I think your version is more useful.) Mario On Wed, Jul 8, 2020 at 2:39 PM

[Metamath] MM0 -> MM translation challenges

. Many of the points above also apply to MM -> MM translations, for example type guards and alignment also occur when translating peano.mm to set.mm or hol.mm to set.mm. It would be nice if we had a good story around interpreting MM databases into abstract (set-theoretic?) models and from

<    1   2   3   4   5   >