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



> On 2 Mar 2019, at 01:49, José Manuel Rodriguez Caballero <josephcmac at gmail.com> 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.