alt Hacker NewsNo, obviously not ...
I'm pointing out that the way Mathematics works as a discipline is that a new proof builds on existing proofs. If we have a bunch of machine-generated proofs, then a human Mathematician has to decide whether to reference any relevant machine proof that has been put out there.
If, as you suggest, human Mathematicians 'choose to ignore' a machine proof, then another human decides not to, what then? Mathematics bifurcates into 'pure human' proofs and 'mixed machine-human' or maybe 'pure machine'?
Well ok I understand your point. I’m trying to say the system has to change to adapt.
Imagine accountants saying the same thing against calculators. They had to adapt. So do mathematicians. So do I in software development.