Return to Revisions

I am waiting for a time when high ranked journals will require besides mathematical proofs written for human also alternative proofs that can be checked by computers (written in special language like Coq or Mizar). In this case referee will not have the obligation to check the validity of the proofs (this will be done automatically at the submission stage) but concentrate on evaluation of the importance of obtained results etc. This would save a lot of referee's valuable time and simultaneously will guarantee that the papers accepted for publication do not contain errors.