Zulip Chat Archive

I've been looking at formalizations of Modal Logic, however the most relevant ones I can find are some papers using Lean3 (Notably the ones by Bruno Bentzen 2021, Jiatu Li 2020, & especially Paula Neeley 2021).

From what I can tell, Paula Neeley's formalization of DEL was in MathLib. I believe Mathlib was then converted into Lean4, however I can't find it in there.

The only Lean4 logic I've found so far is https://github.com/FormalizedFormalLogic/Foundation, though I can't tell if this is in Mathlib since I'm still pretty new. This also doesn't cover S5 etc as far as I can tell.

I.e. If I want to use DEL will I need to expand on the above work / translate the Lean3 works into Lean4? I'm fine with doing so I just want to make sure I'm not doing unnecessary work.

Yaël Dillies (Oct 29 2024 at 13:58):

Paula Neeley's thesis does not mention that their formalisation was upstreamed to mathlib. And indeed I don't remember such an upstreaming ever has happened.

Yaël Dillies (Oct 29 2024 at 14:00):

FormalizedFormalLogic's authors have tried to upstream their project to mathlib, but this has kind of stalled because of a mismatch with mathlib's philosophy of having very general and reusable objects

Yaël Dillies (Oct 29 2024 at 14:00):

I hope we will resolve this so that we can get their project in mathlib. But it's a lot of effort

Ward (Oct 29 2024 at 14:04):

Ah I think I made the assumption based on her giving a presentation at the LeanTogether2021, but I'm not even sure how to find whether or not something is in Mathlib.

On the other-hand, I remember Jiatu Li giving a presentation where he believed Bruno Bentzen's work to be in MathLib, but again Idk how to check for that and he could've been mistaken.

Yaël Dillies (Oct 29 2024 at 14:09):

We have plenty of tools to search mathib. My favorite is #docs, but it requires you to know the name of the lemma/def you are looking for. Else you can use #loogle, #moogle or #leansearch