Lean Golf – Code golf but you're proving theorems in Lean
2 days ago
- 洞1（简单）：酒吧里有一个人，如果他喝酒，那么所有人都喝酒。（饮酒者悖论）
- 洞2（中等）：螺旋问题（描述缺失）。
- 洞3（中等）：没有函数在应用两次后恰好加一。
- 洞4（中等）：马尔可夫问题有无穷多个解。
- 洞5（中等）：整数的任何2染色都包含一个单色的三项等差数列（范德瓦尔登定理）。
- 洞6（困难）：巴塞尔界问题（描述缺失）。
- 洞7（困难）：每个正整数都能整除一个仅由0和1组成的数。
- 洞8（困难）：斐波那契数列模任意整数都是周期的（皮萨诺周期）。
- 洞9（困难）：莱维问题仅在……（不完整）。
- 洞10（困难）：雅可比猜想是错误的。
- 洞11（不可能）：打破一致性（可能是一个悖论）。