Looks very cool, but what I've wondered - there is any other tool like Isabelle? upd. https://en.wikipedia.org/wiki/Proof_assistant
In the mathematical community, the best known proof assistants are Coq, Lean and Isabelle.
Formalising a new proof that the square root of two is irrational
21–30 of 94 posts
Re: Formalising a new proof that the square root of two is irrational
#22Re: Formalising a new proof that the square root of two is irrational
#23The 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.
That's an interesting proof, because I can easily follow it mechanically, but I have absolute no intuition for it.
Re: Formalising a new proof that the square root of two is irrational
#24The 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.
There are some assumptions in there that you haven't made explicit. They're correct, but they make the proof feel a little "cheaper". 1. Let K be the set of positive integers {n: n√2 ∈ ℤ} 2. Supposing K is non-empty, denote its minimum as k. 3. Consider k' = k√2 - k = k(√2 - 1) Lemma 1: k' L1. When x > 1, √x Lemma 2: k' is a positive integer L2a: By hypothesis, k√2 ∈ ℤ. L2b: By hypothesis, k is a positive integer. L2…
Thanks, this is actually a much better description, especially 4. OP's description can be used to "prove" that 1/2 is irrational.
Re: Formalising a new proof that the square root of two is irrational
#25> 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…
An academic paper should cite sources because such a paper makes a claim to originality of its own. So it is 'bad form' not to cite sources because you would be implying that their work is yours. A blog post does not necessarily claim originality and in particular this one does not, it's showing how a proof can be automated.
Of course, it's a good idea to cite sources anyway and it's a convenience for the reader, as well as a courtesy to the authors. But it's not a moral failing. If blog posts were as onerous to write as journal articles, there would be no advantage to blogging.
Re: Formalising a new proof that the square root of two is irrational
#26https://www.cambridge.org/core/journals/mathematical-gazette... https://en.wikipedia.org/wiki/Theodor_Estermann
[deleted]
Re: Formalising a new proof that the square root of two is irrational
#27Earlier quoted context omitted.
There are some assumptions in there that you haven't made explicit. They're correct, but they make the proof feel a little "cheaper". 1. Let K be the set of positive integers {n: n√2 ∈ ℤ} 2. Supposing K is non-empty, denote its minimum as k. 3. Consider k' = k√2 - k = k(√2 - 1) Lemma 1: k' L1. When x > 1, √x Lemma 2: k' is a positive integer L2a: By hypothesis, k√2 ∈ ℤ. L2b: By hypothesis, k is a positive integer. L2…
Thanks, this is actually a much better description, especially 4. OP's description can be used to "prove" that 1/2 is irrational.
> OP's description can be used to "prove" that 1/2 is irrational.
That won't work; in that case, k' will not be a positive number (k/2 - k is negative whenever k is positive), so you'll fail to produce a contradiction.
Re: Formalising a new proof that the square root of two is irrational
#28The 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.
[deleted]
Re: Formalising a new proof that the square root of two is irrational
#29The 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.
[deleted]
Re: Formalising a new proof that the square root of two is irrational
#30The 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.
[deleted]
Notice thay you know sqrt(2)<2 (this is easy), which does not happen in your case.