The rules

In golf, the goal is to complete each hole in as few strokes as possible. In code golf, it is to solve a problem with the shortest program. Inspired by this sport, and particularly by the code.golf site, lean.golf is code golf for theorem proving.

Each hole is a Lean 4 theorem with a locked statement. You write the part after the :=. A proof scores if it compiles, contains no sorry, and uses no forbidden axioms. Shortest proof wins.

Playing a hole

The theorem statement sits at the top of the editor and cannot be changed. Your proof starts on the next line. The right-hand pane contains three tabs: the goal at your cursor, Lean's Infoview messages, and the leaderboard for the hole. If you have used Lean in VS Code or Lean's web playground, the first two will work as you expect.

lean.golf currently runs Lean v4.32.0 and imports all of mathlib4. You can use proof-search tactics such as exact?, simp?, hint, and aesop? while you work, but you need to apply their suggestion before submitting. (Metaprogramming is also not allowed.) Regular tactics such as simp, omega, decide, and aesop are fair game.

Scoring

In each mode, the shortest proof on a hole gets 1,000 points. Everyone else gets round(1000 × shortest ÷ yours). The clubhouse adds up your points across the course and ranks players by that total.

Each hole has two modes. Classic allows tactics. Term is for proofs that never enter tactic mode (i.e., no by). The modes have separate rankings. Since a term proof is also a classic proof, a new term best can improve your score in both.

golfbot is the house account. Its reference solutions are scored normally and show up on the same leaderboards. It has a term proof for every hole it has solved except the Jacobian one. That one was too hard. See if you can beat it!

Verifying

Submitting checks your proof straight away, sending it to comparator to check it again before the score is recorded (to make sure you didn't cheat). While that runs, the board shows your byte count dulled in the position it is about to take. It settles in a few seconds to a couple of minutes, depending on the hole. Don't worry if it takes a while - if you didn't do anything weird and it compiled when you submitted, the proof will go through.

Keeping score

Sign in with GitHub and the site will save your drafts and best solutions automatically. Your public scorecard lives at /u/@your-username.

Ready? The course is this way.