Is there any theorem related to the existence proof of Rubik

Stream: Is there code for X?

[chenjulang]

Is there any theorem related to the existence proof of Rubik's cube solution?
Something in group theory, maybe.
Something providing an existence proof and list of solutions. It doesn't matter whether it's in lean or not.

[Johan Commelin]

Can you write down the precise theorem statement that you are after?

[chenjulang]

No, i cannot even state the theorem

[chenjulang]

I was thinking Mathlib may has something to do with Rubik's Cube

[chenjulang]

Something in Group Theory, and i can climb on it

[Johan Commelin]

Can you state the theorem informally? What is "the existence proof of Rubik"?

[chenjulang]

Maybe what state of a cube can be solved? What is the Iff (Necessary and Sufficient Condition).

[chenjulang]

And its most complex moves is under 20(or 26), I was thinking this can be proved.

[chenjulang]

All the movements of a cube can be descriped in a "state graph", right?

[Johan Commelin]

chenjulang said:

And its most complex moves is under 20(or 26), I was thinking this can be proved.

This is something that can be stated in Lean.

[chenjulang]

Great!

[Johan Commelin]

chenjulang said:

Maybe what state of a cube can be solved? What is the Iff (Necessary and Sufficient Condition).

How do you want to describe the possible states. You can not simply list all solvable states. Because that list would be gigantic.

[chenjulang]

emm...Yeah, but we dont need to list all the "Perm n"(for example n=100). We may find the road to the goal only, maybe?

[chenjulang]

And considering the most complex road is less than 26 moves, it is not really really big , right?

[chenjulang]

i know it is hard even in traditional maths

[chenjulang]

Something about providing and proving an algorithm. (something called Kociemba)

[Johan Commelin]

chenjulang said:

emm...Yeah, but we dont need to list all the "Perm n"(for example n=100). We may find the road to the goal only, maybe?

In that case I don't know what the statement is that you are after...

[chenjulang]

i dont know either. I think i was looking for an algorithm to solve rubik's cube in lean. And Lean is good at proving things, it may be able to prove the algorithm feasible.

[Johan Commelin]

Proving the existence of an algorithm is "easy", because "brute force" is an algorithm that works. But if you want an efficient algorithm, then this is going to be a really hard project.

[Jeremy Tan]

For a start you might want to prove that the Cube can be solved in 52 moves (Thistlethwaite's)

[chenjulang]

Ok, thanks for advising :smiling_face_with_hearts:

[Damiano Testa]

The size of the group generated by moves allowed in the Rubik's cube is

43252003274489856000.

This is therefore also the number of solvable configurations. While this number is much smaller than

48! = 12413915592536072670862289047373375038521486354677760000000000

it is still probably not very practical to simply list all the solvable elements and argue on them separately.

[Damiano Testa]

(Information taken from Wikipedia.)

[Kim Morrison]

It would be lovely to implement Schreier-Sims!

Here's a 1-page version of solving the Rubik's cube (=understanding a subgroup of S_n given by generators): https://www.math.toronto.edu/~drorbn/Talks/CUMC-0807/NCGE.pdf

It would be tricky to set up nicely, but not particularly harder than Gaussian elimination or Smith Normal Form.

[Matt Diamond]

There was some work done on formalizing the Rubik's cube group in Lean 3 by @Kendall Frey: https://github.com/kendfrey/rubiks-cube-group

[chenjulang]

(deleted)

[chenjulang]

Try this too, this is in LEAN4.
https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Rubiks.lean

[chenjulang]

And this:
https://github.com/AlexDuchnowski/rubiks-cube/tree/main/RubiksCube

[chenjulang]

image.png

[Kim Morrison]

Scott Morrison said:

It would be lovely to implement Schreier-Sims!

I couldn't resist: branch#schreier_sims has the basics of the Schreier-Sims algorithm (algorithm is there, some sorries about invariants needed in the algorithm, and none of the theorems about it).

It can cope with the Rubik's cube, computing the size of the group correctly just being shown the generators, and it can determine membership. The data structures would need a little updating in order to solve the word problem, but the computation is already happening.

It would be lovely to get this polished up and usable, but I probably won't do this myself. If anyone would like to adopt it (it could be a great project for someone?) please do. I'm happy to talk through what should be done.

[Kim Morrison]

It has a partial step in the algorithm that would be easy to make total. It would be fun (but perhaps unrealistic?) to see if Lean could compute the size of the Rubik's cube group by rfl!