[FOM] Sergeyev-gate

[José Manuel Rodriguez Caballero]

>
> Katz wrote:
> (1) Sergeyev's reputation has been firmly established already in 2017
> through the unanimous disowning statement by the editorial board of
> EMS Surveys, where his article was published by mistake, accessible at
> http://www.ems-ph.org/journals/notice/emss/ed_note.pdf and this was
> followed by the resignation of both Editors-in-Chief who had the
> integrity to own up to their error.


This is another example of the importance of proof assistants in current
mathematical practice. One of Voevodsky's motivations for developing
mathematics in a computer was to improve the reviewing process in journals.
The problem with Voevodsky's approach (https://github.com/UniMath/UniMath)
was that most of current mathematics is not based on infinite-groupoids
yet. So, a more realistic project of computer-verified mathematics could be
ALEXANDRIA (https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/).

By the way, I meet a person in France who claimed to have a proof of the
Riemann hypothesis. I said to him: fine, formalize your proof in a proof
assistant. He said to me that it will be hard to learn a proof assistant. I
reply him: if you are able to prove the Riemann hypothesis, to read the
manual of a proof assistant is nothing for your brain. Here is the claimed
proof of the Riemann hypothesis, for the curious readers:
https://arxiv.org/abs/1804.04700

Kind Regards,
Jose M
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180830/c24405f7/attachment.html>