Formalizing proof of some conjecture on modal logic

Stream: lean4

[SnO2WMaN]

Recently I formalized the proof of a conjecture of modal logic, "Boxdot Conjecture", on our formalizing mathematical logic project (Formalized Formal Logic).

https://github.com/FormalizedFormalLogic/Foundation/blob/master/Foundation/Modal/Boxdot/Jerabek.lean

I followed the proof of Jeřábek's: https://arxiv.org/abs/1308.0994 (remark: it is already published) and omit the details about this conjecture here.

And it is noted that this conjecture is listed on google-deepmind/formal-conjectures. I don't know it's reported to formalized/proved some problem on this list, but it might be first one. (I don't know how to contribute when proved/formalized on this list, issue opened)

[Kim Morrison]

In what sense is it "10-years unsolved" if there's an arxiv paper from 2013 proving it?

[SnO2WMaN]

Kim Morrison said:

In what sense is it "10-years unsolved" if there's an arxiv paper from 2013 proving it?

I have misunderstood this thing and choosing wrong words. This problem was originally posed in 2009 and already solved by Jeřábek in 2013 (officially published in 2016). I only formalized this proof, not solved, so edited the first message. thanks.