cubing a cube

Stream: maths

[Kevin Buzzard]

Larry Paulson issued the following challenge in his Big Proof talk: formalise a proof that it is impossible to divide a cube up into n>1 smaller cubes all of different sizes, in a theorem prover of your choice. Here's an example of an informal proof: http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof . I think it's OK to assume that all the cubes are oriented in the obvious way, i.e. no weird diagonal cubes; what I'm saying is that the problem can be formalised as a statement in discrete mathematics rather than one about the real numbers.

[Koundinya Vajjha]

why this particular problem though?

[Kevin Buzzard]

I'm just reporting on his talk. It's finished now but I can ask him. I think I know the answer though. He formalised the proof that you can't cover an 8x8 chessboard with two opposite corners removed, with dominoes, and was just issuing a challenge of a similar nature which is harder.

[Koundinya Vajjha]

isn't this related to dehn invariants or some such?

[Mario Carneiro]

I'm going to sleep now but in case anyone else wants to pick this up: https://gist.github.com/digama0/4bf0be9d7a0991a61693f490575c81c8

[Kenny Lau]

Mario sleeping? This is a miracle! :P

[Mario Carneiro]

I go into low power mode for a while :D

[Floris van Doorn]

I'm also trying to prove this :)

[Floris van Doorn]

Hmm... Your characterization of tight is probably better. My formulation was (trying to use roughly your notation):

{bottom} × base ∩ (⋃(c ∈ cubes), {c 0} × c.proj.interior) ⊆ {bottom} × base.interior

(where × means set.prod)

[Floris van Doorn]

don't you also need the condition in no_cubes_partition_aux that all cubes c have c.p 0 + c.side <= 1?

[Chris Hughes]

I don't think that fact is actually used in the proof.

[Floris van Doorn]

But I can cube a box of dimensions (1/60) x 1 x 1 assuming the cubes may be higher than the box (just by squaring a square), and I think that contradicts Mario's lemma.

[Floris van Doorn]

Here is my attempt so far: https://gist.github.com/fpvandoorn/d3da85a261169b7f37007d80cb5e59bf

The main thing missing is that the smallest cube in a "valley" cannot be in the corner or on a side. I do have the reason that once such a cube is in the middle of the valley, then there is another "valley" on top of it.

[Johan Commelin]

If we manage to finish this challenge before @Kevin Buzzard's talk on Wednesday, I think he should leave a challenge for the others... maybe something like: state and prove local (global?) class field theory in $THEOREM_PROVER_OF_CHOICE.
Apparently these challenges are quite productive (-;

[Mario Carneiro]

I updated the gist a bit, but I should get back to my other work and defer to Floris

[Johan Commelin]

Good morning, Mario!

[Johan Commelin]

How long did you manage to stay in low-power mode?

[Mario Carneiro]

:P

[Kevin Buzzard]

So this is a problem on Freek Verdijk's list of 100 problems. I talked to him over breakfast today. He said that Lean is not one of the provers on his list but he'd happily add it if someone got in touch with him and told him which of his problems had been formalised in Lean.

http://www.cs.ru.nl/~freek/100/

He made it clear that he was not going to force a formal statement onto anyone, so any reasonable interpretation of what the question is, would be satisfactory. In particular he said it was fine if we assume that the small cubes were "flat" within the big cube.

[Kevin Buzzard]

Mario maybe you should document some of your code if you want to pass it on. I'm very busy until Thursday evening, I have two talks this week.

[Mario Carneiro]

The hard part with adding lean to the 100 theorems list is getting the historical data to find out who proved what and when

[Johan Commelin]

We need another list (-; One that doesn't include silly recreational thingies, but does include class field theory.

[Mario Carneiro]

Also I probably shouldn't race to finish this proof especially if it's on the 100 theorems list. I have more than enough credits on that page already, any more would just be rude

[Mario Carneiro]

granted, I don't have any credits using lean, but neither does anyone else because no one around here likes recreational math :P

[Johan Commelin]

We could distribute the work of adding Lean to Freek's list. Just push the data to https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md

[Mario Carneiro]

I think you undervalue these problems @Johan Commelin . The point is that they aren't actually that hard - with a week of dedicated work you can get almost any of them. That's important for motivational purposes for newcomers. Asking people to climb everest won't get them off the couch

[Mario Carneiro]

The history isn't as easy as that. Abhimanyu Pallavi Sudhir wasn't the first person to prove irrational (sqrt 2) in lean. I had a proof before it was refactored to the current form, and I adapted work from Jeremy in lean 2

[Johan Commelin]

Sure, so people should feel free to update this file.

[Mario Carneiro]

hm, that seems like it's going to make it unclear how sure we are about the provenance of these theorems

[Johan Commelin]

Nr 96 Principle of Inclusion/Exclusion that one is actually useful (-; Even though it has a recreational flavour

[Johan Commelin]

Does @Freek Wiedijk accept entries without authors?

[Johan Commelin]

It's hard to dispute that certain theorems have been formalised in Lean, even if we don't know who contributed...

[Mario Carneiro]

Coq has some entries attributed to "standard library"

[Johan Commelin]

Aah, I like that author.

[Johan Commelin]

Maybe I'll start adding things to mathlib under that pseudonym.

[Floris van Doorn]

I'm close pretty to finishing (I updated the Gist above), but I should really go to bed now (or really a couple of hours ago).
Oh, I didn't know that this was one of the 7 unsolved problems on Freek's 100 list. Cool!

And I also saw that the independence of CH is on the list, so we can strike that one off soon(ish), too.

[Johan Commelin]

@Floris van Doorn Well-done! Only 5 more to go (-;

[Johan Commelin]

16. Insolvability of general higher degree equations... nobody did that??

[Mario Carneiro]

it's hard, man

[Mario Carneiro]

you have to do galois theory and everything

[Mario Carneiro]

even stating the problem is tricky

[Johan Commelin]

We'll see... I was hoping this would just drop out as a side-effect of doing Galois theory.

[Johan Commelin]

And we're getting closer to that goal every day (-;

[Mario Carneiro]

also you need the fundamental theorem of symmetric polynomials, I don't think we have that

[Johan Commelin]

I've added all the 100 theorems. I also added some entries that I knew we had. We probably have a lot more.

[Mario Carneiro]

from memory, we have

• 17 (de moivre)
• 25 (schroeder bernstein)
• 36 (brouwer FP)
• 39 (pell equation)
• 52 (number of subsets of a set)
• 58 (number of combinations) maybe not in mathlib
• 60 (bezout's theorem)
• 63 (cantor's theorem)
• 66 (sum of geometric series) - not positive
• 68 (sum of arithmetic series) - often used as an example, maybe not in mathlib
• 69 (GCD algorithm)
• 71 (order of a subgroup)
• 74 (induction)
• 78 (cauchy-schwarz)
• 79 (intermediate value theorem)
• 80 (FT of Arithmetic)
• 86 (lebesgue measure and integration)
• 94 (law of cosines) - not positive

[Mario Carneiro]

I would suggest putting the statements of theorems we have in the md file

[Mario Carneiro]

and comment out the missing theorems so that the template is there but they don't pad out the display

[Johan Commelin]

Wait, how do you even comment something out in markdown? @Mario Carneiro

[Mario Carneiro]

I think HTML comments work? <!-- -->

[Mario Carneiro]

If that doesn't work, maybe just move them all to the end of the file without the giant headers

[Mario Carneiro]

Here's the metamath 100 file for comparison: http://us2.metamath.org/mm_100.html

[Mario Carneiro]

Also I'm not sure I have a solution to this, but the links with line numbers are going to get out of date quickly

[Johan Commelin]

Aah, those comments work. I've updated the file.

[Mario Carneiro]

I think the link style can be compressed to * n. Theorem (Author, Date?, [`thm_name`](link/to/mathlib.lean#LINE))

[Johan Commelin]

Hmm... I might reformat it some time. If you can fix it up with regexes, go ahead...

[Mario Carneiro]

I think Jeremy wrote exists_infinite_primes

[Neil Strickland]

Inclusion-exclusion is at https://github.com/NeilStrickland/lean_lib/blob/master/src/combinatorics/matching.lean. I will put it in mathlib at some point.

[Floris van Doorn]

Note: The Undecidability of the Continuum Hypothesis is still in progress, so maybe it shouldn't be on the list yet (or at least it should be mentioned).

[Mario Carneiro]

I agree that we shouldn't "overcommit" to in progress theorems on the page. It is well known that this makes project completion less likely.

[Kevin Buzzard]

I overcommitted on the perfectoid project for months :-) (much to Patrick's chagrin)

[Johan Commelin]

I put the file on a community branch for a reason (-;

[Floris van Doorn]

I'm mostly done with the proof. I showed that the smallest cube cannot be on the bottom or the left sides (or their analogues in higher dimensions). Unfortunately I set up my definitions so that the symmetry for the other sides is not immediately obvious, but I'm now refactoring the code so that I can reuse most of my argument for the other side.

It's very likely that I can finish tonight :) If so, I'll also cleanup my messy code (https://gist.github.com/fpvandoorn/d3da85a261169b7f37007d80cb5e59bf).

[Kevin Buzzard]

If you're done within 10 hours then I can announce it in my talk at 9am Scottish time tomorrow and it will be another dagger in the back of the Isabelle people ;-)

[Kevin Buzzard]

I would help but I'm frantically writing my talk :-/

[Floris van Doorn]

I'll try to make that deadline, and even give you an hour to copy-paste the statement on your slides (if you want) :)

[Floris van Doorn]

I finished the proof, and added some comments explaining what's going on in the formalization.

[Floris van Doorn]

(here is the link again: https://gist.github.com/fpvandoorn/d3da85a261169b7f37007d80cb5e59bf)

[Floris van Doorn]

(deleted)

[Floris van Doorn]

The final result is

theorem cannot_cube_a_cube :
  ∀{n : ℕ}, n ≥ 3 →                              -- In ℝ^n for n ≥ 3
  ∀{ι : Type} [fintype ι] {cs : ι → cube n},     -- given a finite collection of (hyper)cubes
  2 ≤ cardinal.mk ι →                            -- containing at least two elements
  pairwise (disjoint on (cube.to_set ∘ cs)) →    -- which is pairwise disjoint
  (⋃(i : ι), (cs i).to_set) = unit_cube.to_set → -- whose union is the unit cube
  injective (cube.w ∘ cs) →                      -- such that the widths of all cubes are different
  false :=                                       -- then we can derive a contradiction

and it only depends on the following definitions not in mathlib:

structure cube (n : ℕ) : Type :=
(b : fin n → ℝ) -- bottom-left coordinate
(w : ℝ) -- width
(hw : 0 < w)

/- The j-th side of a cube is the half-open interval `[b j, b j + w)` -/
def side (c : cube n) (j : fin n) : set ℝ :=
Ico (c.b j) (c.b j + c.w)

def to_set (c : cube n) : set (fin n → ℝ) :=
{ x | ∀j, x j ∈ side c j }

def unit_cube : cube n :=
⟨λ _, 0, 1, by norm_num⟩

[Johan Commelin]

Nice work!

[Floris van Doorn]

Oh, and thanks to Mario, I stole some small things from his files:

• The idea of using din n -> _ for vectors. That works much nicer than either vector or dvector(which I tried both before that)
• Some basic lemmas at the top of his file
• The idea on how to define the "tightness" in a valley (the property that all sides are higher than the base of the valley). I formulated it a bit differently, since I'm not removing cubes from my family during the process.

[Kevin Buzzard]

My talk has this underlying story of "Lean is really cool, get on board" and stuff like this really helps. Thanks a lot Floris, and Mario too! I'll put this in my talk -- this is really timely.

[Floris van Doorn]

I would have loved to attend. Your talks are always a pleasure to listen to (I watched a couple of them online). Too bad the talks are not recorded (right?)

[Kevin Buzzard]

Yeah, apparently this ICMS thing is only a few months old and they don't have everything they want yet, this (recording talks facility) being one of them.

[Floris van Doorn]

Here is a better link to the formalization: https://github.com/fpvandoorn/mathlib/blob/cubes/src/cube.lean

[Mario Carneiro]

the description of a valley A valley is a square on which at least two cubes in the family of cubes are placed does not reflect the "at least two" in the formal definition

[Floris van Doorn]

That's fair. It felt like the most natural way to say it in English, but I updated the comment to reflect the formal statement more faithfully.

[Johan Commelin]

@Floris van Doorn If you want, you should PR this to mathlib (-; It might be merged before Kevin's talk :rolling_on_the_floor_laughing:

[Floris van Doorn]

I was considering that, but it seems like the result cannot really be reused. Therefore I thought it was not really suitable for mathlib.

[Mario Carneiro]

The last conjunct in valley is a bit confusing to me. Isn't it just saying cs i != c?

[Mario Carneiro]

I'm also wondering what to do with "satellite" proofs like this. I know we want to be able to link to it long term, and preferably it should stay updated with mathlib, but right now the only reliable way to keep stuff from bitrot is to put it in mathlib

[Floris van Doorn]

yes, it is equivalent to that. I guess that is a simpler formulation (but probably a bit further away from how I use it).

[Mario Carneiro]

maybe swap the arguments? (cs i).b 0 = c.b 0 -> (cs i).w != c.w better matches the informal We also require that no cube on it has the same size as the valley

[Floris van Doorn]

That is indeed more natural (and reduces the number of uses of modus tollens by 1). :)

[Kevin Buzzard]

As I'm sure you're aware, in maths departments we keep a very strict count on number of uses of modus tollens.

[Mario Carneiro]

it's the modus toll

[Floris van Doorn]

After those latest budget cuts, you cannot afford to use modus tollens sparingly anymore.

[Mario Carneiro]

you can use cases n, {cases hn} in the final proof

[Mario Carneiro]

or possibly rcases n with <<>> | n

[Mario Carneiro]

oh wait no that last one doesn't work

[Floris van Doorn]

I thought we were discouraged from using nat computation in the kernel like that when working with insanely large numbers like 3 :)

[Mario Carneiro]

the hardcore term proof is cases not_lt_of_le hn (bit1_pos _) I think

[Keeley Hoek]

Though this is a "satellite proof", at least some lemmas at the top there should make it into mathlib, shouldn't they?

[Mario Carneiro]

yes, in both my version and Floris's

[Mario Carneiro]

doing pretty much anything in lean produces a few of these, and they should make it into mathlib

[Johan Commelin]

We can start recreational/

[Mario Carneiro]

outside src/?

[Johan Commelin]

Even inside it

[Floris van Doorn]

Yes, I started that with #1094 (not actually used in my file, but I found that it was missing).

[Kevin Buzzard]

We can start recreational/

It's the perfect place for perfectoid spaces ;-)

[Floris van Doorn]

I'm happy to put this in mathlib. I think it would be good to have a folder outside src/ (so that it's clear it's "less important") which is compiled every PR. We might also loosen some coding style restrictions a bit for this folder. I don't really want to rename everything to the mathlib naming scheme. I would also be happy if I do not have to remove all my nonterminal simps, although I can see that keeping them might make maintenance a bit more work.

[Mario Carneiro]

I don't think these files should need to "coexist", although we might need to fix the leanchecker command to allow this

[Mario Carneiro]

I forget if all our tests currently have to coexist, or if there are five foo's in there

[Johan Commelin]

I'm fine with loosening the naming scheme

[Johan Commelin]

But the maintainability standards should be the same.

[Mario Carneiro]

I think we can also loosen the style a bit (e.g. mathlib compressed proofs not required), but it should be clear

[Mario Carneiro]

think AFP

[Jeremy Avigad]

In a sense, exists_infinite_primes was the first real theorem proved in Lean (version 0.1). I did it while Leo was still implementing the kernel type checker. There were no inductive types (Leo axiomatized the natural numbers and proved a recursion theorem to define plus and times), Prop was known as Bool (this was before Leo decided to keep the core constructive), there was no tactic mode (so Kevin is saying "oh, the horror!"), and you had to run Lean from the command line. I just found it in my mailbox, from February 11, 2014. Reading the e-mails was a trip down memory lane! It is hard to believe it was only five years ago. I am attaching the code. Alas, it does not still compile in Lean 3. primes.lean

[Jeremy Avigad]

Kevin's talk at the meeting was spectacular. And the cubing the cube theorem had a great effect. Larry Paulson made a big deal about it in his talk on the first day, and Kevin casually dropped the formal statement into at the very end of his slides. There was a big collective gasp from the audience, and Kevin just let hang there.

[Mario Carneiro]

Heh, Nat is capitalized. Looks like we are returning to our roots in lean 4

[Mario Carneiro]

I think I prefer the name refute to classical.by_contradiction

[Johan Commelin]

@Floris van Doorn Extra kudos to you!

[Johan Commelin]

It's too bad we can't hear the big collective gasp on Scott's video recording of the talk.

[Jesse Michael Han]

i'd like to hear more about the big deal Larry Paulson made about the problem in his talk. (did he claim it was inhumanly difficult in isabelle even with sledgehammer, etc)

[Scott Morrison]

I wasn't there, but just asked Jeremy the same question. I think it was more that he put it up as an example (including Littlewood's "human" proof), and said something like: "after all these years, still no one has done it in any theorem prover".

[Jesse Michael Han]

thanks Scott! also, congrats Floris: pasted image

[Ian Stark]

I felt Larry was presenting at as an example of something that has a particularly large gap between the intuitive explanation (which for me involves visualising the chimney above a small square surrounded by large cubes) and any mechanised proof (which would be — how?). I don't know at all whether the Lean result Kevin showed captures that. It wasn't that you couldn't mechanise it, but that it seemed challenging to capture a particular proof-by-visualisation.

[Johan Commelin]

That makes sense... Nevertheless, given that it was done in ~600 lines. I would say Floris can't have gotten too bogged down into gorey technical details.

[Jesse Michael Han]

i think that "chimney" is the valley in Floris' proof., which more or less follows the intuitive proof and makes it rigorous (you can't really tell from the snippet Kevin showed because a lot is being hidden in the correct predicate)

of course technical details come up because of design choices like representing the cubes in Euclidean space using specified basepoints and half-open intervals, but the parts I looked at were quite easy to visualize

[Ian Stark]

Neat.

[Kevin Buzzard]

My talk was certainly lively -- but actually a lot of the talks have been lively. I am really sorry to have left. Independent of all the Lean stuff, I met two philosophers (Silvia De Toffoli and Fenner Tanswell) who seemed very interested in the fact that there are gigantic gaps in mathematicians' informal literature. This always feels funny to me, because as mathematicians we all know about these problems, and we don't really think of them as a big deal; as a group we accept the proof, even if no one person understands it all and part of it is not published. But there are words in philosophy (a subject I know very little about) which seem to accurately describe these sorts of phenomena, and as time goes on and things get in some sense worse, philosophers seem interested in the occasional update.

[Kevin Buzzard]

I agree with @Ian Stark by the way. Larry was making the point that one could write only a few lines of text which would convince any mathematician, and yet it was equally clear to anyone who has formalised any mathematics that this is not the sort of thing that one gets cheaply in a theorem prover. The thing which I think is interesting though, and was some recurring theme in my talk, was that things get done in Lean -- it has this sort of magic property, at least at the minute, where people ask for stuff or mention stuff, and then sometimes other people step up and do that stuff. Sometimes it's as simple as a beginner asking for help, but at other times it can be quite complex code that gets written.

[Johan Commelin]

https://www.amazon.com/Getting-Things-Done-with-Lean/dp/0143126563/

[Kevin Buzzard]

ha ha, I haven't clicked but I know what Lean that will be.

[Floris van Doorn]

I had to ctrl+F5 to see the changes on http://www.cs.ru.nl/~freek/100/ but it's really there. Let's update Johan's markdown page so that Freek can link to it.

[Floris van Doorn]

@Ian Stark The proof definitely misses some of the intuitiveness of the informal explanation, and it took some thought to convert the informal explanation into a formal argument. For example: how to best express that the smallest cube cannot be on a side, because then the three adjacent cubes have to intersect?
That said, the formal proof follows the informal proof closely, as - I hope - the comments above the main lemmas explain.

[Kevin Buzzard]

I had to ctrl+F5 to see the changes on http://www.cs.ru.nl/~freek/100/ but it's really there. Let's update Johan's markdown page so that Freek can link to it.

Also, the 93% has gone up to 94% :-)