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

[Michael Shulman <shulman@sandiego.edu>]

Thanks Martin!  Of course you are right that there are people who
don't need to be convinced and who derive benefit and pleasure from
their formalization efforts, and in our community we probably
encounter a lot of them.  However, I still maintain that the *average*
working mathematician is not yet going to find such work useful or
rewarding for its own sake.  If you go to, say, the U.S. Joint
Mathematics Meetings and stop a hundred mathematicians at random in
the lobby and ask whether they have ever formalized their work in a
proof assistant, how many do you think will say yes?

Perhaps I am too pessimistic.  But let me in turn offer myself as an
example: in addition to being a homotopy type theorist, I have another
hat as a classical category theorist and homotopy theorist.  When I
prove things in HoTT, I often formalize them in a proof assistant.
But when I prove things in classical mathematics, I very rarely
consider formalizing them.  Only once have I formalized a proof in
classical category theory; the experience was more time-consuming and
less enjoyable than I expected, and I have no plans to do it again.
And I expect that as classical mathematicians go, I am (even when I
have my classical mathematician hat on) pretty far on the
sympathetic-to-formalization side of the spectrum.



On Wed, May 29, 2019 at 12:05 PM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
>  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.

-- 
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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.