ulamai/ulamai

UlamAI是一个开源的Lean定理证明器，结合大型语言模型引导推理与Lean验证，能够生成机器可验证的Lean4证明。它支持从自然语言提示生成证明，并集成代码生成模型进行定理形式化。