Rubik's cubes discussions

Stream: general

[Utensil Song]

Announcement: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Rubik's.20cubes

[Utensil Song]

@Violeta Hernández Interesting work, particularly the constructive approach. Reading the future work section on README reminds me that I've long wished for On the nxnxn Rubik's Cube and alike to be formalized in Lean, which seems to be the general case. As the 3x3x3 case has been worked on from various angles. Wonder if similar goals also interests you.

[Nir Paz]

I haven't looked at the code yet, but there are also lots of interesting things to do with 3x3! For example it was only recently proven that every even position (even number of quarter turns) is a commutator, and if I recall right, the proof is pretty simple. It could be cool to computably prove this.

[Violeta Hernández]

Utensil Song said:

Reading the future work section on README reminds me that I've long wished for On the nxnxn Rubik's Cube and alike to be formalized in Lean, which seems to be the general case.

This is really cool! I'm glad there's actual literature on the mathematics on Rubik's cubes.

[Violeta Hernández]

The future work section was meant less as "I will do this in the future" and more as "this might be fun to do if you're interested". This was a pretty time-consuming endeavor and I don't think I'll have the time to follow it up in the near future.

[Violeta Hernández]

A main difficulty with the general nxnxn case is that my equivalence of "pieces represent both stickers in a Rubik's cube and their positions" doesn't work anymore. There will generally be various pieces with the same stickers on them. As a consequence, there are more possible solved states.

Even cubes have the extra difficulty that they can be "rotated", whereas odd cubes always have their centers fixed in place.

[Violeta Hernández]

I actually think the 3x3x3x3 case might actually be simpler, since a lot of the concepts generalize straightforwardly.

[Daniel Weber]

I wonder how hard it will be to provably implement the Schreier–Sims algorithm to automatically solve these kinds of problems. It will probably require native_decide

[Violeta Hernández]

Oddly enough the most computationally expensive part of my code is the Stickers code for inputting a Rubik's cube manually. Array.map seems to be the bottleneck - I had to raise maxHeartbeats to a million for a particular proof.

[Violeta Hernández]

The proofs regarding the algorithm itself were relatively quick.

[Violeta Hernández]

Oh wait, you mean whether it'd be feasible to use Schreier-Sims to find the algorithms for permuting/flipping edges and corners automatically?

[Violeta Hernández]

That's an interesting question. There's really no need for it in this 3xx33 case - there's only four explicit algorithms required and I found them by either using a solver or asking my cuber friends. And I imagine that in the general nxnxn case, you could also just find a few families of algorithms and hopefully they'd work the same for center pieces in different layers.

[Daniel Weber]

In GAP, for example, you can directly input the permutations on the stickers the turns represent, and it can compute the order for you: https://web.archive.org/web/20240410065206/https://www.gap-system.org/doc/Examples/rubik.html . I'm wondering whether that could be done in Lean, although I agree that there's no need for it here

[Violeta Hernández]

Computational group theory is something I know little about... but I'd also love seeing it in Lean :smile:

[Utensil Song]

Having skimmed the code, I would like to share that it's well organized clean code, well documented, reminiscent of Mathlib quality, yet on such a concretely perceivable object (Rubik's Cube). Reading the code is a rather pleasant experience.

[chenjulang]

Amazing！！！I want to know if it can be used to prove that Thistlethwaite's algorithm has less than 52 moves？

[Violeta Hernández]

That requires lookup tables in the millions of moves. So it would almost definitely require native_decide. But in every other regard, it should be possible.

[Violeta Hernández]

I didn't actually introduce any API for the quarter/half turn metrics, but that should be pretty easy :smile:

[Violeta Hernández]

Being able to prove any nontrivial bounds on God's number would be a pretty cool project

[Bhavik Mehta]

Something like https://www.ryanheise.com/cube/human_thistlethwaite_algorithm.html could be cool, the cases seem simpler in most situations

[Siddhartha Gadgil]

I was going to mention that @Bhavik Mehta taught me a cool way to generate proofs instead of using native_decide when I saw he is on the thread. I will let him expand on it.

[Bhavik Mehta]

I learnt it from Mario! Or more specifically, from understanding how he wrote norm_num in Lean 3. I'm not completely sure how the ideas there transfer nicely here, but I will think about it.