Very good analogy, thank you. This is what someone who knows only about printing press would say about impossibility of showing text on a computer screen - "imagine the work that would have to be done to split the image into pixels and then put them together so that they don't look like gibberish".

If you really want you can always make this statement true by selecting the right definition of "genuine problems", for example defining genuine problems as those that have not been formalized yet. Otherwise you may want to check the list of top 100 of mathematical theorems to see which ones have proofs written in a formal proof language.

Here you have a point. This proof is not designed to explain to a human why the theorem is true. It should not be called a proof, it should be called a verification script. But this is just an unfortunate choice of the language. There are other proof languages that are designed to be readable by humans.

There is such check: writing proofs in a formal proof language so that they can be verified by a machine. This is a barrier high enough that no crackpot can jump over it. Too bad math departments don't teach formal proof langauges.

Readability and writeability are separate and diametrically opposed issues. (...) We apparently both agree that readability and writeability are conflicting goals.

Not exactly. My opinion is that readability and writeability are orthogonal in the design of a formal proof language. For most formal proof languages the design effort was invested in writeability because those languages were intended to be used for formal verification of software. However, mathematicians are not only interested in the fact that the assertion of a theorem is true, but also want to know why it is true, i.e. they want to be able to read the proofs. There is a line of formal proof languages whose design goal is readability (Mizar, Isar and the declarative proof language for COQ ). After getting used to, proofs in those languages are as readable as standard (informal) proofs.

machine readable proofs are not useful for developing new math, and they are also not useful for teaching mathematics to the general public

Well, if you phrase it this way I agree. Writing formal proofs will always be more difficult than writing the standard ones. This is because they contain much more information. It is not useful for a mathematician to write his/her proofs in a formal proof language before publication. In most cases it is not even practically possible because there is not enough background in formalized form. So, if you are a mathematician, formalized mathematics will not be of much use. It will not advance your career. It may inhibit it as it is a bit addictive and may consume the time you should spend writing publications and grant proposals. It is also not useful for educating general public. It typically requires some background in the foundations, like set theory. General public doesn't know set theory. General public doesn't know how to add fractions. So what is formalized mathematics good for? I personally do it for fun and as expression of creativity. I think it may be useful for getting more information about existing mathematics. For example, take the role of the axiom of choice in the construction of Lebesque measure. Since in ZF you can not prove that real numbers are not a countable union of countable sets, you can not construct the Lebesque measure (or any nontrivial measure on real numbers that assigns zero to all singletons) without using the axiom of choice somewhere. Where exactly is it used? What can you get without it? It would be very easy to find out if we had a formalized construction. Another use of formalized mathematics could be learning mathematics not by the "general public" but by the students of mathematics. We may disagree on that since you don't believe that formal proofs can be made readable. But I think they can, and if they are structured well, as Isar allows, the machine can display the desired level of detail, zoom in if some step is not clear and zoom out if some part is (seems) obvious. This use is more about knowledge representation than correctness of proofs.