I have a strong tendency to seek automation. Perhaps it's just laziness on my part, but I like important but routine business to happen automatically, without me putting a lot of work in.
Of course, this usually means that I or someone else put a lot of "meta-work" in, for it is inevitable that the ingenuity required in automating a task is much greater than simply performing it. but there is nothing like having a well-designed tool that does your work for you. It's every person's dream to lead a purely hedonistic existence where every wish is instantly granted; by definition, there is nothing better!
Humanity as a whole tries to move in this direction, and automation is of course prevalent in modern life. We have things like automatic billing and direct deposits, spell check, speed dial, T9, etc., as well as much more sophisticated systems. Undoubtedly in some cases there is still some human involvement behind the scenes that makes the automation automatic, but the joy of being a consumer of computer+human+other automation is that whatever is supposed to happen just happens, without us ever thinking about it. and if it's really done right, then we don't even (realize it happened); we simply (don't realize) that it didn't happen. Perhaps being able to take an automated task for granted is what makes automation so wonderful.
Automation is not a new idea, and it isn't specific to software. Aqueducts, the printing press, and the cotton gin come to mind as obvious historical inventions that automated particular tasks. and there are millions, each one making life a little easier.
but mostly I want to talk about computer programs. Software can automate an amazing number of things, from building an entire web site to computing integrals. As someone who spends a lot of time writing code, significant effort in my life is put toward this type of automation. In my case, the goal is to automate mathematics.
The simplest reason for using computers to study mathematics is that they free us of the tedious computations needed to produce data. Once we have a program to generate the objects we are studying, we can let the program run, and (if it is sufficiently fast!) it will do all the work for us. With enough data (say, the first 10 or 20 terms in a sequence of integers), we often can see the general pattern. For example, what is the general term in the following sequence? 2, 7, 14, 23, 34, 47, ...
Well, sometimes finding the general pattern isn't so easy. so another common use of software is to manipulate the data into something that a human can analyze and hopefully recognize. Visualization plays a big role here: Humans are very visual creatures, so it is incredibly useful that software can automate putting data into a form suitable for human consumption.
If the human fails to understand the data visually, then software can automatically fit the data to several different forms (or ansätze) and look for a match. I can't help but mention the Mathematica symbol FindSequenceFunction, which does precisely that for sequences. (This function hasn't lost the luster of a new toy for me yet, and I still get excited every time it identifies a sequence for me.) Perhaps the sequence is given by a polynomial, or perhaps by a linear recurrence of a certain type. If the experimental data can be generated by a function with fewer degrees of freedom than the data (for example, a polynomial of degree 10 correctly reproducing the first 20 terms), then it is a good bet that the sequence has been identified.
Experimental mathematicians use the preceding techniques every day, often with great success.
Let's take it one step further, though, because there is much potential for additional automation: Wouldn't it be great for software to automatically conjecture the answer to a question posed in English? For example, "How many words of length l in the free group on n generators collapse to the empty word when adjacent inverses are canceled?" This isn't as crazy as it might sound. The computer needs to parse the input, of course. Once it has done that it can start generating data naively. Successive terms in this particular sequence are more and more time-consuming to produce, because there are a lot of words to check. but perhaps the software starts to look for shortcuts in the computation. Perhaps it generalizes the problem so that relationships can be identified to other integer sequences that weren't directly requested. Perhaps it can use the data it has already generated to conjecture a faster way of computing terms. Perhaps it can do all these things that currently require human assistance. Then it finds it can generate lots and lots of terms for each n, it experimentally discovers the form for each n, and finally it finds the relationships between these forms to give an answer.
We're not quite there yet, but it's not crazy to imagine that we'll be doing this sort of thing regularly in few decades with software that doesn't just compute in lots of different areas of mathematics but that "knows" how they relate to each other.
and why stop there? Why not have the software automatically generate a proof of its new conjecture?
In fact, why doesn't the software just ask the question to begin with?
Well, I'm not sure exactly what that means. There are of course many many mathematical questions we can ask, but most of them are very very dumb. What makes a question interesting is something that I don't see immediately how to relegate to automation. There is a large element of creativity and aesthetic that goes into choosing a question to ask, and creativity (as distinct from randomness) is not straightforward to automate. In most of the automation that I do, creativity is not an issue; my programs generally accomplish relatively narrow tasks in deterministic ways. However, there are some remarkable examples of "creative automation". David Cope's experiments in musical intelligence come to mind.
Barring creativity, we can always use the brute force approach: Generate all truths within an axiom system by recursively applying every applicable axiom to every known truth. We don't need to know which questions are interesting, because we can tell which answers are interesting — the theorems that are nontrivial yet widely applicable. Sufficiently powerful computers could comb through vast numbers of theorems in all sorts of axiom systems and find interesting ones to report to us. Every morning over breakfast we would browse a digest of all the interesting theorems discovered the previous day, and I think there would be many — far more than a typical arXiv digest.
and very quickly we would lose interest, the same way we have no interest in picking up a random technical paper in a field we know nothing about, because it is completely meaningless to us. It's not challenging or engaging to try to keep up with a slew of computer-generated papers in computer-edited, computer-refereed online journals! so humans would stop paying attention, and the computers would go on proving theorems for themselves in their own mathematical ecology and awarding computer-(Fields Medals), from their perspective obviating human mathematics.
Where does that leave us humans? Maybe it would be nice to have around a humongous searchable corpus of computer-produced lemmas and theorems, so that next time you need an ugly technical lemma to prove your gorgeous theorem you can just find it in the database and say, "Thus Lemma 11A15.267229635085 applies, so we have proved the theorem." but that feels like cheating, because probably the computer already proved the theorem too. Then we either must require the computers to discard the "nice" theorems and only keep the ugly ones, or just raise the bar for ourselves that much higher and hope that there are some people smart enough to find results better than machines.
The same problem appears on the larger level of human effort as a whole... Perhaps eventually no one will need to grow food or cure disease, because these too will be automated. Perhaps novels and films and symphonies will be generated on the fly. Once we have automated life, then what? If everything just happens for us, there will be nothing to do but enjoy it, and quickly we will be bored with our newfound omnipotence! Somehow by solving all our problems we will have created a new one.
Even though complete automation seems to be our goal, I think it's not actually what we want, even if it is possible. I don't think I'd wish for automatic writing or reading of this post. We like to be involved. Part of the reason I write code is that I enjoy it. Certainly I'd rather discover a theorem for myself than read it in a book. We don't want to replace our own creativity with automation; we want to augment it with automation.
What this suggests is that the goal of mathematics is not to produce theorems — it is to build understanding. Analogously, the main goal of life isn't to live easily but to experience being alive. Therefore we should automate only until it interferes with a more important objective, stopping far short of automating everything.
Fortunately or unfortunately, the world still has plenty of problems, so I suppose we're not in danger of soon automating away our lives and our mathematics, and that we'll cross that bridge if it exists.