[Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

Kevin Buzzard kevin.m.buzzard at gmail.com
Tue Mar 17 01:01:49 CET 2020


>
> It seems to me that if you are working with structures, i.e. do structural
> Mathematics you need to understand what they are and they cannot be reduced
> to their encodings. Hence what is the equality of structures, if not their
> structural equality? If I remember correctly, in your talk at Nottingham
> you discussed a construction by Grothendieck where he used equivalence of
> structures as if it were equality. This seems to be an omission and you and
> your students were able to address this, I think by choosing a canonical
> representation. However, the funny thing was that you were using a system
> which doesn’t allow you to express any non-structural properties but
> because of the way equality is done in Lean you cannot exploit this.
>

There is something subtle going on which I do not really understand, but it
would not surprise me if there are plenty of people on these lists who do.
Our problem with formalising the work of Grothendieck was that he assumed
that objects which were "canonically" isomorphic were in fact equal.
Canonical isomorphism is this weasel word which mathematicians often do not
define properly, but in this particular case (we had a proof of P(A) and I
could not deduce a proof of P(B) when B was "canonically" isomorphic to A)
we solved the problem by noticing that in this particular case "canonically
isomorphic" meant "satisfied the same universal property". We then changed
our proof of P(A) to prove instead P(anything satisfying the universal
property defining A), and then we were OK. I think it is interesting that
at the point in my talk when I explained this, I said "and we couldn't
believe it -- our proof barely needed changing" and you laughed and said
something like "of course it didn't!". We are mathematicians learning how
mathematics works :-) But we did not go "full univalence", we did not argue
that isomorphic objects were equal, we only needed that "canonically"
isomorphic objects were equal. In my experience of mathematics, this is the
principle which is used. My fear of univalence is that because it goes a
bit further, and that extra step seems to rule out some basic principles
used in Lean's maths library and hence makes a whole bunch of mathematical
proofs far more inconvenient to write. I am still learning about theorem
provers but am urging my community to start formalising mathematics and
this sort of thing is one of many issues which deserves to be better
understood -- certainly by mathematicians!


> I don’t know what Mathematics is actually happening in Maths departments
> but you seem to agree that it can be done in Type Theory, e.g. in Lean.
> Indeed, in a way Type Theory is not far away from Mathematical practice (if
> we ignore the question of constructiveness for the moment). And it is
> different from set theory in that it structural by nature. I just find it
> strange if one cannot go the last step and exploit this fact. It seems
> somehow this is a blast from the past: because we cannot have univalence in
> set theory we don’t need it in type theory either?
>

I just do not know whether we need it in "Fields Medal mathematics" or
whatever you want to call it, because so little "Fields Medal mathematics"
is being done in theorem provers. I have this other life when I am going
round maths departments arguing that current mathematical practice is
extremely unhygenic, producing example after example where I think that pen
and paper mathematics has got completely out of control. One thing I have
learnt from a couple of years of doing this is that most mathematicians are
(a) completely aware of the issues and (b) don't care. A mathematical
historian told me that in fact mathematics has often been like this,
basically saying that it is the nature of progress in mathematics research.

Ok, this is a different topic (and I didn’t say anything about constructive
> Maths in my original posting). I think the sort of Maths you are doing is
> very much influenced by what you are using it or what it has been used for
> in the past. It seems to me that until recently natural science and
> hardware engineering was the main application of Mathematics and hence
> influenced what Mathematicians considered as important. The world is
> changing and computer science and information technology are becoming an
> important application of Mathematics. For historical reasons and also for
> reasons of funding a lot of the Maths for Computer Science is actually done
> at Computer Science departments. I am just thinking that you, the
> Mathematicians, maybe miss a trick here; and so do we, the Computer
> Scientists because we could profit more from the wisdom of Mathematicians
> like yourself.
>

Mathematics is an incredibly broad discipline nowadays, as you say, and
serious mathematics is being done in plenty of places other than
mathematics departments. The group of people I am trying to "represent",
not necessarily by being one of them, but at least by having what I think
is a good understanding of their desires, are those people who do not care
about any of these applications, and just want to prove stuff like the
p-adic Langlands conjectures, abstract conjectures saying that some class
of infinite-dimensional objects coming from analysis are related to actions
of an infinite group on some spaces coming from algebra -- results which I
personally suspect will never have any applications to anything, but which
are just intrinsically beautiful and are hence funded because part of the
funding system in mathematics firmly believes in blue sky research. The
people I'm talking about are beautifully caricatured in "The Ideal
Mathematician"
https://personalpages.manchester.ac.uk/staff/hung.bui/ideal.pdf by David
and Hersh (in fact I slightly struggle to see what is so funny about that
article because I so completely understand the point of view of the
mathematician). In fact the only difference between some of the
mathematicians I know doing "Fields Medal mathematics" and the "ideal
mathematician" described in that article is that the areas the "Fields
Medal mathematicians" actually work in areas which are taken *much* more
seriously (like the p-adic Langlands philosophy), with very big communities
containing powerful people who are making big decisions about where the
funding is going within pure mathematics. These people might seem very
extreme to many of the people reading these mailing lists -- most do not
care about computation or constructivism, they spend their lives doing
classical reasoning about intrinisically infinite objects, and they do not
see the point of these proof assistants at all (and they also do not care
about bugs in computer code because the only point of the computer is to
check a gazillion examples to convince us that our deep conjectures are
true, and we know they're true anyway). The reason that the computer proof
community should be bending over backwards to accommodate these people is
that *these people are the important ones* within pure mathematics, and
many of them have very entrenched ideas about what is and isn't
mathematics, and what is and what isn't important. Thorsten makes some
excellent points about all the other places where mathematics is being used
but it's the people at the top of this particular tree who I want. It is
these people who should be telling us what kind of type theory should be
being used, at least for the system or systems that I believe they will
ultimately adopt. But until they notice that the systems exist it is very
difficult to get clear answers -- or indeed any answers.

> As I said to me it seems that too much surface stuff is moved into the
core of systems like Lean.


What Lean has going for it is that in practice it is turning out to be very
easy to quickly formalise the kind of mathematics which these "top of the
tree" pure mathematicians care about. However this might be because of some
social phenomena rather than because of its underlying type theory.


Kevin








Thorsten

On 08/03/2020, 14:25, "Agda on behalf of Bas Spitters" <
agda-bounces at lists.chalmers.se on behalf of b.a.w.spitters at gmail.com> wrote:

    Dear Kevin,

    The excitement about HoTT is that it has brought together several
    communities. Some are interested in homotopy theory and higher
    category theory, some (like Vladimir) want a new foundation for modern
    mathematics.
    Some combine those two by higher toposes.

    Some are trying to improve the previous generation of proof
    assistants. E.g. this influenced the design of quotients types in
    lean.
    By Curry-Howard this also influences the design of programming
    languages, like the cubical agda programming language
    (https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf)

    If we consider HoTT as an extension of type theory with the univalence
    axiom, then *of course* everything that was done before can still be
    done.
    E.g. the proof of Feit-Thompson is constructive and thus also works in
    HoTT. (I can elaborate on this if needed.)

    In fact, classical logic is valid in the simplicial set model
    (https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf).
    Moreover, that model also interprets strict propositions, so one could
    even extend lean with univalence (I believe).
    It would be interesting to know whether this simplifies the definition
    of perfectoid spaces.

    Best regards,

    Bas

    On Thu, Mar 5, 2020 at 12:25 PM Kevin Buzzard <kevin.m.buzzard at gmail.com>
wrote:
    >
    >
    >
    > On Wed, 4 Mar 2020 at 07:18, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:
    >>
    >> Dependent types are good for pure mathematics (classical or
    >> constructive). They are the natural home to define group, ring,
metric
    >> space, topological space, poset, lattice, category, etc, and study
them.
    >> Mathematicians that use(d) dependent types include Voevodsky (in Coq)
    >> and Kevin Buzzard (in Lean), among others. Kevin and his team
defined,
    >> in particular, perfectoid spaces in dependent type theory. Martin
    >
    >
    > The BCM (Buzzard, Commelin, Massot) paper defined perfectoid spaces
in Lean
    > and looking forwards (in the sense of trying to attract "working
mathematicians"
    > into the area of formalisation) I think it's an interesting question
as to whether this definition
    > could be made in other systems in a way which is actually usable. My
guess: I don't see why it couldn't
    > be done in Coq (but of course the type theories of Lean and Coq are
similar), although
    > there is a whole bunch of noncomputable stuff embedded in the
mathematics.
    > I *suspect* that it would be a real struggle to do it in any of the
HOL systems
    > because a sheaf is a dependent type, but these HOL people are good at
tricks
    > for working around these things -- personally I would start with
seeing whether
    > one can set up a theory of sheaves of modules on a locally ringed
space in a HOL
    > system, because that will be the first stumbling block. And as for
the HoTT systems,
    > I have no feeling as to whether it is possible to do any serious
mathematics other than
    > category theory and synthetic homotopy theory -- my perception is that
    > the user base are more interested in other kinds of questions.
    >
    > In particular, connecting back to the original question, a sheaf of
modules on a
    > locally-ringed space is a fundamental concept which shows up in a
typical MSc
    > or early PhD level algebraic geometry course (they were in the MSc
algebraic
    > geometry course I took), and if one wants to do this kind of
mathematics in a
    > theorem prover (and I do, as do several other people in the Lean
community)
    > then I *suspect* that it would be hard without dependent types. On
the other hand
    > I would love to be proved wrong.
    >
    > Kevin
    >>
    >>
    >> On 03/03/2020 19:43, jasongross9 at gmail.com wrote:
    >> > I'm in the process of writing my thesis on proof assistant
performance
    >> > bottlenecks (with a focus on Coq), and there's a large class of
    >> > performance bottlenecks that come from (mis)using the power of
dependent
    >> > types.  So in writing the introduction, I want to provide some
    >> > justification for the design decision of using dependent types,
rather
    >> > than, say, set theory or classical logic (as in, e.g.,
Isabelle/HOL).
    >> > And the only reasons I can come up with are "it's fun" and "lots of
    >> > people do it"
    >> >
    >> > So I'm asking these mailing lists: why do we base proof assistants
on
    >> > dependent type theory?  What are the trade-offs involved?
    >> > I'm interested both in explanations and arguments given on list,
as well
    >> > as in references to papers that discuss these sorts of choices.
    >> >
    >> > Thanks,
    >> > Jason
    >> >
    >> > _______________________________________________
    >> > Agda mailing list
    >> > Agda at lists.chalmers.se
    >> > https://lists.chalmers.se/mailman/listinfo/agda
    >> >
    >>
    >> --
    >> Martin Escardo
    >> http://www.cs.bham.ac.uk/~mhe
    >
    > --
    > You received this message because you are subscribed to the Google
Groups "lean-user" group.
    > To unsubscribe from this group and stop receiving emails from it,
send an email to lean-user+unsubscribe at googlegroups.com.
    > To view this discussion on the web visit
https://groups.google.com/d/msgid/lean-user/CAH52Xb0X%3D06U2O7K%2BLGRXyPu%3DhaKxp2FcQr3SFK0f4jm8kv9mQ%40mail.gmail.com
.
    _______________________________________________
    Agda mailing list
    Agda at lists.chalmers.se
    https://lists.chalmers.se/mailman/listinfo/agda





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.



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.
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200317/c602f7e2/attachment.html>


More information about the Agda mailing list