3 ms·

Disappointing that there's no mention of infinities. How do you teach a computer to think in symbolic terms about Cantor's concepts of infinity? There's no co

Disappointing that there's no mention of infinities. How do you teach a computer to think in symbolic terms about Cantor's concepts of infinity? There's no computational representation for irrational numbers, and barely for rational numbers. Even floating-point representations are a long-standing problems - and integers? Overflows are a problem, even just signed integers are a problem. The pencil-and-paper mathematicians and their symbolic representations of infinities, will computers and AI ever come to grasps with that? i.e. https://www.bbvaopenmind.com/en/science/mathematics/georg-cantor-the-man-who-discovered-different-infinities/ https://www.bbvaopenmind.com/en/science/mathematics/georg-ca...

pirocks 4y ago
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.
hutchisonc 4y ago
The mathlib discussed in the article does include representations of infinite cardinalities; see e.g. https://leanprover-community.github.io/mathlib_docs/data/real/cardinality.html https://leanprover-community.github.io/mathlib_docs/data/rea.... There was also a (now completed) project to prove the independence of the continuum hypothesis from ZFC in Lean; see https://github.com/flypitch/flypitch https://github.com/flypitch/flypitch.
defrost 4y ago
With symbolic computer algebra systems, eg: Magma Computer Algebra System Matrix Groups Over Infinite Fields http://magma.maths.usyd.edu.au/magma/handbook/matrix_groups_over_infinite_fields http://magma.maths.usyd.edu.au/magma/handbook/matrix_groups_... this dates back to the mid 1980s. TLDR; in the same manner that humans reason about infinity: abstractly.
freemint 4y ago
> How do you teach a computer to think in symbolic terms about Cantor's concepts of infinity? All the other answers have been well so i do it tongue and cheek. "With Floating Point numbers"

pirocks 4y ago

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.

hutchisonc 4y ago

The mathlib discussed in the article does include representations of infinite cardinalities; see e.g. https://leanprover-community.github.io/mathlib_docs/data/real/cardinality.html https://leanprover-community.github.io/mathlib_docs/data/rea.... There was also a (now completed) project to prove the independence of the continuum hypothesis from ZFC in Lean; see https://github.com/flypitch/flypitch https://github.com/flypitch/flypitch.

defrost 4y ago

With symbolic computer algebra systems, eg: Magma Computer Algebra System Matrix Groups Over Infinite Fields http://magma.maths.usyd.edu.au/magma/handbook/matrix_groups_over_infinite_fields http://magma.maths.usyd.edu.au/magma/handbook/matrix_groups_... this dates back to the mid 1980s. TLDR; in the same manner that humans reason about infinity: abstractly.

freemint 4y ago

> How do you teach a computer to think in symbolic terms about Cantor's concepts of infinity? All the other answers have been well so i do it tongue and cheek. "With Floating Point numbers"