Autoformalization

将自然语言数学命题自动翻译为交互式定理证明器（如Lean）可验证形式化代码的AI技术，是连接自然语言数学与机器严格验证的关键环节