Git issues in formal-conjectures

Stream: Formal conjectures

[Timothy Chow]

I am a novice user of both VS Code and Git. I have been trying to submit a conjecture to the Formal Conjectures project, but have been running into problems, doubtless because of my own ineptitude.

You can take a look for yourself here: The Latin Tableau Conjecture. Paul-Lez and Yael Dillies have been very helpful and have suggested a number of improvements to my original submission. Initially, the changes were minor enough that I wasn't using VS Code to make them; I was using a text editor and pushing them to the Git repo. At some point, however, things got complicated enough that I needed to fire up VS Code to resolve the conflicts, and that's when I started to get errors that I did not understand. I won't reproduce the whole conversation here, but Paul-Lez and Yael Dillies suggested that I create a conversation here on Zulip for the benefit of others who might encounter similar problems in the future.

[Yaël Dillies]

For future reference, the issues was that Timothy had only their own fork set as a git remote, and therefore couldn't fetch the changes from the upstream repository.

[Yaël Dillies]

Looks like you got to the point of being able to merge. Now, you need to solve the merge conflicts

[Timothy Chow]

With a great deal of help from Yaël Dillies, I have finally completed the submission. As this is one of my favorite conjectures, I hope it will attract some attention. It is entirely elementary, and I think anyone can understand it by spending half an hour reading the first few pages of the paper (or even less time, if you have some prior familiarity with colorings of graphs).

I'm pretty confident the conjecture is not easy, because about a dozen people have seriously attempted to prove it, so far without success (although there are partial results). At the same time, a dozen people is not that many people, so it's still conceivable that there is a relatively short proof (or counterexample, although I did run a moderately large computational search for counterexamples).