Engineering Automated Proofs in Lean for Arbitrary Types: Tactic Synthesis and Scalable Verification2025年10月10日探讨Lean中针对任意类型的自动化证明生成工程实践，包括tactic合成机制与验证可扩展性配置要点。