Comment by gems
13 years ago
How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers? You can't ask the computer to enumerate the solutions for you. You have to reason in a roundabout way, possibly building some abstraction.
Even if there are some branches of mathematics that will be affected by computers, at the end of the day, there will still have to be someone who does the conjecturing, someone with enough knowledge to pose the question to the computer.
> How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers?
Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
Give me an example of how this is done or can be done.
Check out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: http://adam.chlipala.net/cpdt/html/Coinductive.html
I'll repeat what szany and xyzzy123 mentioned: you work at a level of abstraction where infinite data structures are represented symbolically with enough definitional scaffolding to allow proofs to go through.
In a sense, a properly typed program provides a proof of some theorem over infinite data structures. For instance, an instance of a tree (in generic Java) is usually a finite data structure, but the set of all trees representable in Java is infinite. (Handwaving begins) The types prove that certain operations can't happen, like a tree of Strings changing to a tree of Arrays by a node search algorithm, which is a proof about an infinite set.
Essentially the same way we reason about infinite mathematical structures in our heads: we define infinite structures by a finite system of generators and prove things by induction. The computer verifies that your inductive proof is correct.
That is until a computer is capable of reason, which I personally think will never happen. I'm not suggesting some other technology will not be able to reason, but it's not going to be a jumped up Turing machine.
> You have to reason in a roundabout way, possibly building some abstraction.
You're assuming that computers can't handle abstractions.
The only thing I asserted in that comment was that you can't ask the computer to help you (effectively) in a naive search when the space is large or infinite. I'm not familiar with how theorem provers work, so I'm most likely wrong anyway.
How does a computer build abstractions on its own?
How does it build them? That's not a simple question, but it's possible to do. E.g. machine learning is computers building abstractions.
But it doesn't have to do that, anyway, it can provide means for users to build their own abstractions, abstractions that may be useful for them.