"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
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.
"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
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.