Lean Golf – Code golf but you're proving theorems in Lean
2 days ago
- Hole 1 (easy): There is someone in the pub who, if they drink, everyone drinks. (Drinker's paradox)
- Hole 2 (medium): Spiral problem (description missing).
- Hole 3 (medium): No function on applied twice adds exactly one.
- Hole 4 (medium): Markov problem has infinitely many solutions.
- Hole 5 (medium): Any 2-coloring of integers contains a monochromatic 3-term arithmetic progression (Van der Waerden's theorem).
- Hole 6 (hard): Basel bound problem (description missing).
- Hole 7 (hard): Every positive integer divides a number written with only 0s and 1s.
- Hole 8 (hard): The Fibonacci sequence is periodic modulo every integer (Pisano period).
- Hole 9 (hard): Levi problem only at ... (incomplete).
- Hole 10 (hard): The Jacobian conjecture is false.
- Hole 11 (impossible): Break consistency (likely a logical paradox).