Any activity that can be broken up into sequential steps can be programmed with enough time, smarts, and computing power behind it.
How humans create proofs (from my experience):
1.) Propose a rule (random with a bias towards principles already shown inductively)
2.) Lay out definitions (use natural language)
3.) Do a quick check for counter-examples
4.) Select an approach (ex: pure algebra, using series', using iffs, bias towards what works with similar problems)
5.) Determine what the approach would have to result in
6.) Use all known theorems, identities, and so fourth to manipulate the 'equations', most related manipulators first (by recalling similarities to other proofs) with a hint of randomness, tend towards more simplified states unless it returns to a previously explored, simplified state
7.) If the problem isn't solved return to 6 (many times)
8.) If the problem still isn't solved return to 4 (till no more relevant approaches exist)
9.) Retrace steps, see if the steps within the proof can be simplified
10.) Present steps
All seems quite doable, heuristics for similarities, giant databases of theorems and identities, randomness here and there... of course new approaches to proofs would remain in the domain of humans unless someone fleshed out steps for this, which i'm sure is possible
edit: O, and humans of course 'break the rules' sometimes, where there's room for that (where something is prudent but not necessary) the computers could have a weighted random chance of breaking a rule.
Post has been edited 2 time(s), last time on Oct 13 2014, 1:07 am by jjf28.
Rs_yes-im4real - Clan Aura - jjf28.net84.netReached the top of StarCraft theory crafting 2:12 AM CST, August 2nd, 2014.