Competitive programmers

Stream: lean4

[Huỳnh Trần Khanh]

More competitive programmers are becoming interested in formal verification. Are there any competitive programmers in this community besides me and Reid Barton?

If 1000000007 and 998244353 look familiar to you, you are a competitive programmer.

[Sebastian Ullrich]

Surely Leo is the most competitive programmer of them all

[Siddharth Bhat]

@Huỳnh Trần Khanh I dabble from time to time, mostly to learn algorithms :) Obligatory link to algorithms collection (in C++): https://github.com/bollu/w/tree/master/algo

Does any online judge support Lean4?

[Donald Sebastian Leung]

Codewars supports Lean 3.39.1 at the moment, but it's possible to support Lean 4 given enough support from the community

[Eric Wieser]

Welcome back @Huỳnh Trần Khanh! I've taken part in google codejam pretty much every year for the last decade or so, so I guess that makes me a competitive programmer? I'm pretty sure they don't support Lean though, nor would I want to use it at the current point in time!

[Eric Wieser]

Are you aware of https://do.proof.in.tum.de/competitions/contest/25?

[Alex J. Best]

I used to do ICPC, and IPSC sort of thing once in a while. I'd definitely be curious to see how using lean (4) would be for one of these competitions. It would also be very interesting to collect verified fast Project Euler solutions for Lean 4 at some point, this would simultaneously work out the compiled speed and the mathematics libraries which would be fun.

[David Wärn]

I used to do quite a lot of competitive programming. I'm also quite interested by the idea of solving cp problems (or writing a library like KACTL) in Lean 4 -- I would hope that it would allow for better abstractions compared to C++ and that dependent types could help catch some bugs

[Reid Barton]

Huỳnh Trần Khanh said:

If 1000000007 and 998244353 look familiar to you, you are a competitive programmer.

Back in my competitive programming days, computers couldn't handle large numbers like these

[Huỳnh Trần Khanh]

Speaking of online judge support, users of uncommon languages usually compile their code to some sort of assembly and then submit the assembly wrapped in a more common language. Is it possible to compile Lean 4 to WASM?

[Huỳnh Trần Khanh]

If so, you should be able to wrap the WASM code in Node.js

[Huỳnh Trần Khanh]

I actually think we should market the Lean software to competitive programmers. Competitive programming is mostly about proofs nowadays.

but Lean 4 pretty please

[Huỳnh Trần Khanh]

I once explained to an orange coder how to use Lean. He understood it quickly and he was able to write elegant proofs. I think formal verification is very easy to understand for competitive programmers, as competitive programming uses roughly the same skill set. I might be wrong, but that's my impression

[Huỳnh Trần Khanh]

A red coder said this:

imagine sau này thi cp mà các bạn code bằng cái đó, và giờ chấm bằng các verify proof

which means

imagine in the future competitive programmers code with proof assistants and submissions are graded by the correctness of the proofs

So there's certainly some interest!

[Huỳnh Trần Khanh]

I feel like this community places too much emphasis on math research and thus we completely ignore a very big community that also does a lot of proving stuff

[Mac]

Huỳnh Trần Khanh said:

I feel like this community places too much emphasis on math research and thus we completely ignore a very big community that also does a lot of proving stuff

Don't worry, there are many in the community who have non-mathematical interests in Lean! The problem is that, for the moment, mathematics is the most published use case for Lean and thus a lot of the focus (and funding) is found there. If others can find a niche for Lean and exploit it, I am confident the devs would be happy to support it in the future. After all, that is how much of the current strong support for mathematics came about. Mathematicians found Lean when it was in a fledging stage (when it also had experimental features for other formal use cases -- e.g., HoTT -- that did not take off), used it, brought in many new users and much fame, and thus earned the focus of the devs.

[Arthur Paulino]

I'd say that the fact that the Lean community is mostly made of mathematicians as of today due to their own merit. As Mac said, they picked up Lean 3 a few years ago and built this highly professional living ecosystem with responsible maintainers that implement smart processes to allow a healthier growth of mathlib.

What I am trying to say is that it's not the other way around. If we want to see Lean 4 growing towards programming as well, we, programmers, will need to do our homework too. We need to use, find bugs, help the developers fix them, understand that they have priorities, negotiate design choices, build more libs, accompany the API evolution and understand what changes etc etc. It's a partnership!

[Arthur Paulino]

When you say "this community focus too much on math research"... of course! They are the community for the most part. They're doing their job. And they're doing it well as far as I can see.

[Kevin Buzzard]

I absolutely agree with what Arthur is saying. Lean has made inroads into the consciousness of mathematicians but this is certainly not because it was intrinsically designed with mathematicians in mind -- far from it! Even in 2019 Leo would freely admit that he did not really know what we were doing or why we were doing it, and he told me very clearly in 2019 or 2020 (I forget exactly when) that he felt it was too early in Lean's lifecycle to start making a gigantic mathematics library. I replied that we were having too much fun to stop. Because we focussed our ideas on stuff which had never been done before in formalisation, when we started having success the community noticed, and when our ideas started appearing in places like Quanta and Nature it became clear that we were doing the right thing. Right now there is a heavy focus by the devs on getting the maths library ported from Lean 3 to Lean 4 but I am absolutely sure that the moment this is done that the math community will take on the job of growing mathematics, leaving the Lean 4 devs to focus on growth in other areas. Lean is definitely not "a math project", it just happens to be a project which is playing a role in a minor revolution in the math community. This certainly doesn't stop it playing a role in doing amazing things in other areas :-)

[Henrik Böving]

To add to this I also think that it's absolutely fair Lean 4 is focusing on helping the existing user base move on from the earlier version, it's just what every other good software project should do as well. And in this case the existing user base simply happens to be mathematicians, if it were programmers and mathematicians only got interested in Lean 4 I'm sure the existing large base of programmers that are using lean 3 and want to move on would be the focus.

[Arthur Paulino]

My philosophy is "be the change you want to see in the world" :D

[Huỳnh Trần Khanh]

I think the easiest thing that we can do is create a verified KACTL equivalent in Lean 4. Hey competitive programmers, who's willing to take the initiative?

Let's do something small first, and then we can advertise our thing on Codeforces!

[Huỳnh Trần Khanh]

But first, is Lean 4 a viable imperative language or do I have to write everything in a functional way? Do I have to abuse persistent data structures like in other functional programming languages?

[Arthur Paulino]

What do you mean by "abuse persistent data structures?"

[Huỳnh Trần Khanh]

For example I can't have a real array backed by a contiguous section of memory and I need to use some sort of persistent map

[Kyle Miller]

docs4#Array is a real array backed by a contiguous section of memory

[Kyle Miller]

And if you modify it and there's only one reference to it, it'll be done in-place.

[Huỳnh Trần Khanh]

This is great. So I think we could formalize a Fenwick tree. It's somewhat nontrivial and it's an important data structure in competitive programming.

[Huỳnh Trần Khanh]

The next thing would be an iterative segment tree. Let's see how we can convince competitive programmers to switch to Lean.

[Huỳnh Trần Khanh]

https://youtu.be/kPaJfAUwViY

[Arthur Paulino]

Huỳnh Trần Khanh said:

Let's see how we can convince competitive programmers to switch to Lean

They'll need to see advantages :+1:

[Eric Wieser]

My impression of competitive programming is that rigorously proving your program is correct is totally at odds with your time constraints, so I doubt the proving capabilities of lean would be of much relevance

[Alex J. Best]

Well if proving helps you spot that you missed an edge case it can definitely be helpful to not fail a submission, especially if you have powerful automation that will only start complaining if something is actually false, but we are a long way from that yet!

[Kyle Miller]

Something I found to be nice when programming in Lean 4 is that you can prove small invariants here and there to make sure you're not making silly mistakes. Even just stating the invariants of a data structure (even if you end up proving them with sorry) is helpful, since it serves as unambiguous documentation of what needs to be true.

I think this is similar to how proponents of static typing (like Haskellers) argue that types reduce the incidence of bugs. Even though you're not proving the correctness of the entire program in Haskell, type correctness gives you pervasive small-scale proofs that the program doesn't have basic classes of defects. So, even if you don't prove your entire Lean 4 program is correct with respect to some specification, the additional power in the type system lets you prevent as many types of bugs as you might want. I'd easily believe that some of these in competitive programming would be worth the time cost.

[Andrés Goens]

To the point of formalized mathematics and the community: I personally only heard about Lean and was drawn to it because of the formalization efforts of math in Lean (and hearing @Kevin Buzzard' s talks on that). Only later I've realized that there's a lot of really interesting aspects of it as a programming language on its own. It's a gradual scale between "mathematicians" and "programmers" (I don't know as which I'd qualify) and proving things about programs vrs mathematical objects is also a shades-of-grey kind of thing, e.g. are graph algorithms math or programming? I think Lean forces mathematicians to think more like programmers, and programmers to think more like mathematicians, and ultimately we all benefit from both!

[Arthur Paulino]

I have concrete experience that sorry can be used strategically as a TODO item if the type is well specified enough. This is obviously true for theorem proving, but also applies to programming! It opens up a new level of possibilities for less ambiguous collaboration

[Kevin Buzzard]

One of the things I've really enjoyed about mathematical collaboration in lean is that you can really precisely say "this is what we need".

[Yuri de Wit]

@Kyle Miller, that is quite interesting! Do you have a few patterns for these small scale proofs that could be worth sharing?

[Yuri de Wit]

I also find it interesting that both @Arthur Paulino and @Kevin Buzzard mentioned 'collaboration' and that @Andrés Goens mentioned the gradual scale between "mathematicians" and "programmers" (btw, I am in the programmers camp, but find the math community around Lean its biggest strength at this point and a huge source of learning for me). Could Lean itself help programmers and mathematicians collaborate better? Maybe that is already part of Lean's vision (one language for proofs and programming)?

Anyway, after reading a bit about module systems the past week, I can't stop thinking that a better module system could provide additional tools to help this collaboration. One team could create packages with signatures/holes (e.g. declared theorems, just to use the example from earlier messages) and another team that could "implement" these holes in other package(s) without recompilation, etc. I am sure the devil is in the details ...

[Huỳnh Trần Khanh]

My impression of competitive programming is that rigorously proving your program is correct is totally at odds with your time constraints, so I doubt the proving capabilities of lean would be of much relevance

Maybe. But we can't say for sure. Keep in mind that practicing is also very important as well. Even if formal verification is completely infeasible during contests, which I doubt, it's very beneficial to use an interactive theorem prover when practicing. It enforces a mental model where all observations have to be rigorously checked, and you can't just come up with some random solution and hope that it passes the tests. This is literally the reason why a lot of people, including myself in the past, find competitive programming so hard to understand.

[Huỳnh Trần Khanh]

But anyway, I need a way to compile Lean 4 code to WASM. Can anyone tell me how? I imagine that the code also needs some FFI.