Comment by aureianimus
2 months ago
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.
I haven't come across this before. I will spend time on comparator. thank you very much for the suggestion.