[FOM] Sergeyev-gate

[katzmik at macs.biu.ac.il]

Hi José,

Thanks for an interesting comment.

As far as formalizing things in a proof assistant, in Sergeyev's case it would
be difficult not only because there are glaring inconsistencies in his
production but especially because he raises imprecision about definitions to
the level of a methodological postulate (see his postulate 2).

Cheers,

MK

On Fri, August 31, 2018 01:06, José Manuel Rodriguez Caballero wrote:
>>
>> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>