bsubs

5 ms·

1.
by bsubs 2mo ago
> I wish you spent at least a couple words in the paper about that. That makes sense; it just happened that we tried the other identities after having written and submitted the paper. More importantly, the variants of Wilkie's ident
2.
by bsubs 2mo ago
Indeed, having a different "exotic identity" that has smaller countermodels would be awesome. Unfortunately, we tried a few alternatives to Wilkies and didn't find smaller countermodels. Note that it's not obvious at all
3.
by bsubs 2mo ago
Hi! One of the authors here. Whether checking the LLM-generated Lean statements/definitions is easy or not depends heavily on the area of mathematics and the concrete definitions at play. In this case it was remarkably easy. As you can
4.
by bsubs 2mo ago
I'm one of the authors of the arXiv paper. Thanks for bringing this to our attention! We were fully unaware of this repository, and it unfortunately did not come up during our literature search. Our approaches to the lower bound are p
5.
by bsubs 2y ago
If you’d be interested in being mentored in a research project send me an email; bersub@cmu.edu
6.
by bsubs 4y ago
I see what you’re saying, but note that as mentioned above I did edit the post based on your feedback to be precise, stating that the conjecture we disproved was that regardless of the center color the chessboard of 1s could be assumed wlog
7.
by bsubs 4y ago
Assume you know that 13 colors aren't enough and you want to prove that 14 aren't enough either. Any 14 packing-coloring of the grid must use color 6 somewhere, as otherwise it would be only using 13 colors that are no better than
8.
by bsubs 4y ago
I agree, and it would be amazing for someone to find a deeper intuitive reason for why 15 is the answer to this problem, or 8 is the answer to that other problem, or many such cases. This is however extremely hard in my opinion (note that I
9.
by bsubs 4y ago
I think I see what you mean, but it seems to me that you're mixing ideas about the chessboard conjecture in this particular context, with more general versions of the conjecture (a bunch of which we don't know the answer for, and
10.
by bsubs 4y ago
Let me be a bit more precise here (at risk of being pedantic) to make sure we're on the same page. (Also, if you have a concrete idea of how to reformulate the text so this is clearer, I'm definitely interested!) Here are two well
11.
by bsubs 4y ago
Thanks jxf! I just fixed some, although it's likely that some typos remain. I agree with you about Coq, although there are some very smart folks working on it. My concern is that most of the improvements I've heard of are not abou
12.
by bsubs 4y ago
Thanks to you for the feedback!! :) reading some positive comments here has definitely paid off the investment of time in writing the post and taking care of the figures (by far the most time-consuming part haha).
13.
by bsubs 4y ago
This is a question I've spent significant time on! (under a more technical formalization, of course) I've proved that this is not possible in infinite 1-dimensional graphs (like the infinite path, or an infinite grid of size C x I
14.
by bsubs 4y ago
Even though you're right in general, this is not the case here! We have proved that no smaller counter-example exists (again by using a computer search through optimized SAT-solving). As for the question of why no smaller counter-examp
15.
by bsubs 4y ago
Thanks! this is a correct answer. Indeed I stated the conjecture a bit imprecisely in the blog post (the paper is more detailed in this respect). Just to make it fully precise, the conjecture was that if you take any $D_r$ graph, and force
16.
by bsubs 4y ago
Thanks! silly omission on my side, will fix it now! Hopefully that didn't harm understanding!
17.
The Packing Chromatic Number of the Infinite Grid is 15: the story behind it(bsubercaseaux.github.io)
94 points by bsubs 4y ago|34 comments
18.
by bsubs 4y ago
In this blog post I tell my story working on a Math problem that I discovered in a Facebook Math group, and worked on for almost 3 years, until solving the problem and getting congratulated by my personal hero Don Knuth.
19.
by bsubs 5y ago
Author of the paper here, in case someone wants to ask a question :) I originally didn't think it would get much attention, provided it's a bit technical...