Hacker News Reader

Comment by ocfnash | Hacker News Reader

I've been following Buzzard's evangelism of proof assistants for some time.

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.

View on HN

I like to think that I'm good at these combinatorics-kind of questions, but I can't wrap my head around this one. I can follow the construction of the matrix, but I don't understand how you came up with the formula.

I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse.

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))

These are equivalent to:

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

And so it is sufficient to have:

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

We can then rearrange this to the headline formula by noting:

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

And then simplifying by repeatedly using the fact that for any x, y, z:

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

All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...

Cool!

Thanks. I just don't understand how you arrived at

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

The rest is clear.

Oh I see. Here's how I got there (still using the terminology / notation of my original post).

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)

Since I want to be able to conclude that there is a cell that is neither column-bad nor row-bad, and since there are rc cells in total, I then further require that k is such that:

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

(The point is that this is a strict inequality and so there must be a cell that is neither column-bad nor row-bad.)

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.

Ah, it makes total sense now! Thanks for taking the time to explain your thought process to a random stranger on the internet ;)

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.

You're welcome.

Reply on news.ycombinator.com