Brief proof that the sqrt of 2 is irrational.

Suppose that sr2 is rational. Then it can be expressed as two integers with no common factors[0], p and q, as p/q.

  sr2 = p/q   (1)

Thus

  2 = p^2/q^2 (2)

  2q^2 = p^2  (3)

So p^2 is divisible by 2. Since 2 is prime, and 2 divides p*p, it must also divide p. So p = 2p'.

Plugging this back into (3) we have

  2q^2 = 4p'^2

Which implies

  q^2 = 2p'^2

Which means that q is also divisible by 2. Which means both p and q are divisible by 2 which violates are orginal assumption [0] that p and q shared no common factors, which can be assumed for any rational number, which means that sr2 cannot be rational.

Compare the above with:

https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot....

and you get an idea of the work that needs to be done to make proof assistants more ergonomic before wide adoption in mathematics. The benefit from ensuring no mistakes were made (I'm betting I messed up somewhere above; like not specifying that p and q are not zero) is dwarfed by the difficulty in expressing the core intuition and thus reusability of the proof.

The proof included with the proof assistant Isabelle is a lot shorter and much easier to read than the Cow proof (in my opinion):

https://www.cl.cam.ac.uk/research/hvg/Isabelle//dist/library...

Interestingly, Isabelle is the director of the INRIA institute in Paris where a lot of coq is developed. I wonder if it's named after her :)

That is indeed far easier to read and understand. :)

Funny I came to complain that the final version of this exact proof is not human readable any more:

Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p x p = 2 x (q x q) -> False. intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf). clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq)); intros Hlt_O_q Heq. apply (Hrec (3 x q - 2 x p) (comparison4 _ _ Hlt_O_q Heq) (3 x p - 4 x q)). apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 x p); rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with x. apply new_equality; auto. Qed.

This doesn't have to be. Maybe the author assumed that the audience knows the proof by heart. I don't, I know a proof but none including (3 * q - 2 * p). So longer names and comments please, ideally in a way understandable both by humans and machines. Or the goal was to 'get the proof done' with maximal brevity. Then please don't include it in the 'show off' page.

In a future version of coq 'sqrt2_not_rational' might be spelled out "Theorem: sqare_root(2) not rational"

PS: stupid HN removing unicode signs

> the final version of this exact proof is not human readable any more:

In general, Coq proofs are meant to be read using tools, not as plain text. You start out with the theorem you want to prove, and you apply a rule to it. Then Coq shows two new things to prove. You apply a rule to each of these, and so on.

Without seeing the list of active "proof goals" at each step, there's no way to guess what "apply sym_not_equal" means. But if you step through the proof line-by-line in the editor, then you can examine how each step updates your "proof goals". (I have an old blog post that shows what this looks like: http://www.randomhacks.net/2015/07/19/proving-sorted-lists-c...)

I admit, it can still be pretty arcane. But with the right tools and a bit of experience, it does get a lot easier.

The real head-scratcher are advanced "proof tactics" like "auto", which automatically apply a long lists of possible transformations until they find an answer:

    Theorem basic_conj' : forall (A B : Prop),
      A -> B -> A /\ B.
    Proof. auto. Qed.

This is the Coq version of "the proof is left as a exercise for the computer."

It's pretty cool technology if you like math, well worth some time to puzzle it out. But expect to have to read some tutorials and think about them.

> I don't, I know a proof but none including (3 . q - 2 . p).

It's weird. I'm still looking at it. It would be nice to have an explanation here by someone that is a Coq specialist.

Anyway, in a google search found this other proof that uses that

> The last digit of the square of any positive integer written in base 3 can not be 2. [near a reference to Robert Gauntt]

http://www.mathpath.org/proof/sqrt2.irrat.htm

I'm not sure that it is related, but the 3q-2p and 3p-4q look like something that can be related to base 3.

It looks like the base 3 proof doesn't use the Fundamental Theorem of Arithmetic, that is a very powerful result and I'm not sure if they have already a formal demonstration of that in Coq.

Your point is clear... but as to the example, unless I'm misunderstanding your notation, the premise is that

    2 = (p/q)^2

which is not the same as

    2 = p^2/q^2

as you have in (2).

Those statements are equivalent. If p and q share no common factors, then p^2 and q^2 also don't, so p^2/q^2 is still irreducible.

They're the same, surely?

  (p/q)*(p/q)
  = p*(1/q)*p*(1/q)
  = p*p*(1/q)*(1/q)
  = (p*p)/(q*q)

Or

  (p/q)*(p/q) 
  = ((p/q)*p)/q
  = ((p*p)/q)/q
  = (p*p)/(q*q)

I find it very interesting to see how experienced Coq programmers prove things. I have enough experience to know how deliberate there choices have to be.

All this may become much easier when we manage to merge proof assistants with automatic provers.

Here is how you can prove the first theorem in Dafny. https://rise4fun.com/Dafny/GxplK

This bug only effects proofs that use types with more than 256 constructors. Also, it involves a command that is meant to optimize proofs so it isn't neccessary to ever use it. Personally, I still trust the implementation despite this edge case.

I believe this comment is meant to be a response to another post (https://news.ycombinator.com/item?id=18155410) who pointed out a flaw (now fixed) in Coq that allowed false theorems to be proved.

Github link:

https://github.com/clarus/falso