My journey with Lean4. Starting with Theorem Proving in Lean 4 during the summer and a math bachelor @EPFL