Formalising a new proof that the square root of two is irrational
lawrencecpaulson.github.io
Formalising a new proof that the square root of two is irrational
1–10 of 94 posts
Re: Formalising a new proof that the square root of two is irrational
#2> Recently, somebody shared on Twitter a new proof
As far as I can tell there is no link to this tweet in this post which is bad form to say the list. The post has multiple links promoting author's other posts, but not to the raison d'etre for this post.
Clarification: The post does link to a Tumbler post which one might infer had been mentioned in the tweet, but without a link to said tweet, it's odd. It is common to give credit to the work that led to one's discovery of related work.
PS: Apparently, the author is Director of Research, Computer Laboratory, University of Cambridge which makes this lack of proper citation even more perplexing.
PPS: Compare the intro paragraph of this post to one that properly cites related work[1] with actual links to the referenced works:
>> Yesterday I came a across a new (new to me, that is) proof of the irrationality of \sqrt{2}. I found it in the paper “Irrationality From The Book,” by Steven J. Miller, David Montague, which was recently posted to arXiv.org.
PPPS: It is especially ironic that the author has also wrote this at some point[2]:
>>> Many people write their related work section in a wholly passive mockery of English, never mentioning the names of their colleagues: ... It’s discourteous and reads badly. Reference numbers are not names, so why do you keep forcing your reader to look them up in the bibliography? The direct way is also clearer: ...
[1]: https://divisbyzero.com/2009/10/06/tennenbaums-proof-of-the-...
Re: Formalising a new proof that the square root of two is irrational
#3Looks very cool, but what I've wondered - there is any other tool like Isabelle?
upd.
https://en.wikipedia.org/wiki/Proof_assistant
Re: Formalising a new proof that the square root of two is irrational
#4> Recently, somebody shared on Twitter a new proof As far as I can tell there is no link to this tweet in this post which is bad form to say the list. The post has multiple links promoting author's other posts, but not to the raison d'etre for this post. Clarification: The post does link to a Tumbler post which one might infer had been mentioned in the tweet, but without a link to said tweet, it's odd. It is common t…
The first sentence in the blog post contains a link to the proof itself, which seems to have been posted to tumblr: https://theapproximatepresent.tumblr.com/post/51484587425/a-...
I'm not sure it is necessary for the author also post the link to the tweet that referred to the tumblr post, since the tumblr post is where the actual proof is.
Re: Formalising a new proof that the square root of two is irrational
#5> Recently, somebody shared on Twitter a new proof As far as I can tell there is no link to this tweet in this post which is bad form to say the list. The post has multiple links promoting author's other posts, but not to the raison d'etre for this post. Clarification: The post does link to a Tumbler post which one might infer had been mentioned in the tweet, but without a link to said tweet, it's odd. It is common t…
The first sentence in the blog post contains a link to the proof itself, which seems to have been posted to tumblr: https://theapproximatepresent.tumblr.com/post/51484587425/a-... I'm not sure it is necessary for the author also post the link to the tweet that referred to the tumblr post, since the tumblr post is where the actual proof is.
The tweet is the "secondary source" whereas the Tumbler post is the "primary source" in this context[1]:
> For example, suppose you are reading an article by Brown (2014) that cites information from an article by Snow (1982) that you would like to include in your essay. For the reference list, you will only make a citation for the secondary source (Brown). You do not put in a citation for the primary source (Snow) in the reference list. For the in-text citation, you identify the primary source (Snow) and then write "as cited in" the secondary source (Brown).
Regardless of one's preferred style guide, it is odd not to credit the author whose work that led to one's discovery of the inspiration for one's own work.
[1]: https://guides.library.uwm.edu/c.php?g=1007936&p=7303662
Re: Formalising a new proof that the square root of two is irrational
#6> Recently, somebody shared on Twitter a new proof As far as I can tell there is no link to this tweet in this post which is bad form to say the list. The post has multiple links promoting author's other posts, but not to the raison d'etre for this post. Clarification: The post does link to a Tumbler post which one might infer had been mentioned in the tweet, but without a link to said tweet, it's odd. It is common t…
The first sentence in the blog post contains a link to the proof itself, which seems to have been posted to tumblr: https://theapproximatepresent.tumblr.com/post/51484587425/a-... I'm not sure it is necessary for the author also post the link to the tweet that referred to the tumblr post, since the tumblr post is where the actual proof is.
it's a little more confusing than that, because while he does link to a proof, the proof does not claim to be new, the guy says
"A favourite proof of mine: first demonstrated to me by my professor in number theory. I think its beauty stems from the fact that it requires no knowledge of mathematics above the definition of what it means for a number to be rational, and can be written almost in one line."
Re: Formalising a new proof that the square root of two is irrational
#7> Recently, somebody shared on Twitter a new proof As far as I can tell there is no link to this tweet in this post which is bad form to say the list. The post has multiple links promoting author's other posts, but not to the raison d'etre for this post. Clarification: The post does link to a Tumbler post which one might infer had been mentioned in the tweet, but without a link to said tweet, it's odd. It is common t…
The first sentence in the blog post contains a link to the proof itself, which seems to have been posted to tumblr: https://theapproximatepresent.tumblr.com/post/51484587425/a-... I'm not sure it is necessary for the author also post the link to the tweet that referred to the tumblr post, since the tumblr post is where the actual proof is.
I think the grandparent is under the impression that the alleged Twitter version of the post had a non-anonymous author and that the Github blog instead chose to link to a Tumblr blog, where the blog author claims they learned the proof from an anonymous number theory professor, thus laundering out the authorship.
But I suspect the alleged Twitter version was just a link to the Tumblr, for which it's clearly not necessary to attribute the retweeter (especially in the context of the post being "the proof is actually incomplete, not very good, and less beautiful/more complex than the canonical proof").
Re: Formalising a new proof that the square root of two is irrational
#8Earlier quoted context omitted.
The first sentence in the blog post contains a link to the proof itself, which seems to have been posted to tumblr: https://theapproximatepresent.tumblr.com/post/51484587425/a-... I'm not sure it is necessary for the author also post the link to the tweet that referred to the tumblr post, since the tumblr post is where the actual proof is.
The tweet is the "secondary source" whereas the Tumbler post is the "primary source" in this context[1]: > For example, suppose you are reading an article by Brown (2014) that cites information from an article by Snow (1982) that you would like to include in your essay. For the reference list, you will only make a citation for the secondary source (Brown). You do not put in a citation for the primary source (Snow) in…
You keep saying “author”, but putting a screenshot of a Tumblr post on Twitter is stretching the word quite considerably.
Besides, the Tumblr post is already a secondary source.
Re: Formalising a new proof that the square root of two is irrational
#9The new proof rephrased:
Let K be the set of positive integers k such that k √2 is an integer.
Suppose K is non-empty, denote its minimum as k.
Consider the positive integer k' = k √2 - k = k (√2 - 1).
Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.
Re: Formalising a new proof that the square root of two is irrational
#10The new proof rephrased: Let K be the set of positive integers k such that k √2 is an integer. Suppose K is non-empty, denote its minimum as k. Consider the positive integer k' = k √2 - k = k (√2 - 1). Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.
... which contradicts the hypothesis that k is the minimum. Therefore, K is empty.