If math is so deductive, why is it so hard to discover new math?

Question

Some considerations:

• The conclusions of much latter/new math may be said to be already existent within the premises of current math
  • The importance of deduction changes depending on if math is said to be invented or discovered
• Some parts of math are inductive and not necessarily deductive
  • Specifically, mathematical operations (deductive) are different from the human activity/enterprise of doing math (somewhat inductive?)
• Discovering new math is distinct from validating math
• Computers and automatic theorem provers: maybe the question need not be about the difficulty of discovering new math for humans but even why is it difficult for computers?

Answer 1

If the rules of chess are so simple, why is it so hard to beat a grandmaster?

The answer is the 'combinatorial explosion'. You have a small and well-defined set of moves you can make at each step. Let's say there are an average of 10 moves you can make each turn. Then in two turns there are 100 moves to consider, in three turns 1000, in just nine turns there are a billion options, and even the computers are starting to struggle.

Some chess games last longer than 250 moves! Some maths proofs extend to thousands of pages. And of course, there are a lot more than ten moves you can make in any one step. The number of options to consider is mind-boggling, and practically impossible by any sort of brute-force search. You find yourself walking lost in a vast unknown landscape where thick fog prevents you seeing more than half a dozen steps in any direction.

You need more than just deduction. You need to build more powerful tools, spot patterns and regularities between one bit of terrain and another, understand how the landscape as a whole works, have a broad idea before you start of where you are going and roughly how to get there, carry the route maps made by all the explorers who went before you, and you need a toolkit of many clever strategies for getting round local obstacles, and then when you set off through the maze towards that goal, you may be able to make steady progress, rather than just walking randomly in circles getting nowhere.

Answer 2

“Doing mathematics” or “discovering new math” is not the same as “giving new formal mathematical deductions”.

Here is an analogy: Why is it hard to write new literature, or new poetry? It’s extremely easy to sit down and write sentences — or to program a computer to write millions of new sentences. The catch is, of course, that those sentences will be very uninteresting.

The same holds in mathematics. Yes, as you say, it’s easy to “deduce” or “discover” new mathematical statements; I just “discovered” the new fact that

693231199129595158083847394455047696598247638918275897185767
× 3789646553083442259894838769031132462258686714508315149522260739
= 2627101224271371669002924770003683951740288901293873531621791047742288186636589219835264858478032122307193763954409693701813

and given a little time I could produce a deductive proof of it in the formal system of your choice. And with a little more thought, I could generate new statements/proofs of arbitrary logical form and complexity.

But this isn’t “doing mathematics” in the sense of mathematical research, any more than writing grammatical sentences is new literature. Of course, one can argue over terminology and definitions, and philosophers of mathematics have done so. You can choose to define “mathematics” as any suitable formal deduction, and in that case, you conclude that it’s easy to discover new math, but hard to discover new math that’s interesting or useful. Alternatively you can say that “mathematics” in the real-world sense doesn’t just mean any formal deduction — that being interesting or useful or similar is also part of what mathematics means — and that’s the sense in which it is hard to discover new math. But whichever viewpoint/terminology you take, it’s clear how the tension of your question is resolved: It’s easy to give new deductions of new facts; what’s hard is doing interesting new mathematics.

Answer 3

I think the premise of the question is false. Actually, it's easy to discover new math.

Here's one way to find some new math. Take a sheet of paper and write down a bunch of "nonsense" equations with one or more letters on each side, like WJ = OF and EEN = T. Next, say that two sequences of letters are "equivalent" if you can change one to the other by replacing letters according to the equations that you just wrote down. For example, with these two equations, LOFTY is equivalent to LWJTY, which is equivalent to LWJEENY (and, of course, that means that LOFTY is equivalent to LWJEENY and LWJEENY is equivalent to LOFTY).

Now try investigating the system that you've created. Can you find some words that are equivalent to each other? Can you find two words which are not equivalent to each other? How can you prove that they're not equivalent to each other? Are there infinitely many words which are equivalent to each other? Are there infinitely many words which are not equivalent to each other? Can you figure out an algorithm to determine whether two words are equivalent to each other?

If you've written down some of these equations and thought about some of these questions, then congratulations! You're (probably) doing math that no human has ever done before, and discovering mathematical facts that no human has ever discovered before.

Answer 4

To elaborate on Nullius in Verba's answer (this started as a comment but became too long!).

You can think of each step in a proof as an application of a valid rule of deductive inference to the axioms of mathematics (e.g., the axioms of ZFC set theory together with the rules of classical 1st-order predicate logic in the most standard foundation). This creates a branching tree structure with the set of axioms at the root of the tree and branches at each node for every applicable rule of inference. Clearly, the tree grows exponentially with every step away from the root.

To find a proof of a theorem T means finding a path through the tree starting from the root (axioms) and ending at T. So why can't we have a computer program that crunches all the possibilities and find this path? For short enough paths this is possible; provers like Isabelle/HOL can already automate proof finding for very simple proofs. For longer paths a brute force search is not computationally feasible due to the exponential growth in the size of the tree with every additional proof step.

In addition, for proving theorems in general the problem of finding the proof path is not just computationally intractable due to finite speed constraints, but actually computationally undecidable. This means that there is no finite algorithm that could, even given infinite computing power, find every theorem. This is due to Gödel-type issues since any algorithm we might suggest is itself representable as a big binary number, and using this number encoding we can define a self-referential and therefore undecidable mathematical statement for that specific algorithm.

A final reason that discovering new math is hard is that it doesn't only involve finding proofs. Mathematicians who create new math do so by gaining some sort of intuitive insight into a mathematical domain and discovering a way to translate this insight into a formal definition. It isn't as if there is some God-given list of mathematical statements that mathematicians need to find proofs for. Rather, they discover interesting conjectures (possible theorems) in the process of exploring their intuitions about a mathematical domain that is considered interesting or valuable.

It is worth noting that the universe of all definable formal systems is much larger than the universe of formal systems that mathematicians actually care about. One of the major creative activities of mathematicians is creating new definitions/constructions that give rise to mathematical concepts/structures. Why choose to focus on some definitions over others, when any definition that is well-constructed is equally valid from a strictly formal point of view? When you listen to mathematicians talk about mathematical research they focus a lot on the questions about which definitions are "most natural" in some informal sense. Again, this points to the fact that facilitating human understanding is the central concern, not merely finding proofs for some pre-determined set of statements.

So proofs in math are not intrinsically valuable but only instrumentally valuable to the extent that they serve the interests of human mathematicians in achieving meaningful insight. Given the progress in AI recently, it could well be the case that in the next 10 years we will have deep-learning based theorem-provers which can find arbitrary proofs in an acceptable timeframe (setting aside undecidability issues). Even then, there would then still be a role for human mathematicians in deciding what theorems are worth proving, coming up with new mathematical constructions to prove things about, and understanding the meaning of the proofs that are generated by the AI.

Answer 5

Math proofs are deductive, but the discovery of math proofs is an abductive process which requires a healthy exercise of expertise and intuition. Mathematical argumentation, like all argumentation, relies on healthy doses of defeasible thought.

Often times, the articulation of an axiom for a theory is a challenging endeavor, and historically a famous example of that is the invention of non-Euclidian geometries which not only involved a new axiom, but the rejection of an old one. The abandonment of the parallel postulate was a great leap forward, but didn't happen for almost 2,000 years.

Theorems often can be complex mathematical objects requiring an extensive number of steps. Also, mathematical techniques themselves have improved from the days of the Ancient Greeks who conducted geometrical activities with straightedges (not rules) and compasses (not protractors). In fact, the Cartesian plane was a revolution in mathematics which let one consider not just the shape of the circle a circle, but a locus of points given by algebraic methods. In fact, at the secondary level, a straight line goes from being something drawn with a ruler to a formula: y=mx+b. That was a technique not used by Euclid. The same can be said of the number 0, imaginary numbers, and a host of new techniques including systems that automate proving hundreds or thousands of mathematical theorems (mathscholar.org).

Also, consider how a single proof itself, like Wiles's proof of Fermat's Last Theorem, might be a tremendously difficult undertaking requiring a lifetime of knowledge across many different subdisciplines of math. From WP:

Wiles's proof uses many techniques from algebraic geometry and number theory, and has many ramifications in these branches of mathematics. It also uses standard constructions of modern algebraic geometry, such as the category of schemes and Iwasawa theory, and other 20th-century techniques which were not available to Fermat. The proof's method of identification of a deformation ring with a Hecke algebra (now referred to as an R=T theorem) to prove modularity lifting theorems has been an influential development in algebraic number theory.

An undergraduate in mathematics would have to research this paragraph just to understand it.

Lastly, for some, mathematical systems can become deeply held beliefs that border on religion. In a famous apocrypha, the followers of Pythagoras are said to have cast the discoverer of the irrationality of root 2 off a cliff in protest. For modern mathematicians, entire careers might be spent and professional reputations staked on beliefs. But mostly, building rigorous mathematical theories from the ground up is a difficult act requiring expertise in the foundations of math, a gift with abstraction, a prodigious memory, and an understanding of how syntax can be meaningfully constructed and used.

Answer 6

There are already many good answers to this question. In particular, Nullius in Verba has described that the complexity of finding the derivation becomes exponentially higher with the length of the derivation itself. And, Avi C has pointed out that finding the proof of a theorem can be undecidable.

I wanted to shed some more light on Avi C's point.

Some simpler logics, like propositional logic, have proof systems which have a property called the subformula property. This means the following: Suppose there is a proof for a statement S. Then, there is a proof of the statement S that only involves applying steps of logical inference only to statements which are structurally smaller than S. (This shows that there is a mechanical procedure to find proofs in such a logic. Since the number of structurally smaller statements is finite, you can just try every possibility.)

Perhaps this is the view of mathematics that OP has in mind. This would mean that the more complex statements in mathematics are simply the consequence of the simpler statements. However, the subformula property does not hold for more interesting mathematical logic, like first-order logic, for example. This means that to prove a simple statement, one may have to derive it from a more complex statement, which in turn means that one needs the creativity to guess what this complex statement is.

We see this manifest in practice in many different ways. Sometimes we need to have a stronger induction hypotheisis to prove something by induction. Other times, we may need to find a clever invariant to prove a certain seperation.