[aureianimus]

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.

[colin7snyder]

I haven't come across this before. I will spend time on comparator. thank you very much for the suggestion.