Modal logic

Stream: mathlib4

[Leucocholia]

Has anyone tried to implement modal logic in Lean or Mathlib? I'm reading Boxes and Diamonds by Richard Zach and it seems interesting

[Matt Diamond]

You might be interested in this project: https://github.com/FormalizedFormalLogic/Foundation

it's formalizing logic more generally, but includes modal logic

IMHO the docs are a bit hard to navigate but I think this is a good starting point:

https://formalizedformallogic.github.io/Summary/Foundation/Modal/System/Basic.html