A useful example for you might be Floris van Doorn’s formalization of
the Atiyah-Hirzebruch and Serre spectral sequences for cohomology
in HoTT using Lean:
https://arxiv.org/abs/1808.10690
Regards,
Steve
> On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote:
>
> Hi from a Lean user.
>
> As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others.
>
> I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings.
>
> I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT.
>
> Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is.
>
> If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics).
>
> Kevin Buzzard
>
> --
> 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+unsub...@googlegroups.com.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com.
I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better.
For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object.
For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com.
... But looking at
the things he formalised, he was doing things like the p-adic numbers,
and lots and lots of category theory. I am surprised that he did not
attempt to formalise the basic theory of schemes.
I would like to add my grain of salt to the discussion.
I think that mathematical research is more a communal activity than we think.
What is considered a proof largely depends on a consensus developed within the mathematical community.
Of course, the consensus relies on the opinions of experts and specialists.
Publications and referees have an important role.
But there is also a mathematical culture based on knowledge of abstract ideas
and the mastery of symbolic computations.
Homotopy type theory is contributing to the present mathematical culture by bringing
a new formalism and new abstract ideas.
It claims to be constructive and general (everything is a type).
There is an old philosophical debate concerning constructive mathematics
that was initiated by the work of Cantor, Kronecker, Hilbert, Brouwer and Bishop, to name a few.
It is true that a constructive theorem is in a sense better and more general.
In reality, constructive and non-constructive mathematics are the two faces of the same coin.
The latter is feeding the former with results to be proved constructively!
It seems obvious that the debate will endure for many generations to come.
I believe that the contributions of homotopy type theory to the mathematical
culture are important and real. It is worth developing abstractly and for
the purpose of creating user-friendly powerful proof assistants.
The language of type theory includes parametrised objects, sums, products, universes and univalence.
It is not incompatible with the language of category theory and of homotopy theory.
Hopefully, the three languages will be combined.
Best,
andré
________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Tuesday, May 28, 2019 5:50 AM
To: Kevin Buzzard
Cc: Homotopy Type Theory
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory
--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com.
--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk.
The thing I know for sure is
that there are modern maths undergraduates who grew up with computer
games and who find the idea of turning their example sheet questions
into levels of a computer game quite appealing.
Sees my name was mentioned (says the devil).
Computer games are the perfect analogy. You are fighting a proof and once you have done it you reach the next level. But then there is still the boss lemma to be defeated.
When I started using Type Theory using Randy Pollack’s LEGO system ages ago, I was playing nethack at the same time. The similarity of the two activities was intriguing (also both were entirely ASCII based). Also you can still to formal proofs when tired and or drunk. But you can’t do paper maths.
Thorsten
From:
<homotopyt...@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo...@gmail.com>
Date: Tuesday, 4 June 2019 at 21:51
To: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory
--
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
HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
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.