> rather than to Lean

Indeed, I don't think anyone should be led to believe that AI can do math on its own without _some_ kind of oracle providing extremely rigorous feedback.