这个是原帖，转侵删什么的我就不想说了，总归是我回答了问题也不至于连我转载一下都不让吧。。
染色问题http://tieba.baidu.com/p/5137020533

为了防止链接失效还是复制一下原帖主的问题：将平面上的所有点染成红蓝两色，是否存在一种染法使得任意四个同色点无法构成正方形？

证明的大致过程：
一个自然的想法就是先考察格点，虽然这会损失一些东西，但毕竟格点中的正方形是很好找的（而且在旋转下有一部分子图可以构成一组新的格点）
然后画了几次直觉得出总归是有同色正方形的
于是反设无同色正方形
我接下来的一个想法就是考察哪些构型，或者说子图，是会导致产生同色正方形的
于是就考察了u形，因为u形大小适中，既不会信息量太少难以推演，也不会太苛刻难以应用
得出u形不存在之后，就很高兴，想进一步考察一个更小的子图：三度点，是否存在
结果分类知，同样不存在
这就很省事了
而折角的二度点总归是存在的，于是从二度点为基础，应用刚才两个不能存在的子图，进行推演
推出存在正方形，这就推翻了假设
另外，还可以进一步地估计，多大的格点图，一定会有同色正方形
但是我懒得这么做，md作业写不完了

昨天吃饭前后随手做了下
得到了一个只要四张图的解法
稍微快上一些，也不需要过多Lemma
用到的唯一Lemma是拐字形的存在性，这个用一张图即可证
剩下三张图是由两次分类讨论得到的
有时间整理一下发出来

用了23张图（实际草稿还要多）暴力讨论出了一个结果：
一个9*9的网格中，必存在同色正方形

期间浪了几天，刚才又重新开始做了下
确信了9*9的确必有同色正方形
这次用了一个全新的炒鸡好用的Lemma

图证总共12张~
为了防止吞贴，依旧以网盘的形式给出
https://pan.baidu.com/s/1qyIuAkTdJA_Y-MrkViMdfw

自7.18以来，一直咕咕咕
今天来继续填一下坑吧
先来一局元气骑士再说（

为了提高效率做了个自动推理姬
可以自动搜索正方形中的同色三点，给出下一步染色的指示
嘛……明明这种东西半个下午就做出来了（还是在我仅有学校里的编程知识的情况下……
之前做的话可以节约很多人参
这玩意再进一步做一下的话就可以直接针对一个矩形网格，以一种比穷举高效的多的方式（大概），判定是否必有同色正方形
不过思考了一下，如何教给程序在不能判定下一步的时候，选取合适的点分类讨论，似乎不会弄
还是人工+程序吧

好了，基本成形了
程序主要讨论了29个分支，用了776步，完成了7*7的判定
7*7必有同色正方形被机器打败了真不甘心，虽然是自己写的……
程序的唯一问题是不能无中生有，即如果连同色正方形的两个顶点都没有的话，它就不能运行……
然鹅这个直接初始输入一下就好
这次输入的是R0R1，1在0的正上方

略微改了一下代码，来看看完全展开的步骤数……
然后发现两种初始状态都是4000步上下……并无优劣之分
分支数懒得写代码算了……
4000<<2^49

1366步推导出7*6必有同色正方形
这个应该是极小的，因为6*6不可
1 0 1 0 1 0
0 0 0 0 1 1
1 1 0 1 1 0
0 1 1 0 1 0
1 1 0 0 0 0
0 1 1 1 0 1
7*5不可
1 0 1 1 0 0 0
0 0 0 1 1 0 1
0 1 1 1 0 1 1
1 1 0 0 0 0 1
0 1 1 0 1 1 1

这是一个5*15的循环节，为了证明它的确没毛病，周期延拓后任取一5*19的片段验证即可
0 0 0 0 1
0 1 0 1 1
0 1 1 0 1
1 1 0 0 0
0 1 0 1 0
0 0 0 1 1
1 0 1 1 0
1 1 0 1 0
1 0 0 0 0
1 1 1 0 1
0 0 1 1 0
0 1 1 0 0
0 0 1 1 0
0 1 1 0 0
1 0 1 1 1