証明可能性論理の形式化のために最近少しずつやっているが，可証性述語が存在する算術が不動点補題を満たし導出可能性条件/形式化された完全性定理などを満たすならば，不完全性定理やLöbの定理などが証明できるという事実をLean4で形式化していた（どうやって可証性述語をとったりそのような条件を満たすかを示すかは一切触れていない）

https://github.com/SnO2WMaN/lean4-modallogic/blob/896246058108e612671e5f0eae4da6d9cc1fad86/ModalLogic/Arithmetic/IT1.lean#L38-L44