Re: [HoTT] doing "all of pure mathematics" in type theory

["Martín Hötzel Escardó" <escardo.martin@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2167 bytes --]

 Thanks for this discussion. I like it. 

Maybe I would like to argue with this point:

On 28/05/2019 10:50, Michael Shulman wrote:
> I think it's fairly hopeless to convince a classical mathematician
> that they should put in a lot of work to convince a computer of the
> truth of *something they already knew*.

I am not sure why the person who started this thread, a mathematician,
Kevin Buzzard, decided to put in such a lot of work, but did and he
has (in Lean), with his students.

But having interacted with a lot of students (from my institution, and
from everywhere in the world, from maths, logic, computer science and
philosophy departments (and once even a high school student in the
UniMath School)), what I can say is that they are not trying to
convince the computer. 

They are trying to convince themselves, using the computer to both 
check their understanding and record their understanding when 
the proof is complete.

If I am allowed to speak for myself, I created a univalent library in
Agda for the purpose of *doing something else*. However, it is nice to
stare at the library and see everything developed from first
principles. When presented with the mathematical literature, both as
students and experienced mathematicians, we are never sure how far
back one has to read until everything begins in a precise way. How
much have we created, and how do all the different fields of
mathematics interact with each other? When one records mathematics in
the computer, this begins to become clear, or at least the asnwers to such
questions become possible.

We don't need to *convince* anybody. This will *happen*. And it is
already happening. The students like it. This is my experience.

M.


-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2986 bytes --]