As of 2018, mathematical proofs are still being decided by human consensus. i.e. Give the proof to a few capable humans and if none of them can find any errors than they vote that the proof is correct and it can be published.
This surely is not a foolproof way of deciding mathematical truths.
One would think that there would by now be some standard way proofs could be written and computer checked for accuracy.
I read about a few computer checking systems a few years ago that hoped to do things like check Wile's proof of Fermat's last theorem or the Classification of Simple Groups Theorem. But not much more has been heard about them.
What has happened to this endeavour. Have mathematicians lost interest in having proofs computer checked?
It used to be that mathematicians would strive for formalisation of all mathematics. And yet it seems that they prefer the sloppy formalism of current mathematics which cannot be translated into computer language because much of it is ambiguous.
I would have thought that in 2018, every proof submitted to a mathematics journal would basically be written in a form that could be automatically proof checked. And conversely every unproved theorem written in a language that could be fed into a computer.
Even an amateur could then post a proof to the journal and with the press of a button could see if the proof was correct or garbage.
Do you know what the current state of this is?