>Is this a possible goal? Note the one key insight that I feel the need to repeat: Thomas J. must not be perfect. It must not only put out correct formal proofs. It must be allowed to put out papers like we do.

So, he not only wants correct formal proofs of difficult theorems, but also insights and thoughtful conjectures? I think math is a red herring here, what he really wants is strong AI -- you can put 'writers' or 'economists' in his arguments and not much changes.