Hey , How can one start to proof an algorithm in lean4?

Stream: lean4

[zigzags]

Hey , How can one start to proof an algorithm in lean4. Let's say Insertion sort for example. What are the steps one should take. And if there is a tutorial or some good site for this.

[Will Bradley]

@zigzags You're in luck because this is an example given in the book "Functional Programming in Lean": https://lean-lang.org/functional_programming_in_lean/programs-proofs/insertion-sort.html