AlexDuchnowski rubiks-cube issues - Githubissues

AlexDuchnowski / rubiks-cube

A Lean 4 representation of the Rubik's Cube, some proofs about the representation, and a simple solution algorithm.

6 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Any advise would be appreciated:

#5 chenjulang opened 4 months ago
0
Doubts about "plus_mul".

#4 chenjulang opened 4 months ago
8
Only 2 sorrys left to be proved in "RubiksCubeFunc.lean".

#3 chenjulang closed 4 months ago
1
I think the definition of ps_inv is not very appropriate."ps_mul_left_inv" can be proved like this.

#2 chenjulang closed 4 months ago
1
I proved the ps_mul_assoc, its order should be like this: lemma ps_mul_assoc {p o : ℕ+} : ∀ (a b c : PieceState p o), ps_mul c (ps_mul b a) = ps_mul (ps_mul c b) a

#1 chenjulang closed 5 months ago
3