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

On Mon, Apr 27, 2020 at 7:35 AM Norman Megill wrote: > On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote: > ... > >> >> I know, and this is a bigger issue for set.mm than in the mm0 databases >> because these are smaller and more purpose driven. O

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

> _ > Thierry > > > Le 27 avr. 2020 à 11:44, Mario Carneiro a écrit : > >  > I think there is a unicode symbol for symmetric difference that is a white > upward pointing triangle (U+25B3 △), not an upper case Delta (which looks a > bit different due to weight chang

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

On Sun, Apr 26, 2020 at 9:16 PM David A. Wheeler wrote: > I think formalization of ASCII is a cool idea, and I agree that > '^' (and so on) would be *MUCH* better notation than _^ (and so on). > If nothing else, the '...' notation is *widely* used to represent a single > character, > and we

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

I think there is a unicode symbol for symmetric difference that is a white upward pointing triangle (U+25B3 △), not an upper case Delta (which looks a bit different due to weight changes along the glyph). On Sun, Apr 26, 2020 at 8:19 PM Thierry Arnoux wrote: > Hi all, > > I've been aligning

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

Heh, beat me by 5 seconds. Indeed, I meant 94. On Sun, Apr 26, 2020 at 6:55 PM heiphohmia via Metamath < metamath@googlegroups.com> wrote: > Maybe this is just displaying my ignorance, but decimal 97 is ASCII 'a'. > Perhaps you mean't 94, which corresponds to the caret (i.e. '^'

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

> Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not > "concat"); > By the way, I would like to reserve the notation '^' for the number 97, in preparation for possible formalization of ASCII. (In MM0 I'm using _char but 'char' is less likely to have overlapping usage.)

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

On Sun, Apr 26, 2020 at 17:31:09 +0200 (CEST) fl wrote: > Dijkstra's argument doesn't seem to apply to our problem. He is dealing > with finding a good convention to speak of a sequence of natural numbers > using <= or <. It is not at all our problem. We don't use order relations > to speak of a

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

FWIW I agree with Benoit and Alexander (and Dijkstra) on both counts. :) On Sun, Apr 26, 2020 at 4:23 AM Benoit wrote: > Like Alexander, I agree that word indices start at 0... like natural > numbers ;-) > > On Sunday, April 26, 2020 at 8:49:01 AM UTC+2, Alexander van der Vekens > wrote: >> >>

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

I was thinking the same thing, every integer is even or odd is a good example of XOR but I wouldn't recommend it for most uses (and even for nneo we will probably want the iff version because it has more theorems about it). On Sat, Apr 25, 2020 at 7:39 PM Jim Kingdon wrote: > > Thinking of it

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

I like the idea of using ++ for concatenation, particularly in ascii notation, since I don't want to try to reproduce a frown symbol in ascii. I think the most common symbol for this is adjacency though. Mario On Fri, Apr 24, 2020 at 6:19 PM Norman Megill wrote: > > 1. I have no strong opinion

Re: [Metamath] How can I find the dependencies at the Table of Contents level?

We do not make any serious attempt to make the dependency structure nonlinear, so every later section can refer to any previous section. Between sections and parts this is less common simply because the subject matters are different, but there are no hard rules there. On Mon, Apr 13, 2020 at 2:41

Re: [Metamath] Re: About Metamath zero (mm0)

On Sat, Apr 4, 2020 at 3:14 AM Olivier Binda wrote: > I guess that the restriction on id is this way so that we can do nice > stuff with notations (mostly with numbers). > > For example, at some point, I plan to allow users to write 1283 and to > have that (maybe in a preprocessing step) turned

Re: [Metamath] Re: About Metamath zero (mm0)

On Fri, Apr 3, 2020 at 12:12 PM Olivier Binda wrote: > So far, I have only changed c1 into 1 (same for c2, c3, c4, c5, c6, c7, > c8, c10). Which requires > to replace every instance of "c1" in the mmu and mm0 files with "1" (some > work, but not very hard) > Note that "1" is not a valid mm0

Re: [Metamath] Metamath as a medical tool

This approach sounds like "expert systems" ( https://en.wikipedia.org/wiki/Expert_system) from 80's AI. My understanding is that it's more or less discredited these days, and machine learning systems have little to no resemblance to expert systems. That is not to say that ML is necessarily better,

Re: [Metamath] Metamath as a medical tool

I don't see how this would be workable. Medical information is not logical deduction, and there is very little logical deduction involved. It is all about statistics, and a proof assistant is not the best way to organize that data. I think a more fruitful use of proof assistants in this space is

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

I think the other posters have covered my thoughts on the matter already, so I won't add much, but I did want to mention that regarding machine learning to generate short proofs, I think it is extremely unlikely that the proofs that are generated are going to be harder to understand than the

Re: [Metamath] Problem launching mmj2

Where did you find those build instructions? I have to admit it's a bit out of my depth, and I haven't touched this in a while. I usually use an ant build, in the build.xml file. You may be able to find the commands you need there. On Mon, Mar 23, 2020 at 5:05 AM Benoit wrote: > Not sure I did

Re: [Metamath] Problem launching mmj2

You have to have the .java files on your computer, inside the org/json directory. "git submodule" should put the files in the right place. On Mon, Mar 23, 2020 at 4:44 AM Benoit wrote: > I think it is used as a submodule, meaning that it gets compiled from >> source together with the rest of

Re: [Metamath] Problem launching mmj2

I think it is used as a submodule, meaning that it gets compiled from source together with the rest of mmj2 and bundled into mmj2.jar. It is not an external jar file. Aren't there .deb downloads for earlier versions of the JDK? Mario On Mon, Mar 23, 2020 at 4:28 AM Benoit wrote: >

Re: [Metamath] Problem launching mmj2

I don't know anything about a bug in unify/reformat. Sometimes bad unify commands will throw up a console error and manifest in the UI as a unify that doesn't stop and has to be cancelled. If so, please show the error. Otherwise, I don't know what this could be, and I would be interested to hear

Re: [Metamath] Problem launching mmj2

That bug occurs when you try to use mmj2 on newer versions of the JDK. It has been fixed on master, but I don't think there has been a release with the bugfix. (Unfortunately the fix doesn't completely restore the original chunked undo behavior so you have to undo one character at a time now, but

Re: [Metamath] Second-order theory

On Mon, Mar 16, 2020 at 6:07 PM Ken Kubota wrote: > > Am 17.03.2020 um 01:17 schrieb Mario Carneiro : > > > > On Mon, Mar 16, 2020 at 4:55 PM Ken Kubota wrote: > >> >> Am 16.03.2020 um 23:42 schrieb Norman Megill : >> >> On Monday, March 1

Re: [Metamath] Second-order theory

On Mon, Mar 16, 2020 at 4:55 PM Ken Kubota wrote: > > Am 16.03.2020 um 23:42 schrieb Norman Megill : > > 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

Re: [Metamath] Second-order theory

This is not correct. The system called PA is a FOL axiomatization, not SOL. Second order PA is categorical (has at most one model, and exactly one if you think the natural numbers exist), while first order PA is not. The fifth axiom of PA is not an axiom, it is an axiom scheme, an infinite family

Re: [Metamath] Re: Formalizing IMO B2.1972

ental about > DVs (thanks for clarifying) and secondly about exhaustion of variable names > which somewhat hurts the user experience but I presume it's a minor point. > > -stan > > On Thu, Mar 12, 2020 at 10:20 AM Mario Carneiro wrote: > >> This is a minor design decision in

Re: [Metamath] Re: Formalizing IMO B2.1972

here are better >> strategies ? >> >> From the experience formalizing imo72b2, I think that when relying on >> natural deduction forms, hypotheses should favor quantifiers (stronger) >> while conclusions shouldn't (easier to work with). Going from a lemma >> wi

Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory?

You can't really do raw first order logic in metamath, you would need an infinite number of axioms (even for things like propositional logic). Metamath needs to be able to use schemes to define axiom systems, and to write those schemes you need some concession to higher order variables, although

Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory?

While it is not explicitly based on Väänänen's article, I should note that the Peano arithmetic formulation that I'm working on in peano.mm1 ( https://github.com/digama0/mm0/blob/master/examples/peano.mm1#L974-L977) is quite similar to this. It axiomatizes PA in much the same way as set.mm

Re: [Metamath] reinterpret ax-3

On Mon, Mar 9, 2020, 1:17 PM Benoit wrote: > > Regarding provability of bijust, it is intuitionistically provable with > the standard intuitionistic interpretations of -> and -. . It is an > instance of -. ((p -> p) -> -. (p -> p)), which is true because |- p -> p > is provable, and so from ((p

Re: [Metamath] reinterpret ax-3

If you actually want intuitionistic logic, you cannot get away with using just -> and -. as your basis. You have to add in /\ and \/ , but once you have that, you can just use dfbi1 as the definition (and df-bi is really just an obfuscated version of dfbi2 anyway, once you unfold the definition of

Re: [Metamath] reinterpret ax-3

On Sun, Mar 8, 2020 at 9:18 PM Mario Carneiro wrote: > If you actually want intuitionistic logic, you cannot get away with using > just -> and -. as your basis. You have to add in /\ and \/ , but once you > have that, you can just use dfbi1 as the definition > correction:

Re: [Metamath] reinterpret ax-3

It's not a conservative extension, as the intuitionistic logic development makes clear. Peirce's law ((p -> q) -> p) -> p is not provable from ax-1,2,mp but it is provable from ax-1,2,3,mp, even though there are no negations involved in the statement. By contrast, df-bi is a conservative extension

Re: [Metamath] Re: Formalizing IMO B2.1972

F ` x ) ) ) >> d7:d72,d71:eqeltrrd |- ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( >> abs ` ( F ` x ) ) e. ( abs " ( F " RR ) ) ) >> >> d10::simpr |- ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) /\ >> z = ( abs ` ( F ` x ) ) ) -> z =

Re: [Metamath] Re: Formalizing IMO B2.1972

::|- ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) =/= (/) ) > ``` > > Any idea on how to proceed with this? > > Thanks thanks! > > -stan > > On Thu, Mar 5, 2020 at 6:27 PM Mario Carneiro wrote: > >> There is a theorem specifically for that translati

Re: [Metamath] Re: Formalizing IMO B2.1972

/github.com/spolu/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65 > > One thing I'm quite dissatisfied with is the shape of `imo72b2lem.6`. I'd > much rather have the more natural/intuitive expression `|- ( ph -> A. x e. > RR ( abs ` ( F `x ) ) <_ 1 )` but I completely faile

Re: [Metamath] Re: Formalizing IMO B2.1972

Can't look right now, but you should search for a theorem of the form A = (/) <-> ( F " A ) = (/) . On Wed, Mar 4, 2020, 11:30 AM 'Stanislas Polu' via Metamath < metamath@googlegroups.com> wrote: > I'm now looking to prove that `( abs " ( F " RR ) ) =/= (/)` given `F : RR > --> RR`. From my

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

What I do: * Search the metamath table of contents for group homomorphisms, or failing that, groups or something topical. * Browse the section to see if it's there. Failing that: * Identify the relevant constant (in this case, GrpHom) * Use metamath's search tool to list all theorems containing

Re: [Metamath] Re: About Metamath zero (mm0)

On Sun, Mar 1, 2020 at 1:07 PM Olivier Binda wrote: > Quite satisfying but this raises a question : > The parser of mm0 is great at parsing stuff with binary operators and > turns things like > 1 + 2 into > a tree of the form > + { > 1 > 2 > } > Yet Metamath was designed around co, that

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?

discussed. > > > > > *Ken Kubota* > doi.org/10./100 > > > > Am 24.02.2020 um 22:30 schrieb Mario Carneiro : > > > > On Mon, Feb 24, 2020 at 12:55 PM Ken Kubota wrote: > >> My knowledge about Metamath is limi

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 Mon, Feb 24, 2020 at 12:55 PM Ken Kubota wrote: > My knowledge about Metamath is limited, but I believe that Mario is > correct in that the form of reasoning resembles that of a Hilbert-style > system. > > However, my perspective is different since my intention is to find the > natural

Re: [Metamath] Metamath Zulip

I could create a zulip chat room, but based on experience with the gitter room it seems like the demand isn't really there. Then again, lean zulip has been much more successful than lean gitter, and the threading model works much better for multiple overlapping conversations than unstructured IRC

Re: [Metamath] Re: About Metamath zero (mm0)

On Sun, Feb 23, 2020 at 2:14 AM Olivier Binda wrote: > Hi Mario > Many thanks for the answer > >> >> You probably know this already, but I've been focusing my user interface >> stuff on the .mm1 file format. The mmu file format currently doesn't even >> have a syntax highlighter, although it

Re: [Metamath] Re: Where is the fashionable mathematics?

On Sat, Feb 22, 2020 at 7:22 PM Norman Megill wrote: > 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

Re: [Metamath] Re: About Metamath zero (mm0)

On Sat, Feb 22, 2020 at 12:47 PM Olivier Binda wrote: > Apparently, it is quite easy to write plugins for intellij idea. > > I just tried and one day later, I had written lexers and primary parsers > for the mm0 and mmu files, with JFlex and GrammarKit (and thanks to mario's > answers and the

Re: [Metamath] Re: Riemann-zeta ratio-test rabbit-hole

Once you prove that the sum converges everywhere on a dense set (namely the whole plane except 1 + 2 n pi i or something like that), uniqueness off the poles is trivial because real/complex sums are unique. Uniqueness at the poles is guaranteed by continuous extension in a hausdorff space. You

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

Job 160 is done, after 99.7 hours of CPU time. (I think it was done yesterday, but I got confused with the state of the process and didn't want to mess with it.) It found one lemma, saving 5 bytes. Mario On Thu, Feb 20, 2020 at 7:28 PM Norman Megill wrote: > All jobs from 101 to 158 have

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

/WmovUJiKBAAJ > > Norm > > On Tuesday, February 18, 2020 at 1:53:13 PM UTC-5, Mario Carneiro wrote: >> >> 158 is done (after 62.8 hours), starting 159. 160 is still running. >> >> On Sun, Feb 16, 2020 at 8:13 AM Norman Megill wrote: >> >>> Th

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

, 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 message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this g

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

156 is done (after 31.8 hours), starting 158. 160 is still running. On Sat, Feb 15, 2020 at 7:18 PM Norman Megill wrote: > 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 >> >

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

It may minimize with the statement, then later minimize the statement away. I wouldn't be worried unless "idi" appears in the minimized proof. On Fri, Feb 14, 2020 at 6:27 PM David A. Wheeler wrote: > I just took a quick look at job144.log as posted on: > https://dwheeler.com/temp/job144.log >

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

123 and 124 completed, in about 12 and 13 hours respectively. I'm running 156 and 160 now. Mario On Fri, Feb 14, 2020 at 7:27 AM David A. Wheeler wrote: > On Thu, 13 Feb 2020 19:33:14 -0800 (PST), Norman Megill > wrote: > > I worked out an estimate (in hours) for jobs 133-160 based on the

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

I'm trying out 123 and 124 for now using AWS. I might be able to scale up depending on the results. On Thu, Feb 13, 2020 at 4:51 PM David Starner wrote: > On Thu, Feb 13, 2020 at 2:28 PM Norman Megill wrote: > > > > Here is an update of current commitments as of Feb. 13, 17:30 EST : > > > >

Re: [Metamath] Re: RFC: Mandatory definitions after constants

oit wrote: > On Thursday, February 13, 2020 at 5:46:36 PM UTC+1, Mario Carneiro wrote: >> >> That said, I think it would still be better to move all definitions >> needed for df-prds before it. This is a downside of the "everything >> structure" approach, but it does no

Re: [Metamath] Re: RFC: Mandatory definitions after constants

I realize that it seems especially inconvenient that moving df-gsum back requires moving df-0g back too. But this better reflects the reality, because df-gsum not allowed to refer to constants defined after cgsum anyway (to prevent cycles), and placing df-gsum much further along just makes this

Re: [Metamath] Riemann-zeta ratio-test rabbit-hole

(resend for the benefit of the list) It's nice to see that you're picking up where I left off in working on the zeta function. I'm still not even sure if that formula is the right approach; it is not well known and proofs about it were hard to find. The standard definition is as the analytic

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

I am still not really convinced that semigroup is worth the trouble, but I'm happy to follow the crowd here, and I don't want to belabor any points made by Norm. I just wanted to remark that if you want to prove that Semigroup C. Monoid, the easiest example (that already exists!) is NN. On Sun,

Re: [Metamath] Categories as extensible structures

I figured the monoid example would come up, but I think that really is a special case. Morphisms don't really act like a set, they are more like a |C| x |C| indexed family of sets. It just so happens that when |C| is a singleton that's just one set. In any other case, in any category that is not

Re: [Metamath] Categories as extensible structures

That proposal seems very odd to me. When we talk about categories, we almost always refer to them using their set of objects. For example, the category of groups (and group homomorphisms), or the functor category D^C (using the same exponential notation used for the underlying set of objects; the

Re: [Metamath] Re: Newbie question: is this sane?

On Wed, Jan 29, 2020 at 7:57 AM 'fl' via Metamath wrote: > It is reasonable to keep the system sound but that means there is no > way to understand precisely where smallness occurs precisely in the theory. > Actually, when you are doing relativized category theory, the smallness is quite

Re: [Metamath] Re: Newbie question: is this sane?

The problem with large categories is that they don't fit in as structures. You have to have a completely separate theory for them, so they aren't really categories at all. And category theorists never stop there anyway. They want to make constructions on top of these categories, talking about

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

On Sat, Jan 25, 2020 at 11:36 PM David A. Wheeler wrote: > On Sat, 25 Jan 2020 18:40:53 -0800 (PST), Norman Megill > wrote: > > I know I keep harping on not wanting to add a catalog of definitions > (with > > shallow theorems) that are otherwise unused, but it has been done in the > > past with

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

I'm actually deliberately not answering the header question, as that's Norm's place and not mine. But I can give my take on definitions and the way metamath has historically handled them (following Norm's vision outlined here). As you my know, MM0 departs from metamath in its handling of

Re: [Metamath] Mephistolus development

On Wed, Jan 22, 2020 at 10:51 AM Olivier Binda wrote: > 5) Mm0 > a) get a file for set.mm0 (set.mm translated to mm0) Mario, I'm looking > at you... > b) parse set.mm0 > c) extract a list of all mm0 ids > d) write a parser for mm0 statements > e) make the mephistolus Statement able to be build

Re: [Metamath] Re: AI

On Wed, Jan 15, 2020 at 2:09 PM Mario Carneiro wrote: > > > On Wed, Jan 15, 2020 at 8:16 AM vvs wrote: > >> I was very interested in FOMM 2020, but as there is no transcript I'm >> forced to look at slides and read some second hand impressions. >> > > All

Re: [Metamath] Handling "undefined terms"

On Mon, Jan 13, 2020 at 12:45 PM Benoit wrote: > Thanks for the interesting link. I do not understand Buzzard's comment: > "It's completely safe because every single *theorem* where division by > 0 isn't allowed contains the hypothesis that the denominator isn't 0 in its > statement." > How

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

I agree that both dummylink and idi should not be deleted or discouraged. While mmj2 should normally detect and collapse reused steps, I don't know if this behavior should be relied upon, and if a proof assistant finds a proof using idi then that is just as good, since it produces the right proof

Re: [Metamath] Handling "undefined terms"

On Sun, Jan 12, 2020 at 5:25 PM Benoit wrote: > On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote: >> >> qed::foo |- ( T. -> RH ) >> > > I don't understand: it looks like you are using foo with the substitutions > ph <- T. and THM &l

Re: [Metamath] Handling "undefined terms"

On Sat, Jan 11, 2020 at 11:24 AM Benoit wrote: > 1. Forbid the mere writing of nonsensical terms. > > Here, this would amount to changing cio as follows: > ${ > cio.1 $e |- E! x ph $. > cio $a |- class ( iota x ph ) $. > $} > and either leaving df-iota unchanged or writing it as in the

Re: [Metamath] Re: Difference between formal and classical math

the statement is nonsense. This is ZFC so we can't prevent such statements from being formed, and what the context is exactly is not well defined, but in practice it works well enough. On Fri, Jan 10, 2020 at 5:40 PM Benoit wrote: > On Friday, January 10, 2020 at 1:52:20 AM UTC+1, Mario Carne

Re: [Metamath] Re: Difference between formal and classical math

ou did, but of course multiplication on CC is commutative so ‾\_(ツ)_/‾ On Thu, Jan 9, 2020 at 6:31 PM Benoit wrote: > On Thursday, January 9, 2020 at 12:07:11 PM UTC+1, Mario Carneiro wrote: >> >> If you want the function version, look at dvmul. But the relation version >>

Re: [Metamath] Re: Difference between formal and classical math

If you want the function version, look at dvmul. But the relation version is the core version, because it isn't good enough to know that the derivative equals x if you don't know the function is also differentiable at x. Plus the derivative is not unique in certain pathological cases so you can't

Re: [Metamath] Re: Draft mmj2 tutorial - feedback wanted!

On Wed, Jan 8, 2020 at 11:02 AM David A. Wheeler wrote: > It'd be great to update the tutorial files. > > However, my intent for this video is to "walk through" the mmj2 > tutorial as it is provided by mmj2. So Mario would need to be willing > to accept or make changes to the tutorial within

Re: [Metamath] Re: Draft mmj2 tutorial - feedback wanted!

I think you can just write 510:,,500:syl2anc or 510:500,,:syl2anc for that. On Wed, Jan 8, 2020 at 10:51 AM Jim Kingdon wrote: > On 1/8/20 5:01 AM, Mario Carneiro wrote: > > > I would have completely removed the "?" but it breaks a lot of > > backward compati

Re: [Metamath] Draft mmj2 tutorial - feedback wanted!

On Wed, Jan 8, 2020 at 6:31 AM Marnix Klooster wrote: > Hi David, > > Thanks for this, I think it will indeed help some people to get the > feeling of a hands-on experience by just watching a video. > > Some remarks: > >- Video should probably point to a download link, and some very brief >

Re: [Metamath] Re: Draft mmj2 tutorial - feedback wanted!

I agree with Marnix that you should just pre-fix the tutorial pages rather than talking about how the tutorial is out of date in the video. Also, on page 303 you forgot to put "200,1000" in for step qed. (But it would be more impressive if you put a ! at the start, as in "!qed" with nothing else,

Re: [Metamath] Re: Using underscores in labels

On Mon, Jan 6, 2020 at 12:03 PM David A. Wheeler wrote: > On Mon, 6 Jan 2020 01:03:10 -0500, Mario Carneiro > wrote: > > My understanding of Norm's proposal is that this is a markup feature > only. > > People won't actually look at 3:2+eq+tr+4:3+d -- it's no better

Re: [Metamath] Re: Using underscores in labels

ing something like "[sqr+2+irr]" to sqr2irr, producing: > > $( [sqr+2+irr] The square root of 2 is irrational. See ~ zsqrelqelz for a >generalization to all non-square integers. The proof's core is > proven >in ~ sqr2irrlem , which shows that if ` A / B = sqr ( 2 ) `

Re: [Metamath] Re: Metamath online editor (yet another UI discussion thread)

On Sun, Jan 5, 2020 at 5:23 AM Olivier Binda wrote: > Le samedi 4 janvier 2020 18:28:18 UTC+1, Mario Carneiro a écrit : >> >> Looking at this from a green-field perspective, what should a web >> interface for metamath look like? >> > > I am also reall

Re: [Metamath] Metamath online editor (yet another UI discussion thread)

ams in your language of choice, as well as the bevy of JS-transpilable languages, so JS isn't your only option on the web anymore, practically speaking. On Sat, Jan 4, 2020 at 1:36 PM Thierry Arnoux wrote: > On 04/01/2020 18:28, Mario Carneiro wrote: > > * If I recall correctly, Stefan O'Rear

[Metamath] Metamath online editor (yet another UI discussion thread)

Hi All, This is inspired by the George Hotz thread to some extent but also my own work on MM0 and such. What would be a good user experience for writing metamath theorems in a web application? For example, MM0 currently works via a language server (written in Haskell, with a new LSP server

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

On Sat, Jan 4, 2020 at 10:08 AM David A. Wheeler wrote: > But changing our label conventions so that underscores are between the > abbreviations might be a good idea. > > It'd be a pain to rename everything, but that is something that can be > done once and could be almost entirely automated. >

Re: [Metamath] Page301.mmp fails on mmj2 version 2.5.3 - any ideas?

There was a change to the step format a while back to make it more permissive to syntax errors, but it changed the meaning of single colon statements from step:hyps to step:thm. So that means that you have to write 4:3: instead of 4:3 if you want "3" to be interpreted as a hypothesis and not a

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

There is a follow up video https://youtu.be/OAXjsUZoOgo (7 hours!), where he attempts to prove 2+2 = 4 using the axiomatization of peano.mm. This was an unfortunate choice, because peano.mm has a bizarre axiomatization, uses polish notation for no apparent reason, and has *no theorems*, meaning

Re: [Metamath] Re: Diagonal and scalar matrices

The most similar case I know to this is the definition of polynomials (df-mpl) as a subset of power series (df-psr). In that case, I anticipated that we would not care so much about power series, so df-mpl itself defines a substructure, but the subset is also accessible using "the base set of

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

Wouldn't running the program with sleeps in it or with a scheduling setting ("nice" / process priority) such that it only consumes X% of the CPU resolve the "running hot" problem? Also it could be broken into smaller pieces and run multithreaded or on multiple computers to compensate. How hard

Re: [Metamath] Stone-Weierstrass

In stowei, F is a function, an element of ( J Cn K ) where K is the topology on RR. It is being evaluated at t using ( F ` t ), so I would not expect F to have a free t in it. In metamath we use both the implicit representation of functions via open terms F[t], as well as closed terms F which we

Re: [Metamath] Packaging Metamath for Linux distros

keeps old versions of the tarball with names indexed by date, although I don't know if the dated copies include the most recent version or only start at the second most recent version. Norm will have to give the details on this. Mario Carneiro On Fri, Dec 13, 2019 at 2:01 AM heiphohmia via Metamath

Re: [Metamath] pige3 - why...?

Well, that's a nice proof! I struggled with good proofs of this theorem for a long while before I found the derivative proof, but I'm not wedded to it, and I agree that your proof approach is much more simple and direct. I'm not sure how I missed it. You should contribute it! Mario On Sun, Dec

Re: [Metamath] Re: How to process dummylink?

I agree; I think implementing compressed proof reading is worth the effort, particularly because of the exponential speedup over uncompressed proofs (in the worst case). The scheme is pretty simple to work with. Be sure to read appendix C of the metamath book, which lays it all out clearly. On

Re: [Metamath] Tarski Geometries of dimension N or more

Yes. That. On Sat, Nov 23, 2019 at 4:50 AM Thierry Arnoux wrote: > Dear fellow Metamathers, > > I think I've got it: I'll define "TarskiGLD > " as a relation, where ` G > TarskiGLD N ` holds whenever ` G ` is a Tarskian geometry of dimension ` N >

Re: [Metamath] Mephistolus development

Have you thought about providing a limited release, or a recording of you using the program? It's not really clear to me what the overall program is, and you post snippets that lack the context to make sense of them (I don't think you are expecting people to run them, but I don't even know what

Re: [Metamath] Uniqueness of MM0 secondary parsing

On Thu, Nov 14, 2019 at 11:31 AM Benoit wrote: > I hope parts of this discussion will make their way into some kind of > documentation, in particular the possibility to add extra parentheses > This should be in mm0.md, in the grammar if nowhere else. This might be surprising to a metamath user,

Re: [Metamath] Uniqueness of MM0 secondary parsing

On Fri, Nov 8, 2019 at 4:37 AM Benoit wrote: > Thanks Giovanni. I hope Mario can also chime in on the questions in my > previous message, since these are not right-or-wrong issues, but are more > about balancing pros (proximity with mathematical practice) and cons (more > complex parser). > I

Re: [Metamath] Uniqueness of MM0 secondary parsing

On Thu, Nov 7, 2019 at 6:49 AM Benoit wrote: > What do the colons and digits mean in " ((A:2) -> (B:1) : 1) " ? > They are annotating the precedence levels of subterms. It's basically a shorthand for the CFG rule expr(1) <- expr(2) "->" expr(1) where "expr(1)" is the nonterminal corresponding

Re: [Metamath] Uniqueness of MM0 secondary parsing

On Thu, Nov 7, 2019 at 2:44 AM Giovanni Mascellani wrote: > Hi, > > Il 07/11/19 03:18, Mario Carneiro ha scritto: > > Neither; it means that any time a particular infixy constant appears, it > > must have the same precedence. That is, if you have a notation x $e.$ A >

Re: [Metamath] Uniqueness of MM0 secondary parsing

On Wed, Nov 6, 2019 at 3:33 PM Giovanni Mascellani wrote: > Hi everybody (especially Mario, given the subject!), > > I am working on another MM0 implementation, and I have a few doubts > about the secondary parser (parsing in general is not my strong point). > It is said that, in order to have

Re: [Metamath] A monster theorem

On Mon, Nov 4, 2019 at 6:02 PM Giovanni Mascellani wrote: > Hi Mario, > > Il 04/11/19 21:49, Mario Carneiro ha scritto: > > Maybe you could bring me up to speed on the details here, but as I see > > it, implication introduction is 'ex'. It is important for this that &g

Re: [Metamath] A monster theorem

On Mon, Nov 4, 2019 at 3:22 PM Giovanni Mascellani wrote: > [DAW, sorry for double sending, this is meant for the mailing list] > > Il 04/11/19 18:52, David A. Wheeler ha scritto: > > There's no way to know for certain without trying, but I expect that > > an automated tool could simplify a

Re: [Metamath] Why dvexp is so different from classical math

The proof is by induction: x^1 = x so the derivative is 1 = 1 * x^(1-1), and x^(n+1) = x^n * x so the derivative is (x^n)' * x + x^n * x' = (n * x^(n-1)) * x + x^n = (n+1) * x^n. Writing that all out in formal detail is a bit more work, but not significantly so. Mario On Mon, Nov 4, 2019 at

Re: [Metamath] Why dvexp is so different from classical math

Could you be more specific? It says that the derivative of x^n is n * x^(n-1), which is pretty standard. The notation for describing what a derivative is may not be standard, but we can't easily replicate the math notation for this, which is ambiguous in several ways. On Mon, Nov 4, 2019 at 7:25

<    1   2   3   4   5   >