Claude Code has been super helpful in this; however, I had to do a lot of back-and-forth to verify the output in an IDE and then prompt Claude again with suggestions to fix the proof.
Yesterday, Axiom, one of the model labs working on a foundation model specializing in mathematics, released AXLE, the Lean Engine. The first thing I did was create a Skill so Claude Code can use it as a verifier for Lean code it writes.
Works surprisingly well.