Post

I know it's not particularly exciting for those not obsessed with it, but I just managed to prove my very first somewhat nontrivial theorem in Lean! That is, something outside of Lean4Game, self-written, just for practice.

I defined a single step of bubble sort (basically one pass) as a tail-recursive function, and proved the property that the resulting list/array remains the same length. Took me a while to figure it out and not get lost in the induction steps, but I managed to do it!