1) What Proof Checking systems are currently in practical use?
2) How much are formal proofs longer than usual proofs?
3) What are the lengths (lines) of formal proofs of the following theorems:
a) The set of all prime numbers is infinite;
b) 1^2 + 2^2 + ... + n^2 = n*(n+1)*(2*n+1) / 6
(if you have such formal proofs please send them to me, or give a
reference);
4) How much time is needed for a typical student to write such
formal proofs?
5) How much time is needed for your system to check such proofs?
Thank you Yuri makv@delphi.com