how obvious is "obvious"

Stream: maths

[Jasmin Blanchette]

For a grant proposal, I'd like to say something like

The pure mathematicians who have embraced the Lean proof assistant also report that formalizing a single “obvious” step can take several hours.

I'm looking for such a pure mathematician to (1) confirm so I can point to a private communication and (2) give me a better bound than "several hours", e.g. "several days".

[Jasmin Blanchette]

(I'm using "obvious" like a mathematican and "formalize" like a computer scientist I guess.)

[Ashwin Iyengar]

Can confirm! And, as a still very beginner to Lean, I agree with several hours to a few days depending on how non-obvious the seemingly obvious thing is / how mathlib is set up for that use case.

[Kevin Buzzard]

The problem is that "obvious" can take on a wide variety of meanings. Here are two case studies. The first is a beginner who wanted to prove the obvious fact that an infinite set was nonempty, but had no idea of the API for infinite or nonempty and had no idea of where to look, so spent a long time floundering around and trying all-purpose tactics none of which worked. They then asked me and I wrote a two-line proof within 60 seconds.

The second case study is me wanting to rewrite R[1/f][1/g] to R[1/fg] because those rings are obviously equal in my mental model of localisation, but were not equal in Lean's type theory, which resulted in a huge discussion and the ultimate development of an "is_localisation" predicate and a refactor of mathlib; this process took several months and the phenomenon, which was I guess known before under the name of "characteristic predicate", is now used in several other places in mathlib.

[Jasmin Blanchette]

I guess "obvious" can mean just anything that has ever been proved. With the right audience, I guess you could also invoke, say, Fermat's last theorem by an "obviously". ;)

[Jasmin Blanchette]

Thanks.

[Jasmin Blanchette]

I'll write "an arbitrarily long time".

[Kevin Buzzard]

Another case study is ongoing right now in #condensed mathematics where we are actively trying to figure out how best to define, in Lean, the concept of an int-indexed bunch of types X n equipped with maps X n -> X (n + 1). The problem is that sometimes we want a map X (n - 1) -> X n but n : int is not defeq to (n - 1) + 1 so one runs into "motive is not type correct" errors. I would say that this problem has not been solved and has been going on for years (see Reid's cdga thread from maybe 2019?), however we are actively working on it right now and have several distinct ideas which we are trialling. This is mathematically obvious to the extent that it is extremely difficult to even explain to a regular mathematician what the issue is.

Another example is the thread "algebra is not scaling for me", where something very easy in set theory became a nightmare in type theory. The issue here was that we have three rings A and B and C, with (in set-theoretic language) A a subset of B a subset of C. There are ten ways to set this up in type theory, ranging from A, B, C distinct types and maps between them, to A, B, C all subsets of a random large ring D (the technique used to such great effect in the odd order work). The problem is that the generic "make all your rings a subset of a bigger ring" strategy doesn't work in ring theory because in ring theory A is not a subring of A x B. This took months to solve and ultimately ended up with the one-line definition is_scalar_tower which I still regard as a work of genius.

Another example are the problems that we used to have with category theory, which have been ultimately mostly resolved by Scott. Again these problems are implementation issues (e.g. Lean universe problems) which are not at all apparent to the mathematician.

I think I've gone through the main "come on Lean" issues which exist in the community right now, but perhaps we will see more soon. Perhaps the analysts know examples which showed up when formalising manifolds.

[Jasmin Blanchette]

You should publish your findings in a paper called "When obvious is not obvious". :smiling_imp:

[Jasmin Blanchette]

Or "Come on, Lean!" That would be a good title tool. ;)

[Jasmin Blanchette]

(I'm just playing the part of a computer scientist who's obsessed about publications, no worries.)

[Kevin Buzzard]

Sometimes obvious turned out to be mathmaticians lying to each other (i.e. it's not actually obvious), and sometimes obvious turns out to be issues specific to type theory, or Lean's type theory, which really are obvious in mathematics -- for example the "motive is not type correct" issue, which does not exist in mathematics and in my view represents a limitation of Lean rather than anything else.

[Jasmin Blanchette]

Right.

[Kevin Buzzard]

In fact several of these issues ultimately come down to the difference of opinion between mathematicians and computer scientists want $=$ to mean. You guys are so obsessed with _defining_ it, whereas we just _use_ it. For us, of course X (i - 1 + 1) = X i is true and these two objects are clearly completely interchangeable. The dependent type theory people have a problem with this, because eq.subst is somehow not quite powerful enough. At the other extreme we have assertions like this where the word "canonical" means "we are implicitly identifying three different types here, and the identification is done in such a nice and natural way that we will never check that any resulting replacement of an element of one set with an element of the other will break anything, as ant such check is too trivial to mention".

[Eric Wieser]

A weaker version of CDGAs (without the D) are now in mathlib as docs#direct_sum.ring

[Jasmin Blanchette]

From what I understand, the main issue with DTT is that they like their type checking to be decidable. In STT (HOL), we don't even know the phrase "definitionally equal".

[Jasmin Blanchette]

And PVS, which has dependent types, is probably on HOL's side of the argument.

[Damiano Testa]

To add one more example, which is dear to my heart, to this list. Imagine that you prove a statement about leading coefficients of a polynomial, for instance that the leading coefficient of a product of the product of the leading coefficients (assuming the ground ring is a domain).

Now you want the same statement for the trailing coefficients. Well, this is obvious, but I eventually gave up trying, after many days of trying to build up to this!

If I needed to do it now, I think that I would succeed and that it would be faster, but still it would take time! (Besides, it is notnow in lean, so there is no need to do this anymore!)

[Johan Commelin]

s/not/now/ ? in the final sentence?

[Damiano Testa]

Yes, thanks! Corrected!