Comment by elternal_love

Hmm, is the formal verification through? Lean just asserts no errors in the proof, but like can prerequisites not be fullfilled?