17

In enumerative combinatorics, a bijective proof that $|A_n| = |B_n|$ (where $A_n$ and $B_n$ are finite sets of combinatorial objects of size $n$) is a proof that constructs an explicit bijection between $A_n$ and $B_n$. Bijective proofs are often prized because of their beauty and because of the insight that they often provide. Even if a combinatorial identity has already been proved (e.g., using generating functions), there is often interest in finding a bijective proof.

In spite of the importance of bijective proofs, the process of discovering or constructing a bijective proof seems to be an area that has been relatively untouched by computers. Of course, computers are often enlisted to generate all small examples of $A_n$ and $B_n$, but then the process of searching for a bijection between $A_n$ and $B_n$ is usually done the "old-fashioned" way, by playing around with pencil and paper and using human insight.

It seems to me that the time may be ripe for computers to search directly for bijections. To clarify, I do not (yet) envisage computers autonomously producing full-fledged bijective proofs. What I want computers to do is to search empirically for a combinatorial rule—that says something like, take an element of $A_n$ and do $X$, $Y$, and $Z$ to produce an element of $B_n$—that appears to yield a bijection for small values of $n$.

One reason that such a project has not already been carried out may be that the sheer diversity of combinatorial objects and combinatorial rules may seem daunting. How do we even describe the search space to the computer?

It occurs to me that, now that proof assistants have "come of age," people may have already had to face, and solve (at least partially), the problem of systematically encoding combinatorial objects and rules. This brings me to my question:

Does there exist a robust framework for encoding combinatorial objects and combinatorial rules in a way that would allow a computer to empirically search for bijections? If not, is there something at least close, that could be adapted to this end with a modest amount of effort?

In my opinion, Catalan numbers furnish a good test case. There are many different types of combinatorial objects that are enumerated by the Catalan numbers. As a first "challenge problem," a computer program should be able to discover bijections between different kinds of "Catalan objects" on its own. If this can be done, then there is no shortage of more difficult problems to sink one's teeth into.

Timothy Chow
  • 78,129
  • 2
    FindStat is probably the closest thing, but this is just Python-based brute-force checking of small cases, not Coq-based generation of proofs or definitions. I'm afraid you're asking for mid-21st Century computer science; bijective proofs can contain pretty much every kind of mathematical reasoning, and I haven't even seen a program generating synthetic proofs of results in triangle geometry so far (an obvious first step). – darij grinberg Dec 08 '17 at 22:41
  • 1
    And as someone who spent months trying to learn proof assistants and failed to get to a point where I could actually use them in my research, I would not claim they have come of age, unfortunately. – darij grinberg Dec 08 '17 at 22:43
  • 1
    That said, you might want to talk to Florent Hivert, who has written a proof of the Littlewood-Richardson rule and various other things in ssreflect. – darij grinberg Dec 08 '17 at 22:44
  • 1
    @darijgrinberg : Thanks for the suggestions. I would like to emphasize that at the moment, I'm not hoping for the computer to search for the proof of correctness, but merely the combinatorial rule that sends $A_n$ to $B_n$. It seems to me that the space of possible rules is fairly limited. Even something rather complicated like jeu de taquin is built out of simple local transformations. If algebra is needed to describe how to transform one combinatorial object to another then we typically don't call it a "bijective proof." Algebra is only allowed in the proof of correctness. – Timothy Chow Dec 09 '17 at 00:37
  • 2
    Okay, this sounds a tad closer to the current frontier, although probably still beyond it. Talk to the FindStat people (Viviane Pons and others). Also, Stephen Wolfram might have some thoughts about it -- after all, his atlas of elementary cellular automata was an attempt at brute-forcing combinatorial transformations (and one of them is related to RSK, as far as I recall). Still, if one isn't careful, I feel that fishing out the relevant stuff from the space of possibilities will be just as hard as finding the bijections by hand. – darij grinberg Dec 09 '17 at 01:38
  • 2
    I know Tom Denton used machine learning techniques to devise candidate bijections, but this was all specific to the problem he was working on. While not automated, this type of step seems valuable and is possible with current tools. You might want to talk to him about his thoughts on the matter. – Zach H Dec 09 '17 at 01:39
  • 1
    If you want to get serious about it, the main advantage we have over the machines yet is that we can think by associations and they are confined to formal logic. Playing mathematics for me is like answering the question "How is raven like a writing desk?" There is a famous book by Polya "How to solve a problem". Once the computer can understand it and apply those very basic level techniques with the minimal degree of success, we are talking business. Before that time they can drive cars, fight wars, etc., but are of no real use in math beyond sheer brute-forcing, IMHO. – fedja Dec 09 '17 at 01:48
  • 1
    A first step in this direction may be the automatic generation of a bijective proof based on a known generating functions proof. Say, bijectivizing application of the kernel method. – Alexander Burstein Dec 09 '17 at 01:52
  • 1
    @fedja : I agree with your assessment. You can rephrase my question this way: Perhaps finding bijections doesn't require any ingenuity but can be done by brute force? – Timothy Chow Dec 09 '17 at 04:22
  • 1
    One probably would need to first set up a framework general enough to contain all interesting cases of combinatorics, as well as all interesting bijections. For example, pattern-avoiding permutations is a good candidate - encoding your objects as classes of pattern-avoiding permutations would be a first step. Then perhaps one can find generating functions for these. – Per Alexandersson Dec 09 '17 at 04:31
  • 1
    Sometimes yes. But more often than that no. Take Wolfram alpha, for instance. It is smart enough to tell that $\prod_{k=1}^n(n-k)=0$ but not that $\prod_{k=1}^{n^2}(n-k)=0$. What you are asking for is more or less equivalent to educating it to the extent that it could find products like $\prod_{x,y,z,t=0}^n(n-x^2-y^2-z^2-t^2)$. – fedja Dec 09 '17 at 04:33
  • 1
    Here is a Pythagorean test case: Can any assistants provide a proof, or even a rule, of the bijection between these two subsets of $Z\times Z$? $$SquaresOnSides={(x,y):(-a \le x < 0\ &\ -a \le y < 0)\vee (-b \le x+a < 0 \ &\ 0 < y \le b)},$$ $$SquareOnHypotenuse={(x,y):(0 \le bx+ay <a^2+b^2)\ &\ (0 \le −ax+by < a^2+b^2)}$$ –  Dec 09 '17 at 04:42
  • 1
    @darijgrinberg I can sympathise with your first comment. – James Smith Dec 09 '17 at 11:06
  • 1
    @TimothyChow Perhaps at some point you can expand on why you think that proof assistants have come of age. Maybe there's something I've missed... – James Smith Dec 09 '17 at 11:07
  • 1
    @TimothyChow Feel free to ignore the above question, on reflection it seems a bit flippant, apologies. – James Smith Dec 09 '17 at 13:56

3 Answers3

10

As mentioned in the comments, the FindStat project is aiming at what you want. Concerning the size: it contains currently about 1000 'combinatorial statistics', that is maps $s:\mathcal C_n\to \mathbb Z$ on some (graded) set of 'combinatorial' objects $\mathcal C_n$ and about 150 'combinatorial maps' between two collections. What makes FindStat powerful is the (trivial) ability to compose maps. For example, for Catalan objects we obtain about 1.500.000 a priori different statistics.

Let me point out some possible ways of using it, in the spirit of the question.

  1. 'automatically producing a bijection mapping one statistic to another' is demonstrated in Two statistics on the permutation group and Combinatorics problem related to Motzkin numbers with prize money I.

  2. 'automatically producing conjectures' is achieved by clicking on 'search for distribution' on any of the statistics in the statistics database. The result is a list of statistics that are conjecturally equidistributed with the given statistic, but where a map transforming the first into the second might not be known. A classic is http://findstat.org/St000012.

  3. it is easy to write a script that iterates 2. to find a 'partner' for a given pair of equidistributed statistics. An example is given in the comments to https://math.stackexchange.com/questions/2511943/leaf-labelled-unordered-rooted-binary-trees-and-perfect-matchings. Note that this meanwhile has a proof, also (essentially) discovered by FindStat.

  4. a different kind of conjectures is provided by the list of 'experimental identities' found when selecting any of the maps at http://findstat.org/MapsDatabase. I am guessing that not all identities at http://findstat.org/Mp00101 are immediately obvious.

  5. I am also working on a new package that checks whether a statistic satisfying given constraints can possibly exist. But that's for later...

FindStat
  • 839
2

It is perhaps hard still to automate bijection finding, but if you have a database of statistics on A and B, you can automatically check if there is (empirically) a bijection which sends some statistic on A, to some other statistic on B. That is, you refine the bijection.

I have used this approach successfully in a number of projects, in one case it even required the bijection to be canonical (i.e. there was a unique one that preserved the statistics).

Per Alexandersson
  • 15,598
0

Does the OEIS count? Three of your papers are listed in https://oeis.org/wiki/Works_Citing_OEIS as having used the help of either OEIS or Superseeker , I presume to help find a (potential?) bijection.

JimN
  • 255
  • 1
    No. OEIS can help you discover that your combinatorial objects seem to be equinumerous with some other combinatorial objects, but it does not help you find the combinatorial rule that transforms one type of object into the other. – Timothy Chow Dec 10 '17 at 19:53