leetcode for lean

Stream: new members

[Rado Kirov]

I like doing small programming / algorithmic exercises and leetcode.com has been a great site to log in every few days and try to solve the daily challenge. Almost all problems are at most 50 lines of code, but turns out there is tremendous variety of problems, while staying with in the constraints - only stdlibs for any programming language needed, no advanced CS needed. For easy and medium problems, fairly competent programmer can jump in and solve a problem in <30min, get a small dopamine boost and move on with their day.

I think math has similarly large reservoir of interesting fun problems that can be both challenging and still generally solvable quickly without getting into advanced topics. IMO problems are a great example.

With Lean one can even start to envision a site where a daily problem is shown and one has to write their Lean proof and it is checked and accepted or denied. After all programming = proving (Curry-howard), but when I start to think about the details I am not so sure how would this work in practice:

• how much of mathlib can or should be used. Should some of mathlib be hidden intentionally? Should the right theorem be highlighted somehow. Generally it feels mathlib is much larger than a standard language lib - where one has to memorize array and hashmap APIs, but after that they can basically solve any leetcode problem with maybe tops ~ 100 APIs. In Lean proving it feels like the order of magnitude is larger.
• Would it be fun to allow high-power tactics like grind or intentionally ban them.
• while there are a lot of theorems to pick from - large number of them are trivial, how to find the ones that have some sort of mathematical challenge to them (beyond just telling lean what to do) - like showing lim a + b = lim a + lib b, by picking the right epsilons.
• are there branches of undergraduate math that have more of such proofs - I was thinking elementary number theory maybe?

Has anyone thought about this? Would anyone be interested in doing daily lean challenges if this existed?

[Rado Kirov]

Note the goal is slightly different from NNG and similar games, it is not so much to learn Lean or math, but the do daily practice of the skills one presumably has, but might have gotten rusty on. Some call these in programming coding katas in analogy with martial arts.

[Andrew Yang]

How about yes all mathlib and yes all tactic and the best get merged into mathlib :)

[Rado Kirov]

Do you think there are enough theorems that are both easy enough to prove in 30min, not in mathlib and desirable to contribute to mathlib?

[Andrew Yang]

Yes.
Or I guess it depends on whose 30 min it is and whether that includes the time to come up with the mathematical proofs.

For example here's a fun (and useful) one :)
I haven't tried but the proof is hopefully < 50 lines.

import Mathlib

example {R K : Type*} [CommRing R] [Field K] [IsNoetherianRing R]
    [Algebra R K] [IsFractionRing R K] {x : K} :
    IsIntegral R x ↔ ∃ r : R, r ≠ 0 ∧ ∀ n, r ^ n • x ∈ (⊥ : Subalgebra R K) := by
  sorry

[Rado Kirov]

That's a bit more advanced that what I was envisioning, because of the prerequisite algebra needed, but could be seen as a "hard" problem, I guess.

[Markus Himmel]

We had this in the Lean 3 days: https://www.codewars.com/kata/search/lean?q=&order_by=sort_date%20desc Many of these should be straightforward to port to Lean 4

[Snir Broshi]

As for "hard" problems, I've had a few instances when I thought "I need this lemma, it isn't in Mathlib, but I don't feel like proving it right now", and I wanted to have some database of problems where I can write the statement and then toss it up for grabs.
Such lemmas might be easy, but they also might be impossible because of some missing hypothesis.
This might be a different idea, but maybe it could be integrated to such a leetcode platform?

[Eric Wieser]

Markus Himmel said:

We had this in the Lean 3 days: https://www.codewars.com/kata/search/lean?q=&order_by=sort_date%20desc Many of these should be straightforward to port to Lean 4

Is the Lean runtime that code wars used community-contributed, or did we have to persuade one of the people that owns it to write the glue?

[Rado Kirov]

We had this in the Lean 3 days: https://www.codewars.com/kata/search/lean?q=&order_by=sort_date%20desc Many of these should be straightforward to port to Lean 4

That's exactly what I am envisioning, wasn't aware it existed, thanks for sharing. I see a lot of the usual suspects contributed to it, I am wondering if there any lessons learned to share here.

[Kevin Buzzard]

The questions I proposed were mathematically tricky (indeed Mario complained that they weren't testing lean ability because they were too difficult to solve). Probably an LLM could find a solution now though

[Rado Kirov]

Yeah, I tried a few on the codewars site, but 1) it's extremely hard to write Lean without InfoView (basically a non-starter IMHO) 2) a bunch of the questions were about code verification not math 3) some were just hard.

I have no doubts, LLMs can currently solve every leetcode.com problem, but I would like to say it doesn't take away from the fun of solving them by hand (but with the right UI). I think of it similar to chess, having better than human AIs did not make chess less popular (if anything it had a mini resurgence)

[Rado Kirov]

I think my takeaway is that curation of the right proofs is the key to any success here - too many theorems that are either too trivial or too hard. I think best bet is to start with easier IMO problems.

Btw, https://adventofcode.com/ is coming up in Dec, it could be fun to create a Lean version (like https://adventofsql.com/, etc), but I don't think I can curate 25 good problems in time for Dec. Also, unlike advent of code where one can just submit the result of a computation without the code itself, for a proof the best one can do is submit the whole proof for checking that it has no 'sorries', axiom or other shortcuts.

[Alfredo Moreira-Rosa]

You could just create an advent of code thread and share the code for a solution each day. And with a twist compared to advent of code, to prove that your code is correct.
I have finished all advent of code problems 5 years in a raw in different programming langages.
I may help this year in doing it with lean.

[Rado Kirov]

Oh yeah, that’s a separate topic and I plan to test the waters with verified FP with lean this year on AoC since there will be two days between problems. But my original thread is more about developing advent of math proofs (AFAIKT proving math is easier than writing code and proving its correctness, as you need to know more APIs to do both)

[Rado Kirov]

Just learned that https://typesig.pl/2024/12/12/advent-of-proof-2024.html exists (no word if it is coming back in 2025). Did anyone here participate in 2025? I am definitely going to try it this year, though with regular AoC not sure how much time left I will have.

[heitopai]

Problems on leetcode can be regarded as math problems, and then we can prove that the algorithm for solving the problem is correct or prove the time complexity of the algorithm. I wonder if this idea is feasible?