From: Kevin Buzzard <email@example.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] doing "all of pure mathematics" in type theory
Date: Sat, 25 May 2019 03:12:04 -0700 (PDT) [thread overview]
Message-ID: <firstname.lastname@example.org> (raw)
[-- Attachment #1.1: Type: text/plain, Size: 3305 bytes --]
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
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 HomotopyTypeTheoryemail@example.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.
[-- Attachment #1.2: Type: text/html, Size: 3866 bytes --]
next reply other threads:[~2019-05-25 10:12 UTC|newest]
Thread overview: 31+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-05-25 10:12 Kevin Buzzard [this message]
2019-05-25 10:22 ` Steve Awodey
2019-05-25 12:23 ` Kevin Buzzard
[not found] ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se>
[not found] ` <CAH52Xb1Y=Xq=012v_-KSDUuwgnKpEp5qjrxgtUJf+qc_0RWJUg@mail.gmail.com>
2019-05-25 13:13 ` Fwd: " Kevin Buzzard
2019-05-25 13:34 ` Juan Ospina
2019-05-25 14:50 ` Noah Snyder
2019-05-25 15:36 ` Kevin Buzzard
2019-05-25 16:41 ` Noah Snyder
2019-05-26 5:50 ` Bas Spitters
2019-05-26 11:41 ` Kevin Buzzard
2019-05-26 12:09 ` Bas Spitters
2019-05-26 17:00 ` Kevin Buzzard
2019-05-27 2:33 ` Daniel R. Grayson
2019-06-02 16:30 ` Bas Spitters
2019-06-02 17:55 ` Kevin Buzzard
2019-06-02 20:46 ` Nicola Gambino
2019-06-02 20:59 ` Valery Isaev
2019-06-04 20:32 ` Michael Shulman
2019-06-04 20:58 ` Kevin Buzzard
2019-06-06 16:30 ` Matt Oliveri
2019-05-27 13:09 ` Assia Mahboubi
2019-05-28 9:50 ` Michael Shulman
2019-05-28 10:13 ` Nils Anders Danielsson
2019-05-28 10:22 ` Michael Shulman
2019-05-29 19:04 ` Martín Hötzel Escardó
2019-05-30 17:14 ` Michael Shulman
2019-06-02 17:49 ` Kevin Buzzard
2019-06-04 20:50 ` Martín Hötzel Escardó
2019-06-05 17:11 ` Thorsten Altenkirch
2019-05-28 15:20 ` Joyal, André
2019-05-27 8:41 ` Nils Anders Danielsson
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).