この記事では、自然言語で書かれた数学定理や証明を、Lean 4のような形式言語に自動で翻訳するための新しいフレームワーク「ProofBridge」が紹介されている。従来の手法は、定理の翻訳と証明生成を別々に行う二段階プロセスに依存していたため、真の証明の自動形式化との間に根本的なギャップが存在していた。ProofBridgeは、自然言語（NL）と形式言語（FL）の定理・証明ペアを共有の意味空間に統合する共同埋め込みモデルを中心に構築されており、セマンティックに関連するFLの例を利用して翻訳をガイドする。このアプローチにより、証明の自動形式化において、さまざまな強力なベースラインと比較して改善が見られ、特にセマンティック正確性と型の正確性が大幅に向上したことが実験結果で示されている。