lean.golf

I’ve had an account on code.golf for years. I’m not very good at it, but every so often I log in and bash my head against the wall trying to improve some horribly convoluted program that, say, prints the lyrics to the 12 Days of Christmas.

In Lean, it’s also often of interest to try to “golf” proofs, cutting them down until they’re as short and direct as possible. Naturally, I thought, “why not make code.golf, but for Lean?”

So, I’ve built lean.golf. Like code.golf, lean.golf hosts a number of holes; each hole gives you a theorem, and your job is to prove it as concisely as you can. There are two modes: classic mode allows essentially any proof method; term mode bans tactic mode entirely (no by). Term mode is much harder and feels more like a type-theory puzzle.

You can play the game here! Sign in with GitHub to save your scores and appear on the leaderboards. Have fun!

(As a disclaimer, I want to differentiate between lean.golf and Lean proof golfing. Proof golfing usually means finding a short proof that is still reasonable—normal whitespace, clear information flow, etc. On lean.golf, the only goal is to write the shortest proof possible, regardless of how ugly it looks. And some of my solutions are quite hideous.)

A cropped screenshot of a ridiculously ugly, dense proof of the periodicity of the Fibonacci sequence mod m.

Oh god.

So, the game is really more for fun than practice. Still, I think it gives experienced Lean users a fun excuse to exercise their skills in a different way!

security and deployment

Because lean.golf runs submitted Lean code on my own server, security was the part I was most nervous about. I’m not a security expert in the slightest, but luckily, the engine behind the Lean web playground at live.lean-lang.org is open source! This was a huge help—I was able to reuse lean4web’s Bubblewrap sandboxing to prevent RCE attacks on the server.

This was also my first time self-hosting a web app on a VPS, which was an interesting experience. Somebody really needs to redesign the netcup control panel UI (no offense).

(Update: Thomas Zhu found a vulnerability in the sandboxing mechanism and used it to prove False, as well as run a few commands on the server!! Luckily he told me about the issue before anything was exposed. Very scary though!)

holes

There are 11 holes, which I picked with the help of AI (🙈). Here they are:

hole 1, drinker

theorem drinker (Pub : Type) [Inhabited Pub] (Drinks : Pub → Prop) : ∃ p, Drinks p → ∀ q, Drinks q := sorry

Smullyan’s Drinker Paradox: in every nonempty pub, there is someone such that, if they are drinking, everyone is drinking.

proof

By the law of the excluded middle: if everyone is drinking, choose whoever; otherwise, choose someone who is not drinking.

hole 2, spiral

theorem spiral (n : ℕ) : ∑ i ∈ Finset.range (n + 1), Nat.fib i ^ 2 = Nat.fib n * Nat.fib (n + 1) := sorry

The sum of the squared Fibonacci numbers through FnF_n is FnFn+1F_nF_{n+1}. This is the identity behind the Fibonacci spiral. Proof by induction on nn.

hole 3, no_half_succ

theorem no_half_succ : ¬ ∃ f : ℕ → ℕ, ∀ n, f (f n) = n + 1 := sorry

The successor function on N\mathbb{N} has no functional square root: there is no f:N→Nf : \mathbb{N} \to \mathbb{N} with f(f(n))=n+1f(f(n)) = n + 1.

proof

Suppose f∘f=succf \circ f = \mathrm{succ}. Then f(f(f(n)))=f(n+1)=f(n)+1f(f(f(n))) = f(n+1) = f(n) + 1, so induction gives f(n)=f(0)+nf(n) = f(0) + n. But then f(f(0))=f(0)+f(0)=1f(f(0)) = f(0) + f(0) = 1, which is impossible for f(0)∈Nf(0) \in \mathbb{N}.

hole 4, markov

theorem markov_infinite : ∀ N : ℕ, ∃ x y z : ℕ, 0 < x ∧ x ≤ y ∧ y ≤ z ∧ N < z ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 * x * y * z := sorry

Markov’s equation, x2+y2+z2=3xyzx^2 + y^2 + z^2 = 3xyz, has infinitely many solutions in N3\mathbb{N}^3. Proof by Vieta jumping: hold two coordinates and flip the third across its quadratic.

hole 5, waerden

theorem waerden9 (c : ℕ → Prop) : ∃ a d, 0 < a ∧ 0 < d ∧ a + 2 * d ≤ 9 ∧ ((c a ∧ c (a + d) ∧ c (a + 2 * d)) ∨ (¬ c a ∧ ¬ c (a + d) ∧ ¬ c (a + 2 * d))) := sorry

Van der Waerden’s W(3,2)=9W(3, 2) = 9: no matter how you 2-color the numbers 1 through 9, there is a monochromatic three-term arithmetic progression. Proof by casework.

hole 6, basel_bound

theorem basel_bound (n : ℕ) : ∑ k ∈ Finset.range n, (1 : ℚ) / (k + 1) ^ 2 < 2 := sorry

Prove that every partial sum of

∑n=1∞1n2\sum_{n=1}^\infty \frac{1}{n^2}

is less than 2.

commentary

The Basel problem is already in Mathlib, so this hole is more of a rephrasing problem than a proof from scratch. Mathlib’s hasSum_zeta_two is written as follows:

theorem hasSum_zeta_two : HasSum (fun (n : ℕ) => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)

Interestingly, the above takes advantage of Lean’s junk value 1 / 0 = 0, which lets the sum start at index 0. The sum in basel_bound, however, starts at denominator 1. So, some finagling is still necessary even after invoking the value π2/6\pi^2 / 6. (A formalization quirk that you don’t see in ordinary mathematics!)

hole 7, binary_multiple

theorem binary_multiple (n : ℕ) (hn : 0 < n) : ∃ m, 0 < m ∧ n ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d ≤ 1 := sorry

Every positive integer divides a decimal number made of only 0s and 1s.

proof

Given nn, write the numbers 1i1^i for 1≤i≤n+11 \leq i \leq n + 1 (sorry, (ab)using string power notation here). Mod nn, these numbers lie in {0,…,n−1}\{0, \dots, n - 1\}. By the pigeonhole principle, two of them must be congruent mod nn. Subtract the smaller from the larger to get a positive multiple of nn whose decimal digits are all 0s and 1s.

hole 8, pisano

theorem fib_mod_periodic (m : ℕ) (hm : 0 < m) : ∃ p, 0 < p ∧ ∀ n, (Nat.fib (n + p) : ZMod m) = Nat.fib n := sorry

The Fibonacci sequence is periodic mod mm for any mm (called the Pisano period).

proof

Let S=(Z/mZ)2S = (\mathbb{Z} / m\mathbb{Z})^2 and define f:S→Sf : S \to S by (a,b)↦(b,a+b(modm))(a, b) \mapsto (b, a + b\pmod{m}). The sequence an=fn(0,1)a_n = f^n(0, 1) is eventually periodic because SS is finite. Since ff is a bijection, periodicity extends all the way back to the start. (I got this proof from here.)

hole 9, levi

theorem levi_ben_gershon (m n : ℕ) (h : 3 ^ m = 2 ^ n + 1) : m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 3 := sorry

If 3m=2n+13^m = 2^n + 1, then (m,n)(m, n) is (1,1)(1, 1) or (2,3)(2, 3). Proof by casework and some modular arithmetic.

hole 10, jacobian

open MvPolynomial in
def JacobianConjecture : Prop :=
  ∀ (n : ℕ) (F : Fin n → MvPolynomial (Fin n) ℚ),
    IsUnit (Matrix.of fun i j => pderiv j (F i)).det →
    ∃ G : Fin n → MvPolynomial (Fin n) ℚ,
      (∀ i, aeval G (F i) = X i) ∧ (∀ i, aeval F (G i) = X i)

theorem jacobian_disproved : ¬ JacobianConjecture := sorry

The Jacobian Conjecture is (famously) false. Proof by counterexample.

hole 11, falso

theorem falso : False := sorry

Teehee. Proof by soundness bug.

conclusion

That’s all! I had a lot of fun building lean.golf, and I hope you have just as much fun playing it!