Timeline for Automated search for bijective proofs
Current License: CC BY-SA 3.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 15, 2023 at 9:07 | answer | added | Per Alexandersson | timeline score: 3 | |
| Dec 10, 2017 at 19:54 | vote | accept | Timothy Chow | ||
| Dec 9, 2017 at 13:56 | comment | added | James Smith | @TimothyChow Feel free to ignore the above question, on reflection it seems a bit flippant, apologies. | |
| Dec 9, 2017 at 11:07 | comment | added | James Smith | @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... | |
| Dec 9, 2017 at 11:06 | comment | added | James Smith | @darijgrinberg I can sympathise with your first comment. | |
| Dec 9, 2017 at 9:25 | answer | added | FindStat | timeline score: 11 | |
| Dec 9, 2017 at 7:07 | answer | added | JimN | timeline score: 1 | |
| Dec 9, 2017 at 4:42 | comment | added | user44143 | 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 9, 2017 at 4:33 | comment | added | fedja | 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)$. | |
| Dec 9, 2017 at 4:31 | comment | added | Per Alexandersson | 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. | |
| Dec 9, 2017 at 4:22 | comment | added | Timothy Chow | @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? | |
| Dec 9, 2017 at 1:52 | comment | added | Alexander Burstein | 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. | |
| Dec 9, 2017 at 1:48 | comment | added | fedja | 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. | |
| Dec 9, 2017 at 1:39 | comment | added | Zach H | 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. | |
| Dec 9, 2017 at 1:38 | comment | added | darij grinberg | 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. | |
| Dec 9, 2017 at 0:37 | comment | added | Timothy Chow | @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. | |
| Dec 8, 2017 at 22:44 | comment | added | darij grinberg | 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. | |
| Dec 8, 2017 at 22:43 | comment | added | darij grinberg | 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. | |
| Dec 8, 2017 at 22:41 | comment | added | darij grinberg | 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). | |
| Dec 8, 2017 at 22:32 | history | asked | Timothy Chow | CC BY-SA 3.0 |