Comment by LightMachine

1. I do, but probably not in the current version, since I believe these proofs probably need full closure cloning to be ergonomic.

2. You can express anything actually, because you can clone data, just not functions. So, anything you could implement with datatypes (i.e., without cloned closures), you could probably also prove. But again, people use and abuse closure cloning a lot in Lean. So, how ergonomic would that be? I don't know. It is less about expressivity and more about ergonomics.

3. No, just in the runtime for now. Checking proofs on the GPU will happen when we implement Bend in itself.