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

Chun wrote:
“It’s good to know that formalizing mathematic theorems is still considered as scientific contributions.”

It is bad to know that non-formalizable mathematics is still accepted as a scientific contribution. 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.”

By the way, one of the entries in Archives of Formal Proofs was implemented using a book written by the mathematician that I quoted.

My opinion is that this is a myth. It is important to work in order to demystify mathematics, e.g., to invite mathematicians to use proof assistants in order to trust the software. It is possible to ban Roger Penrose books for a while? (Joke)

Kind Regards,
José M.

Sent from my iPhone

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