The equivalent proof in Metamath that the square root of 2 is irrational is here: http://us.metamath.org/mpegif/sqr2irr.html http://us.metamath.org/mpegif/sqr2i

The equivalent proof in Metamath that the square root of 2 is irrational is here: http://us.metamath.org/mpegif/sqr2irr.html http://us.metamath.org/mpegif/sqr2irr.html "The Seventeen Provers of the World" compiled by Freek Wiedijk shows proofs of "the square root of 2 is irrational" in a variety of systems, making it much easier to compare different systems. http://www.cs.ru.nl/~freek/comparison/comparison.pdf http://www.cs.ru.nl/~freek/comparison/comparison.pdf For example, the Metamath system literally shows every step, no exceptions; many other systems only show a program script to enable the computer to re-discover the proof (instead of being the actual proof itself). Which is "better"? Well, that depends on your goals :-). But it's much easier to compare systems by showing an example.