Wrote a post on Kripke and Beth semantics in lean 4, and added some features to my blog so that you can see the proof state on hover: https://boarders.github.io/posts/beth.html