A few months ago I decided to try formalising some old mathematics olympiad problems in Coq. Part of my motivation was to get a sense for how much work would be involved in proving something slightly non-trivial but still very elementary. I managed it, but it was _a lot_ more work than expected (results here: https://github.com/ocfnash/imo-coq).

Partly based on this exercise, I think that while it is possible that mathematics may go the way of chess, so to speak, it is a lot more distant than the ten years mentioned in this article.

I strongly support, very much hope, and even expect, that the use of proof assistants may become mainstream in mathematics within a generation or so but I think it is impossible to guess the exact role they will play accurately.

Reusing the notation of my post, here's how the formula arises.

The argument based on counting cells that are either row/column good/bad requires the following of the parameter k:

  1. k-1 < r/m
  2. k-1 < c/n
  3. k−1 < cr/(c(m-1) + r(n-1))

  1. k <= ceil r m
  2. k <= ceil c n
  3. k <= ceil cr (c(m-1) + r(n-1))

  k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1)))

  * ceil r m = ceil (cr) (cm)
  * ceil c n = ceil (cr) (mr)

  * min (ceil x y) (ceil x z) = ceil x (max y z)

  k <= ceil cr (c(m-1) + r(n-1))

Without knowing anything about k except that k-1 < r/m, I counted how many cells are column-bad for this value of k. By the pigeon-hole-principle argument in the post this is at most c(m-1)(k-1) cells. Similarly, and still knowing nothing about k except that k-1 < c/n, I count how many cells are row-bad for this value of k and see that it is at most r(n-1)(k-1). Combining these two I know that as long as we have k-1 < r/m and k-1 < c/n the number of cells that are either column-bad or row-bad (or both) is at most:

  * c(m-1)(k-1) + r(n-1)(k-1)

  * c(m-1)(k-1) + r(n-1)(k-1) < rc

And then solve this to get the formula for k. Of course when expositing it in the post, I _start_ with the formula which perhaps makes things seem mysterious at first, but I thought was efficient.

I'd say that the exposition in your post is very fitting for the purpose of proving it. The most elegant proofs are usually not the most enlightening.

I was able to find a basic example of the natural numbers and the operation `plus` in both languages, and it seems like the structure is quite similar.

Coq:

   Inductive nat : Type :=
     | O : nat
     | S : nat → nat.        (* S stands for successor *)

   Fixpoint plus (n : nat) (m : nat) : nat :=
     match n with
       | O ⇒ m
       | S n' ⇒ S (plus n' m)
     end.

Lean:

   inductive nat : Type
   | zero : nat
   | succ : nat → nat

   def plus : nat → nat → nat
   | m nat.zero     := m
   | m (nat.succ n) := nat.succ (plus m n)

The majority is convertible, though. If I had to make a programming analogy, it would be like converting between C++ and D, or different Lisp dialects. The difference is bigger than Python 3 vs Python 2, but less than F# vs OCaml. Clearly possible, in a sense, and if you can read one language, you can read the other, but automatic conversion is just out of reach due to edge cases.

So computers can aid us in verifying our work--but ultimately we aren't interested in determining all the possible logical theorems. Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely.

It's a subtle difference, but for computers to solve that problem requires for them to have a certain understanding of humans and our goals with science.

I think that's more than 10 years out.

For a long time, they didn't like irrationals, so anything involving those didn't count as mathematics. Zero took a long time to be accepted, starting in India. Negative solutions of quadratics were illegitimate until astonishingly recent days. Complex numbers were accepted even more recently. Greek geometers knew they lived on a sphere, but spherical geometry was too unpleasant to contemplate until quite recently, when it turned out interesting theorems could live there.

People worked outside these boundaries all along, but what they wrote didn't catch on. Laplace's transforms were ignored and forgotten until they were needed to shore up Heaviside's extremely practical D operator. Complex numbers turned out to be needed to for electromagnetics. Once people got deeply into the topic, they discovered beauty and then mathematics accepted them.

Mathematics is the world's largest and longest-running effort to produce a collective work of sublime beauty. What is beautiful goes in, what isn't dies with its creator. New forms come to be seen as beautiful as they are shown to open new vistas to explore, but very slowly.

Note that this is more or less a myth.

> Greek geometers knew they lived on a sphere, but spherical geometry was too unpleasant to contemplate until quite recently

Astronomers did a huge amount of sophisticated spherical geometry, from Mesopotamians through e.g. Hipparchus and later Ptolemy, then Arabs/Persians, Indians, medieval Europeans, right down to the present.

I assume yo have no problem with the rest.

That's just empirically false though. Take the "perfectoid spaces" mentioned in the article. Do you think mathematicians are interested in them because they "explain the patterns in the world concisely"? No, they're interested in them because of their mathematical significance, and their applications to problems within mathematics. Mathematicians are not physicists.

These external problems ultimately are about explaining patterns in the world.

I'm just saying you'll never replace the relationship between the mathematician and the physicist by simply replacing the mathematician. Instead, you'd have to replace the whole academic process, making fully autonomous universities. In which case they're still not interested in exactly same problems unless they are constructed in the same way (which they are not, since they are not human).

I'm not saying that computers won't be able to aid us with these meta-theories which help push our main theories forward. So I do agree that they can come up with some theory, but not all of it, and not most of it.

that's maybe a description of how mathematics is used, but that isn't a description of mathematics.

We are transitioning surprisingly fast from kinda explaining stuff to automatically and systematically advancing exclusively through rigurously formalized proofs.

Microsoft Research seems to have done some exciting things with provers over the years - Z3 is another significant program. All under the direction of Leonardo de Moura, notably.

Citation needed. I can make a perfectly reasonable Isar-style declarative proof in Lean. Just because most users of Lean choose not to do this doesn't mean it can't be done. I should mention that users are more willing to write imperative proof code instead of declarative in Lean is because 1) the interactive debugger is responsive and easy to use, and 2) writing a nicely structured declarative proof is more work than an imperative proof.

Constructive mathematics should be more of a thing too.

Many years ago, around 1980, I headed a project to build one of the first program proof of correctness systems. (It's on Github now, about two-thirds working with modern compilers.)[1] We succeeded, but it was just too hard to use. And, back then, really slow. As in 15 minutes to hours.

We had two theorem provers. One was what's now called an SMT solver - it could prove theorems with addition, subtraction, multiplication by constants, equalities, inequalities, and the Boolean operators. It could also accept rewrite rules, which it accepted as true.

Because allowing users to input rewrite rules made it easy to create false proofs, we required that the rewrite rules be proven using the Boyer-Moore theorem prover, which is a pure constructive system.[2] Then the theorems could be transferred to the SMT solver and used there.

One of the things we set out to prove were the "axioms" for arrays. There are four, credited to McCarthy in his classic 1962 paper. But we wanted to prove them from a theory of constructive arrays. In Boyer-Moore theory, we defined arrays as sorted lists of (subscript, value) tuples. And then we set out to prove the classic four axioms for arrays with machine proofs.

Which we did.[3], starting at line 3372. That file is the Boyer-Moore theorem prover grinding its way up from a very low base of number theory to the theorems we needed for our program proving system. (On a modern computer, in seconds. Took 3 hours on a VAX in 1980. We just didn't have enough engine for this stuff back then.) In that notation, "(selecta A I)" means A[I], and "(storea A I V)" is array A with A[I] replaced with V. After some struggles, we got the the prover to find a way to prove that.

But it's ugly. There's lots of case analysis, which mathematicians hate. We didn't get to redefine "equal", so we couldn't have abstract sets. We had to have ordered lists of tuples, which meant all the fussyness of updating an ordered list representation and proving that was sound. But it all worked.

So I submitted this to JACM, back when that mattered. It was rejected. The comments were along the lines of "I don't like having something that ugly at the foundations of computer science". The reviewers all agreed it was valid, but they just didn't like doing it that way, in an automatic but inelegant way.

Looks like the author of the original article here is still having that problem.

Good times back then. But we were way ahead of our time.

[1] https://github.com/John-Nagle/pasv

[2] https://github.com/John-Nagle/nqthm

[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

    True or false – if x is a real number,
    and x² − 3x + 2 = 0, then x = 1.”

    My answer “False – set x = 2.

    Lean: “OK, so it now suffices to prove that
    (a) 2² − 3×2 + 2 = 0 and that
    (b) 2 ≠ 1.

So, you rather give your users something bug free in which they can express the basics of numbers, starting, for example, with the Peano axioms (https://en.wikipedia.org/wiki/Peano_axioms) (and that isn’t even the bottom of the stack; an even more basic system could replicate Principia Mathematica (https://en.wikipedia.org/wiki/Principia_Mathematica))

It’s a long road from there to high school math and an even longer one to mathematics research, so users not only will be able to do the above, but they will have to, if they want to do something at the front of mathematics.

I (I'm not the only one) think that Hilbert was wrong.

Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard.

Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already.

We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever.

Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof?

Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system.

Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering.

Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?

Earlier this year, Patrick Massot, Johan Commelin and myself formalised the definition of a perfectoid space in Lean. I am getting invitations from across the EU to speak in mathematics departments about the work. Serious piece of research, or elaborate PR stunt? Maybe both."

They may be learning more than programming from their contacts in the computer department. Is always much easier to get something out there when it is fully buzzword compatible.

> In April, Christian Szegedy from Google told me that he believes that computers will be beating humans at math within ten years.

I wonder whether automated mathematics software would really be able to compete with humans at explaining how areas of mathematics fit together and what roles different mathematical objects play.

I'm not a mathematician so sorry for the simplistic example, but for example, would automated mathematics software be able to do something like (a) invent the complex numbers (i.e. as an object in algebra -- a "field extension" of the reals), and (b) also make a statement like "these are useful for modeling cyclical/oscillatory behavior"?

From my experience the track record of Outlandish Claims Made by People Having Vested Interest in Casting Them is rather poor. In fact, I can not recall a single one that was accurate.

Kevin also explained live in his talk that his main motivation for his recent interest in interactive theorem provers is a very bad experience he had a few years ago refereeing an important research paper by some famous mathematicians. That experience very much shook his faith in the ability of humans to do correct deep mathematics... I suppose from that perspective "computers will be beating humans" might just mean that humans are convinced of a (false!) result, but computers can't be convinced of that same false result (in the sense that nobody can formalize it).

(Incidentally, some of the people at Kevin's talk were at Richard Stallman's talk in the same place the day before. Evidently RMS didn't allow any pictures or video, so not much will appear from that.)

I don't think anyone knows how long that's going to take. It's clear at this point that it's going to take something more than Deep Learning has to offer.

I don’t think that’s really true. There are cyclical/oscillatory behaviors within pure mathematics, for which complex numbers are useful. Just look at the other math article that’s on HN front page currently, on the Riemann Zeta function (John Baez blog post).