You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Formalization of normal modal propositional logic in Lean 4 / Mathlib — soundness & completeness for all 16 logics in the modal cube, finite model property, and decidability. ~11k lines, fully sorr…