Having trouble understanding (sqrt2irr)

[M Malik]

Hello Metamath peeps,

I am trying to learn advanced math with assistance of Metamath. I understand a lot of elementary theorems that are in the database. However, I thought I would jump to (sqrt2irr -Irrationality of square root of 2), but its proof isn't really making sense to me. 

I am specifically confused about this wff [ For all x e. Z (sqrt2 =/= x/z) ]. Is this something to be assumed true from the start?

Also, in general, is it recommended to download the mmj2 program or the content on the Metamath website sufficient enough?

Thanks.

-Malik.

[Mario Carneiro]

On Sun, Nov 20, 2022 at 9:24 PM M Malik <vayn...@gmail.com> wrote:

Hello Metamath peeps,

I am trying to learn advanced math with assistance of Metamath. I understand a lot of elementary theorems that are in the database. However, I thought I would jump to (sqrt2irr -Irrationality of square root of 2), but its proof isn't really making sense to me. 

I am specifically confused about this wff [ For all x e. Z (sqrt2 =/= x/z) ]. Is this something to be assumed true from the start?

No, it (more or less) is proved by complete induction on z (which is to say, induction on y e. NN such that x < y) at step 78 of https://us.metamath.org/mpeuni/sqrt2irr.html .

 

Also, in general, is it recommended to download the mmj2 program or the content on the Metamath website sufficient enough?

The content of the website should be sufficient for viewing proofs, and indeed is somewhat better than the mmj2 display for many purposes. mmj2 is more if you are interested in writing a proof yourself.

Mario

[M Malik]

Hello Mario,

Sorry if this is too trivial of a question. Where does this statement [ z < 1 -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ] come from? I understand it's associated to ( n = 1 ) case for strong induction, but I am not sure what makes it true. 

Also, is there a way to know what book this theorem was referenced from? I apologize since these questions aren't really related to Metamath but math in general. Let me know if I need to stop posting these kind of questions here. Appreciate your time.

-Malik.

[Mario Carneiro]

These kinds of questions are fine, although you are asking questions about statements rather than proofs. "where does this proposition come from" is not a very targeted question. I assume you are referring to step 13 of https://us.metamath.org/mpeuni/sqrt2irr.html , in which case we can check the proof that leads up to it:

11		nnnlt1 11302	. . . . . . . . 9 ⊢ (𝑧 ∈ ℕ → ¬ 𝑧 < 1)
12	11	pm2.21d 119	. . . . . . . 8 ⊢ (𝑧 ∈ ℕ → (𝑧 < 1 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))
13	12	rgen 3066	. . . . . . 7 ⊢ ∀𝑧 ∈ ℕ (𝑧 < 1 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))

That is, it is true that every natural number z less than 1 satisfies A. x e. ZZ (sqrt`2) =/= (x/z) simply because there are no natural numbers less than 1. (In metamath the set NN denotes the strictly positive integers, i.e. 1, 2, 3, ... and all of these are greater or equal to 1.)

I don't have a particular book to reference for this proof (it would be mentioned in the head comment if there was), but it is a classical proof, by "infinite descent" (I think Fermat is credited for it). The proof in sqrt2irr itself is merely the setup work, the core of the proof is in sqrt2irrlem, where we show that if sqrt(2) = A/B then A/2 and B/2 are both integers, in which case (A/2)/(B/2) is a smaller expression for sqrt(2). So we are doing induction on B here, with the observation that B/2 is a natural number less than B so that we can assume by induction that sqrt(2) is not a fraction with denominator B/2 and hence also not a fraction with denominator B.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b31cd4ce-0dff-496f-9892-b1a714987710n%40googlegroups.com.

[David A. Wheeler]

> I am trying to learn advanced math with assistance of Metamath.

Cool!

> I understand a lot of elementary theorems that are in the database. However, I thought I would jump to (sqrt2irr -Irrationality of square root of 2), but its proof isn't really making sense to me.

I've toyed with the idea of creating an "Introduction to Formalized Mathematics Using the Metamath Proof Explorer (MPE)".
It would highlight the key axioms, definitions, and proofs (with links), with an idea of creating a simple
introduction to the idea & how it's done in MPE. It might be gentler "way to start"
instead of reading MPE directly. It could be done in a different repository, but
if it was in the same repository it'd be easier to keep consistent.

I'd be curious if anyone else thought it'd be a good idea.

--- David A. Wheeler

[Mario Carneiro]

I think we should not put everything in set.mm repo, or if we do, we clearly separate set.mm from the rest of it. I think there is already too much stuff in the repo that isn't about set.mm itself. What you have described clearly sounds like a separate project, like a blog post series or something, and as such it wouldn't need to stay rigidly in sync and could just pin a version of set.mm to work with.

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/46339806-74AD-42C1-B8C3-787454AB0708%40dwheeler.com.

[David A. Wheeler]

> On Nov 22, 2022, at 3:59 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> I think we should not put everything in set.mm repo, or if we do, we clearly separate set.mm from the rest of it. I think there is already too much stuff in the repo that isn't about set.mm itself. What you have described clearly sounds like a separate project, like a blog post series or something, and as such it wouldn't need to stay rigidly in sync and could just pin a version of set.mm to work with.

I agree with your general point of "don't put everything in the set.mm repo".

However, I have in mind a book that syncs with set.mm, that is, the book is updated as set.mm changes, that is, it *DOES* stay rigidly in sync. The easiest way to simultaneously edit them is to put them in the same repo :-).

---- David A. Wheeler

[Mario Carneiro]

I don't think the book needs to stay rigidly in sync at all. It's only had two editions in how many years? In any case, while it is undoubtedly more work to have to manage parallel PRs, it is definitely more scalable than assuming that everything lives in the same repo. If set.mm is to be a monorepo it should probably be renamed to reflect that.

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/067489BC-395A-4AC3-AB27-5D632D09B4DE%40dwheeler.com.

[Mázsa Péter]

On Tue, Nov 22, 2022 at 8:50 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> I've toyed with the idea of creating an "Introduction to Formalized Mathematics Using the Metamath Proof Explorer (MPE)".
> It would highlight the key axioms, definitions, and proofs (with links), with an idea of creating a simple
> introduction to the idea & how it's done in MPE. It might be gentler "way to start"
> instead of reading MPE directly. It could be done in a different repository, but
> if it was in the same repository it'd be easier to keep consistent.
>
> I'd be curious if anyone else thought it'd be a good idea.

I think it is a great and important idea.
As a greenhorn I have a fresh eye for this. Supposed that a student is
already able to compile a simple proof, I think the most interesting
property of Metamath for outsiders is that it gives constant theorem
verification feedback for its users (plus all inputs and outputs of
the transparent verification process are both human and machine
readable). This means that (properly prepared and instructed) students
are able to *experiment* with different proofs or even with different
definitions (how would you define this; if you define it this or that
way then what follows from them, what is and why exactly this is the
definition of it in set.mm which accumulates explicit knowledge,
etc.).
For example, in the case of axioms, what a great piece of storytelling
is the comments of https://us.metamath.org/mpeuni/ru.html ! Can we use
this as a tool as an approach to introduction? Or what a
context-revealing approach is the one in Appendix 7
https://us.metamath.org/mpeuni/mmset.html#subsys !
Of course I do not think that an introduction should begin with the
comparison of the consequences of the alternate axiom/definition
systems - perhaps, after the first steps, analysis/reproduction of
some great theorems is the right way forward - but I feel that this
constant feedback property opens up some exciting new ways for
introduction into Meta/math.

[David A. Wheeler]

> On Nov 22, 2022, at 5:48 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> I don't think the book needs to stay rigidly in sync at all. It's only had two editions in how many years? In any case, while it is undoubtedly more work to have to manage parallel PRs, it is definitely more scalable than assuming that everything lives in the same repo. If set.mm is to be a monorepo it should probably be renamed to reflect that.

I don't mean the "Metamath book" - that's already in a separate repo, and I think that's sensible. I don't propose changing that.

I'm thinking about a *different* book that is essentially a gentle introduction/walkthrough of set.mm as it currently exists, and is updated simultaneously as set.mm is updated. Think of it as set.mm documentation for those new to formal mathematics.

--- David A. Wheeler

[Gonzalo Polavieja]

I'm thinking about a *different* book that is essentially a gentle introduction/walkthrough of set.mm as it currently exists, and is updated simultaneously as set.mm is updated. Think of it as set.mm documentation for those new to formal mathematics.

As a very gentle intro, maybe consider a gamified entry to Metamath similar to the Number game in Lean, https://www.google.com/search?q=number+game+Lean&oq=number+game+Lean&aqs=chrome..69i57j0i22i30l4.3971j0j15&sourceid=chrome&ie=UTF-8

Gonzalo

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1ECB3EDD-4C56-44E0-B6E2-23771ED8D63B%40dwheeler.com.