I believe Lean handles proofs about cardinality and infinities just fine. I'm not sure what kind of computation you want to do with infinities that current computers can't? Can you elaborate? Like sure I can't represent any arbitrary real but like that's never a problem in practice. And Mathematica like software can get pretty close to representing any computable real.
No comments yet.