Markov Decision Process in Lean4 - L3 Internship