Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?

[Kevin Buzzard <kevin.m.buzzard@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 8277 bytes --]

> Kevin, I would like to second Michael's interest in seeing these 20
> commutative diagrams. Moreover, I'd also be very interested in seeing
> your "spaghetti code" (quote from the slides of your Big Proof talk): it
> seems it should be informative to see where your initial approach went
> wrong, and how much these problems and their solution had anything to do
> at all with the formal system you were working in. Are your original
> files perhaps available somewhere?
>

Sorry for the delay.

My original repo with a "bad" theorem is here:

https://github.com/kbuzzard/lean-stacks-project

The bad theorem is this:

https://stacks.math.columbia.edu/tag/00EJ

The problem is that the rings denoted R_{f_i} (localisations of rings) are
typically defined to mathematicians as "this explicit construction here" as
opposed to "the unique up to unique isomorphism ring having some explicit
property" and, as a mathematician, I formalised (or more precisely got
Imperial College maths undergraduates Chris Hughes and Kenny Lau to
formalise) the explicit construction of the localisation and then the
explicit theorem as stated in the stacks project, not understanding at the
time that this would lead to trouble. When I came to apply it, I ran into
the issue that on this page

https://stacks.math.columbia.edu/tag/01HR

we have the quote: "If f, g in R are such that D(f)=D(g), then by Lemma
26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are mutually
inverse. Hence [we can regard M_f and M_g as equal]".

This is a typical mathematician's usage of the word "canonical" -- it means
"I give you my mathematician's guarantee that I will never do anything to
M_f which won't work in exactly the same way as M_g so you can replace one
by the other and I won't mind".

As I explained earlier, by the time I noticed this subtlety it was too
late, and this led to this horrorshow:

https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268

plus the lines following, all of which is applied here

https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208

. That last link is justifying a whole bunch of rewrites along canonical
isomorphisms. These were the general lemmas I needed to prove that if A ->
B was a map, and if A was canonically isomorphic to A' and if B was
canonically isomorphic to B' and A' -> B' was the corresponding map, then
the image of A was canonically isomorphic to the image of A' etc, all in
some very specific situation where "canonically isomorphic" was typically
replaced by "unique isomorphism satisfying this list of properties". Note
that this is crappy old code written by me when I had no idea what I was
doing. One very interesting twist was this: the universal property of
localisation for the localised ring R_f is a statement which says that
under certain circumstances there is a unique ring homomorphism from R_f;
however in https://stacks.math.columbia.edu/tag/00EJ the map beta in the
statement of the lemma is *not* a ring homomorphism and so a naive
application the universal property was actually *not enough*! One has to
reformulate the lemma in terms of equalisers of ring homomorphisms and
remove mention of beta. None of this is mentioned in the stacks project
website because we are covered by the fact that everything is "canonical"
so it's all bound to work -- and actually this is *true* -- we are very
good at using this black magic word.

All of this is fixed in Ramon Mir's MSc project

https://github.com/ramonfmir/lean-scheme

and the explanations of how it was fixed are in his write-up here

https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf

Briefly, one crucial input was that the localisation map R -> R_f could be
characterised up to unique isomorphism in the category of R-algebras by
something far more concrete than the universal property, and Ramon used
this instead.

In HoTT one might naively say that these problems would not arise because
isomorphic things are equal. However my *current* opinion is that it is not
as easy as this, because I believe that the correct "axiom" is that
"canonically" isomorphic objects are equal and that the HoTT axiom is too
strong. I developed some rather primitive tools to rewrite certain
statements along certain kinds of isomorphisms with some naturality
properties, and mathematicians would be happy with these ideas. I can quite
believe that if you stick to homotopy types with the model in your mind as
being topological spaces up to homotopy then the HoTT axiom is perfect.
However there are things other than topological spaces in mathematics, for
example commutative rings, and in my mind the HoTT axiom just looks weird
and wrong in ring theory, and I expect it to backfire when HoTT people
start doing some serious ring theory. I might be wrong. Part of me hopes
I'm wrong, in fact. But this will remain my opinion until someone comes
along and formalises the definition of a scheme in one of the HoTT theories
and proves the "theorem" that an affine scheme is a scheme (I write
"theorem" in quotes because it is a construction, not a theorem). I had the
pleasure of meeting Thorsten Altenkirch earlier this week and I asked him
why this had not been done yet, and he told me that they were just waiting
for the right person to come along and do it. A year or so ago I was of the
opinion that more mathematicians should be using Lean but now I have come
to the conclusion that actually more mathematicians should be engaging with
*all* of the theorem provers, so we can find out which provers are the most
appropriate for which areas. By "mathematicians" here I really mean my ugly
phrase "proper mathematicians", i.e. people doing algebra/number
theory/geometry/topology etc, people who have absolutely no idea what a
type is and would even struggle to list the axioms of set theory. These
people with their "canonical" constructions (a phrase which has no meaning)
are the problem, and they're very hard to reach because currently these
systems offer them nothing they need. I wrote a silly game

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

to help my 1st years revise for my exam (and the game takes things much
further than the contents of the course), and I'm writing a real number
game too, to help my 1st years revise analysis for their January exam. It
would not be hard to write analogous such games in one of the HoTT
theories, I would imagine.

From what I have seen, it seems to me that Isabelle is a fabulous tool for
classical analysis, Coq is great for finite group theory, the Kepler
conjecture is proved in other HOL systems, and the HoTT systems are great
for the theory of topological spaces up to homotopy. But number theory has
been around for millennia and unfortunately uses analysis, group theory and
topological spaces, and I want one system which can do all of them. I think
that we can only find out the limitations of these systems by doing a whole
bunch of "proper mathematics" in all of them. I think it's appalling that
none of them can even *state* the Hodge conjecture, for example. For me,
that is a very simple reason for a "proper mathematician" to immediately
reject all of them in 2019. But I digress.

Kevin

>
>
> --
>
> Nicolas
>
>
>
>
> --
> 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/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz
> .
>

-- 
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/CAH52Xb2AoMWBeCCJ5B8%3DDfa8UgmO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 10887 bytes --]