[j2kun]

This post ignores the central driving force behind why mathematicians do mathematics: mathematics was created by humans for their own pleasure. It's a coincidence that they find such useful applications in the real world, and mathematicians mostly don't care (it's like a bonus if someone finds a nice application of your work, and maybe it provides you more grant money).

In this light, why would any mathematician want to replace peer review with machine checking? It would result in two undesirable things: 1) you'd have to submit papers in a machine-checkable format, which very few people enjoy writing because it's not a natural language to do high-level reasoning in. 2) you'd lose the chance for others to tell you whether they think your research is interesting or not, relate it to other work, give their own conjectures or ask about clarification, which is the real reason for the peer review system. Overly complex proofs with subtle mistakes are few and far in between.

Similarly, why would we want to offload the joy of finding proofs and discovering new techniques to computers? That's like proposing we have computers produce all art and music. The process of creation and discovery is largely what makes mathematics worth doing!

[nnq]

I understand what you say. But my interest is actually into AI, so the same way you find pleasure in creating and understanding interesting proofs, I find pleasure in trying to think about how the human mind works and how to make artificial forms of intelligence that share the properties of human mind but not the damn limitations of the "biological hardware" and of mortality. And I also think that in fields like AI "proof by engineering" is the only way to move forward - we'll have to build them or 'evolve them' in order to prove that they can be built (I know, this is not a line of thinking that mathematicians enjoy :) )

I'd love to see AI evolving to the level at which they create art and music or analogues of these (for their own pleasure and maybe for that of humans too, if the pleasures are compatible).

I know, you'd have to share my belief that strong AI is possible (and really close too I think) and that that minds are nothing but machines themselves and that all forms of intelligence will be comparable, regardless of whether the hardware will be "biology" or "technology", "natural" or "artificial" (in a few hundreds years I think we'll even cease to make the difference between these concepts, they will appear synonyms to our non-human or not-so-human-anymore descendents, just some linguists will identify different etymologies of them) :)

[j2kun]

This is the right attitude; more power to you!

Just don't try to justify it by its "benefits" for mathematicians.