Claude Code Skill to write better Lean4 proofs

I have been getting into Lean4, mostly playing around with writing proofs for properties of distributed software systems.

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.