Provability logics

Stream: Is there code for X?

[É Olive]

I'm interested in proving Löb's theorem. Are there any encodings of provability logics (e.g. Gödel–Löb) into lean? Even other modal logics (e.g. K, S, S4, K4) would be somewhat useful to me.