MSが公開したスライドを見たが、実際にできたのは
MS論文には書かれていないTh3.11.5からCor3.12を導く証明
Th3.11からTh3.11.5を導けるかどうかは現在奮闘中

あと、ZFCのLeanによる形式化云々のところで名前が出てくる
Shogo Saitoは、東北大学にいる数理論理学の研究者らしい

https://sites.google.com/view/sendai-logic/past-seminars/2024-4-2025-3