Very cool! It seems you've got a great setup. An addition that would be very convincing is going the extra mile and making a comparator setup for your Lean proofs. (https://github.com/leanprover/comparator) This ensures that the AI is not, in any way, modifiying the Lean context in ways that could lead to unsoundness.