自动形式化

利用AI/机器学习技术将自然语言数学证明或非正式推理自动转化为形式化证明语言（如Lean、Coq、Isabelle）表示的研究方向，旨在降低形式化验证的门槛与成本