Explantion: x is a 0/1 matrix of live cells.

    0+':x  -> "sum each element with one to the left
               (0 left of the first)"
    1_x,0  -> "drop first, add zero at the end"
    
    (0+':x)+1_x,0 -> "sum each element with the one
                      to the left and the one to the
                      right (sum of previous expressions)"

    a:2{+...}/x -> "do that; transpose; do that; 
                    transpose again, and assign to a.
                    2{}/ means 'do twice'"

At this point, "a" has the same shape of "x", but in every element is the sum of the elements of x from that location, one above, one below, one left, and one right.

    4=a     -> "1 where a=4, 0 otherwise"
    x*4=a   -> "1 where x is 1 and a=4, 0 otherwise"
    a-x*4=a -> "decrease a from 4 to 3 if x=1 in the 
                that place"
    3=a-x*4=a -> "1 where one has 3 neighbours"

So, if x is a 1/0 matrix "life x" does one iteration of Conway's game of life. And "1000 life/ x" would seek convergence or return to first state (but no more than 1000 iterations).

There is code golfing here; It would have been purely readable K code if it wasn't golfed. But it would also have been two to three times as long.