byrnema comments on Formalized math: dream vs reality