[sebzim4500]

>How do you make sure that the LLM doesn't reward hack a proof using these workarounds?

I'm not sure what you mean exactly? There is no soundness issue here, the fact that `sqrt -1` is defined to be 0 does not have any impact on what statements about `sqrt x` can be proved when `x` is positive.

It just means that if you are working on an intermediate step of a proof and you need the result that `sqrt y >= 0` you don't need to provide a proof that `y >= 0`. If you wanted an intermediate result that `(sqrt y) * 2 = y` then you would still need to provide a proof that `y >= 0`, though.

[munchler]

If sqrt -1 = 0, then (by squaring both sides) -1 = 0, which is clearly unsound.

[sebzim4500]

Right but there isn't a theorem saying `(sqrt x)^2 = x`, there's a theorem saying `x >= 0 -> (sqrt x)^2 = x`

[munchler]

Ah, that makes sense. Thank you. As long as every use of sqrt has such a condition.