Can computers do math? Can they reason?

"Computer intelligence" is clearly a very loosely defined term, to the point that it might not mean anything at all, so it's hard to know if we are there yet, or if we will ever be. A much more practical approach, from my (admittedly very analytical) point of view is to think of the "features" of what we might call intelligence, and see if, or how, a computer can replicate them. Some of those features are trivial (computers can remember things, computers can recognize patterns, computers can do algebra and statistics...), but some are not. One that is particularly tricky is the ability to reason, to logically construct useful truths that follow from more basic true assumptions. Of course, that process has a name: mathematics. Can computers do mathematics, in the sense that mathematicians do it?

The story of mathematics and computers is almost as long as the story of computers. Since very early, it was clear that mathematics involved a lot of "mechanical" steps, going from some propositions to other propositions applying clear rules of logic, and that computers could help with that. Many different systems to help mathematicians appeared, and even some old theorems that have resisted proof for centuries were solved with the help of computers, like the well known cases of the four color theorem and the optimal packaging of spheres. Anyway, computer assisted proofs like those have an undeniably sense of inelegance (proving old complex theorems just by exhausting very long list of potential cases, without giving any insight or any useful technique that could be applied somewhere else, is somehow disappointing), and some would even say they are "not real math". More importantly, the list of important theorems in which "computer assisted math" could really help turned out to be rather short, and even Moore's law has not helped: many of the success stories about computer assisted math come from as early as the seventies and eighties. It seems computers are not very good at "reasoning", or at least it did until quite recently.

There are very fundamental advances that are taking place right now in how computers can do math, and by extension their very ability to "reason". They are clearly not as visible as advances in other areas, but in my opinion are at least as important. Both for maths and for computers.

Mathematicians are great at working with abstractions, so it's no surprise they tried to "abstract" the very concept of logic. Without going too much into the history of mathematics, let's just say that by the end of the ninetieth century there was a deep concern about formalizing logic as a way to make the foundations of maths more solid, as illustrated by the famous Hilbert's program. It turned out that things were a lot harder than they looked; G?del killed all hopes of ever finding solid grounds, and things only got more interesting from then on. There isn't a "perfect" set of concepts nor a "perfect" logic that could be used to express and solve all interesting problems using propositional logic. This, rather than having the devastating effect that some people feared at the moment, actually created a much larger interest in formal logic, proof theory, etc., which gets us to where we are today: different systems implement different formal logics, and can be used to either look for or help validate mathematical proofs. But the path that has to be followed from the fundamental axioms of the logic to the useful concepts required to express and proof real, interesting mathematics is so vast that some kind of shorcuts are always needed (typically, in the form of "telling the computer" about concepts and facts not directly deduced by the computer, thus making the computer maths at most as good as what it is being fed, or in other words, having the computer do math "with things it doesn't really understand")

Fortunately, there is an alternative, which is an extremely exciting fact (unfortunately, that alternative might be far from perfect, but the jury is still out on that). There is something called "constructive logic", which, very roughly speaking, means that only mathematical objects for which an example can be provided are considered, and in particular, only propositions for which a proof exist are considered valid (thus rejecting the traditional "law of excluded third" that says that any proposition is either true of false, which in turn invalidates "proof by contradiction"). "Constructive logic" is weaker than other types of logic (there are many important theorems for which a constructive proof does not exit yet), but it has very fundamental advantages when it comes to computer implementation. It is closely related to type theory (via the so-called Curry–Howard isomorphism) and it has been efficiently implemented in automated proof assistants. This means that large bodies of mathematical knowledge could be formalized in this "constructive logic" and "implemented" in those automated proof assistants (or "proved", which in this case is the same!), making them available for anyone willing to use that mathematical knowledge to try to prove further theorems, which is the old dream of computer math pioneers.

Actually, not a dream anymore, but something that is happening as we speak. All the required pieces, coming from many bright mathematicians, have been put together by Vladimir Voevodsky in his "univalent foundations" program, while the computer scientists provided the required infrastructure (like the Coq proof assistant / computer language, Isabelle HOL, Twelf...), and in the last few years more and more areas of mathematics have been formalized. And it's there for anyone to use it, available in github no less! Little by little, the initial focus of "showing that is was possible" is turning towards practical applications, and creating a formal proof in one of these systems is slowly becoming the golden standard for validation of mathematical works (peer reviews of papers are fine, but some areas of mathematics are so specialized that very few people can understand, let alone verify, other people's work, as shown for instance in the famous case of Andrew Wiles initial proof of Fermat's last theorem, that contained some errors that took months to detect and years to solve!). 

Does all of this mean that computers can reason? Not really, or rather not yet, in my view. The typical way to work with systems like Coq involves significant manual intervention: you provide some facts, let the computer deduct as much as it can from them by itself, and when the computer cannot go any further you suggest some strategy to try ("tactics", in Coq lingo), and then let the computer deduct as much as possible again, and repeat that cycle until you prove what you were trying to prove (thus the name "proof assistant", although the instructions created by that automatic reasoning and those strategies become an actual program in the Coq "programming language"). But we are starting to understand what type of "reasoning" computers can and cannot do, and we are actually using that reasoning ability for practical purposes, albeit in a very controlled and limited environment. And anything that is actually used (by some of the brightest minds in the world, no less!), no matter how immature and limited it is, is already on the way to reach its full potential. Which in the case of computer reasoning, it is no less than to be a fundamental feature of "real" artificial intelligence.