On 30/05/2018, 11:53, "Alexander Kurz" <a...@gmail.com> wrote:

 

    It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.

 

I completely disagree. Set theory is untyped and conceptually misleading, to talk about all natural numbers you quantify over all sets singling those out that represent natural numbers. Untyped thinking leads to non-structural Mathematics, to mathematical hacking and a lack of abstraction. Indeed, the impossibility to hide anything in an untyped universe is one of the diseases of contemporary Mathematics.

 

I am not talking about formalising Mathematics (sure it is hard work) but I am talking about thinking about it.

 

It is not true that the difficulty of formalisation has anything to do with typedness. To the contrary types help you to structure your development, they provide a good structure to follow and indeed work well with category theory.

   

    If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.

 

The problem is that people still use untyped Mathematics.

 

   

    

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.