AlexDuchnowski / rubiks-cube

A Lean 4 representation of the Rubik's Cube, some proofs about the representation, and a simple solution algorithm.
7 stars 0 forks source link

Any advise would be appreciated: #5

Closed chenjulang closed 1 month ago

chenjulang commented 6 months ago

Check my files: https://github.com/chenjulang/rubikcubegroup/blob/master/RubiksCube/FuncProofs.lean

I'm proving "valid_reachable" and "Thistlethwaite's Algorithm" and so many related lemmas recently. Any advise would be appreciated, because i'm not good at Lean4 Language. :)