## Stream: maths

### Topic: cubing a cube

#### Kevin Buzzard (May 27 2019 at 15:57):

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 (May 27 2019 at 15:58):

why this particular problem though?

#### Kevin Buzzard (May 27 2019 at 15:59):

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 (May 27 2019 at 16:08):

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

#### Mario Carneiro (May 27 2019 at 20:53):

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

#### Kenny Lau (May 27 2019 at 20:54):

Mario sleeping? This is a miracle! :P

#### Mario Carneiro (May 27 2019 at 20:55):

I go into low power mode for a while :D

#### Floris van Doorn (May 27 2019 at 21:58):

I'm also trying to prove this :)

#### Floris van Doorn (May 27 2019 at 22:28):

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 (May 27 2019 at 22:42):

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 (May 27 2019 at 23:00):

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

#### Floris van Doorn (May 28 2019 at 00:44):

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 (May 28 2019 at 04:56):

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 (May 28 2019 at 05:50):

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 (May 28 2019 at 06:38):

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

#### Johan Commelin (May 28 2019 at 06:42):

Good morning, Mario!

#### Johan Commelin (May 28 2019 at 06:42):

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

:P

#### Kevin Buzzard (May 28 2019 at 08:13):

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 (May 28 2019 at 08:14):

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 (May 28 2019 at 08:20):

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 (May 28 2019 at 08:22):

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

#### Mario Carneiro (May 28 2019 at 08:24):

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 (May 28 2019 at 08:26):

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 (May 28 2019 at 08:29):

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 (May 28 2019 at 08:30):

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 (May 28 2019 at 08:32):

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 (May 28 2019 at 08:32):

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

#### Mario Carneiro (May 28 2019 at 08:34):

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

#### Johan Commelin (May 28 2019 at 08:34):

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

#### Johan Commelin (May 28 2019 at 08:35):

Does @Freek Wiedijk accept entries without authors?

#### Johan Commelin (May 28 2019 at 08:35):

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

#### Mario Carneiro (May 28 2019 at 08:35):

Coq has some entries attributed to "standard library"

#### Johan Commelin (May 28 2019 at 08:36):

Aah, I like that author.

#### Johan Commelin (May 28 2019 at 08:36):

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

#### Floris van Doorn (May 28 2019 at 08:40):

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 (May 28 2019 at 08:42):

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

#### Johan Commelin (May 28 2019 at 08:42):

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

it's hard, man

#### Mario Carneiro (May 28 2019 at 08:43):

you have to do galois theory and everything

#### Mario Carneiro (May 28 2019 at 08:43):

even stating the problem is tricky

#### Johan Commelin (May 28 2019 at 08:44):

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

#### Johan Commelin (May 28 2019 at 08:44):

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

#### Mario Carneiro (May 28 2019 at 08:45):

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

#### Johan Commelin (May 28 2019 at 09:07):

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 (May 28 2019 at 09:18):

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 (May 28 2019 at 09:21):

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

#### Mario Carneiro (May 28 2019 at 09:23):

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

#### Johan Commelin (May 28 2019 at 09:28):

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

#### Mario Carneiro (May 28 2019 at 09:28):

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

#### Mario Carneiro (May 28 2019 at 09:30):

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

#### Mario Carneiro (May 28 2019 at 09:30):

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

#### Mario Carneiro (May 28 2019 at 09:32):

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 (May 28 2019 at 09:35):

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

#### Mario Carneiro (May 28 2019 at 09:38):

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

#### Johan Commelin (May 28 2019 at 09:39):

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

#### Mario Carneiro (May 28 2019 at 09:42):

I think Jeremy wrote exists_infinite_primes

#### Neil Strickland (May 28 2019 at 14:54):

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 (May 28 2019 at 16:30):

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 (May 28 2019 at 16:38):

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 (May 28 2019 at 18:08):

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

#### Johan Commelin (May 28 2019 at 19:42):

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

#### Floris van Doorn (May 28 2019 at 21:54):

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 (May 28 2019 at 21:55):

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 (May 28 2019 at 21:55):

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

#### Floris van Doorn (May 28 2019 at 21:56):

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 (May 29 2019 at 03:58):

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

#### Floris van Doorn (May 29 2019 at 03:58):

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

(deleted)

#### Floris van Doorn (May 29 2019 at 04:01):

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⟩


Nice work!

#### Floris van Doorn (May 29 2019 at 04:54):

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 (May 29 2019 at 05:13):

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 (May 29 2019 at 05:20):

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 (May 29 2019 at 05:21):

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 (May 29 2019 at 05:25):

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

#### Mario Carneiro (May 29 2019 at 05:28):

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 (May 29 2019 at 05:34):

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 (May 29 2019 at 05:34):

@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 (May 29 2019 at 05:35):

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 (May 29 2019 at 05:35):

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

#### Mario Carneiro (May 29 2019 at 05:37):

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 (May 29 2019 at 05:38):

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 (May 29 2019 at 05:40):

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 (May 29 2019 at 05:50):

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

#### Kevin Buzzard (May 29 2019 at 05:50):

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 (May 29 2019 at 05:50):

it's the modus toll

#### Floris van Doorn (May 29 2019 at 05:51):

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

#### Mario Carneiro (May 29 2019 at 05:54):

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

#### Mario Carneiro (May 29 2019 at 05:55):

or possibly rcases n with <<>> | n

#### Mario Carneiro (May 29 2019 at 05:56):

oh wait no that last one doesn't work

#### Floris van Doorn (May 29 2019 at 05:57):

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

#### Mario Carneiro (May 29 2019 at 05:58):

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

#### Keeley Hoek (May 29 2019 at 05:59):

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

#### Mario Carneiro (May 29 2019 at 06:00):

yes, in both my version and Floris's

#### Mario Carneiro (May 29 2019 at 06:00):

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

#### Johan Commelin (May 29 2019 at 06:00):

We can start recreational/

#### Mario Carneiro (May 29 2019 at 06:00):

outside src/?

Even inside it

#### Floris van Doorn (May 29 2019 at 06:01):

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

#### Kevin Buzzard (May 29 2019 at 06:01):

We can start recreational/

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

#### Floris van Doorn (May 29 2019 at 06:05):

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 (May 29 2019 at 06:07):

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

#### Mario Carneiro (May 29 2019 at 06:08):

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

#### Johan Commelin (May 29 2019 at 06:09):

I'm fine with loosening the naming scheme

#### Johan Commelin (May 29 2019 at 06:10):

But the maintainability standards should be the same.

#### Mario Carneiro (May 29 2019 at 06:12):

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

think AFP

#### Jeremy Avigad (May 29 2019 at 15:39):

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 (May 29 2019 at 15:44):

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 (May 29 2019 at 15:47):

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

#### Mario Carneiro (May 29 2019 at 15:50):

I think I prefer the name refute to classical.by_contradiction

#### Johan Commelin (May 29 2019 at 17:02):

@Floris van Doorn Extra kudos to you!

#### Johan Commelin (May 29 2019 at 17:02):

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

#### Jesse Michael Han (May 29 2019 at 17:12):

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 (May 29 2019 at 17:24):

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 (May 29 2019 at 17:36):

thanks Scott! also, congrats Floris: pasted image

#### Ian Stark (May 29 2019 at 17:40):

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 (May 29 2019 at 17:43):

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 (May 29 2019 at 17:45):

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

Neat.

#### Kevin Buzzard (May 29 2019 at 18:00):

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 (May 29 2019 at 18:03):

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 (May 29 2019 at 18:06):

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

#### Kevin Buzzard (May 29 2019 at 18:06):

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

#### Floris van Doorn (May 29 2019 at 19:39):

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 (May 29 2019 at 19:42):

@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 (May 29 2019 at 19:43):

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% :-)

Last updated: May 14 2021 at 20:13 UTC