Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)

Indeed, Roger Penrose thinks as follows:

"The 'unprovability', in this sense, of Goodstein's theorem certainly does
not stop us from seeing that it is in fact true. Our insights enable us to
transcend the limited procedures of 'proof' that we had allowed ourselves
previously. In the present context, this provides a way of organizing an
intuition that can be directly obtained by familiarizing oneself with the
'reason' that Goodstein's theorem is in fact true."
(Roger Penrose, "The emperor's new mind")

The next level in this way is Yaroslav Sergeyev:

"Proof assistants are surely an interesting approach but I am afraid that
our methodology cannot be used in them at the moment since we use a
different (enlarged) w.r.t. tradition language allowing us to better
distinguish infinities and infinitesimals. In this context, our philosophy
of mathematics takes into account the expressiveness (and accuracy) of
languages used to formulate theorems. I attach a long survey about it":
(Yaroslav Sergeyev, personal communication)

Yaroslav Sergeyev's approach encountered a lot of resistance in
contemporary mathematics, e.g.,


But Yaroslav Sergeyev always attacks back:

Kind Regards,
José M.

El sáb., 2 mar. 2019 a las 6:36, Lawrence Paulson (<lp15 at>)

> > On 2 Mar 2019, at 01:49, José Manuel Rodriguez Caballero <
> josephcmac at> wrote:
> >
> > Some important contemporary mathematician, whose name I will omit, told
> me:
> > “I do not think that the notion of invoking proof assistants and full
> formalizations to certify mathematics is a complete approach.
> > My stance is basically the same as Roger Penrose in his books on this
> question.
> > We do intend to formalize our mathematics, but it always has irreducible
> conceptual components that are just as important as the formalization.”
> “Irreducible conceptual components” sound too much like magic.
> Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.