## Stream: new members

### Topic: Graphs, trees, binary search trees, array, algorithms

#### Huỳnh Trần Khanh (Feb 06 2021 at 10:54):

I want to formalize competitive programming problems in Lean. Think of it as a competitive programming analog of the IMO Grand Challenge, LOL. But I don't really know how to formalize commonly used algorithms and data structures such as BFS, Dijkstra, Floyd–Warshall, sparse tables, segment trees and stuff. Can anyone point me in the right direction?

#### Huỳnh Trần Khanh (Feb 06 2021 at 11:05):

For example, could you point me to a GitHub repository of formalized algorithms in Lean?

#### Alena Gusakov (Feb 06 2021 at 11:46):

Personally idk about any repositiories with all of that, but I do know that mathlib currently contains a little bit of material on binary trees

#### Alena Gusakov (Feb 06 2021 at 11:46):

Don't remember how much material there is though

#### Kevin Buzzard (Feb 06 2021 at 11:58):

Can you not just follow the kind of thing done in Haskell?

#### Huỳnh Trần Khanh (Feb 06 2021 at 12:49):

Of course I can't, that's why I'm asking! Sure I can crib techniques from Haskell when I formalize the implementation but I think proving is more complicated, and I'm pretty sure Haskell is not a verification language by any stretch of the imagination.

#### Huỳnh Trần Khanh (Feb 06 2021 at 12:55):

By now I've skimmed through every thread in the Program verification stream and I couldn't find anything I'm looking for.

#### Kevin Buzzard (Feb 06 2021 at 13:38):

I had misunderstood, I thought you were just asking about implementing the algorithms and data structures you listed

#### Kevin Buzzard (Feb 06 2021 at 13:40):

Maybe you should ask a more precise question

#### Mario Carneiro (Feb 06 2021 at 19:47):

Generally speaking, you can just write a program like you would in haskell and as long as it's non-meta you can prove properties about it after the fact in lean

#### Mario Carneiro (Feb 06 2021 at 19:49):

the only thing you have to be careful about while writing the definition is that it is structured such that it "manifestly" terminates

#### Andrew Ashworth (Feb 07 2021 at 00:47):

as always, software foundations has you covered:

#### Andrew Ashworth (Feb 07 2021 at 00:47):

https://softwarefoundations.cis.upenn.edu/vfa-current/index.html

#### Huỳnh Trần Khanh (Feb 07 2021 at 02:34):

@Andrew Ashworth Oh neat! From what I've gathered, it looks like no one has attempted to formalize and prove properties about the algorithms and data structures I mentioned in Lean right? So I could consider myself a pioneer, haha. And I don't expect segment trees, sparse tables or even tries to be covered by software foundations as these data structures are specific to competitive programming, which is a pretty niche field.

Last updated: Dec 20 2023 at 11:08 UTC