|
|
|
|
|
|
by chaitanyya
105 days ago
|
|
|
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. |
|
|