Getting Started: Contributing Algorithm Proofs to CSLib

Stream: CSLib

[Iaroslav P]

Hello everyone!

I would like to start working on providing proofs for algorithms, and I checked the conversation that happened in the thread "Proposal on Time Complexity".

I also checked the current open PR (which is in draft state for now).

That's why I have a few questions:

1. What is the best starting point for me to bring at least some value to CSlib?
2. Would proofs for algorithms and data structures (for example, from the Introduction to Algorithms book) be a good starting point?
3. Am I right that the plan is to have not only implemented but also proven algorithms under "CSlib/Algorithms", and that this is one of the reasons why the PR is still in draft state?

Thank you!

[Sorrachai Yingchareonthawornchai]

For analysis of algorithms in Lean, you can wait a bit until the Time Monad request goes through, so you can use it on your favourite algorithms. I plan to push a request for other stuff right after this request, such as binary search and bitonic search, with correctness and time complexity.

In the meantime, you can check out my lecture on formalizing the analysis of algorithms in Lean in case you want more examples. Students in my class are already formalizing many algorithms as class projects.

[Shreyas Srinivas]

I would argue that you should wait for the free monad approach to go through

[Shreyas Srinivas]

I still maintain that while lightweight approaches are they must be systematic and that the manual tick based approach is too risky and naive. There is a whole long thread discussing this.

[Iaroslav P]

Thanks for the guidance!

I'll go through the lectures while waiting for the Time Monad approach to be merged.

Quick question: Should I avoid algorithms already covered in the lecture materials/student projects, or would it be okay to work on those as well?

[Shreyas Srinivas]

I also recommend working with mathlib’s graph definitions in general since they have relatively battle tested APIs

[Sorrachai Yingchareonthawornchai]

Iaroslav P said:

Thanks for the guidance!

I'll go through the lectures while waiting for the Time Monad approach to be merged.

Quick question: Should I avoid algorithms already covered in the lecture materials/student projects, or would it be okay to work on those as well?

These are supposed to be simple exercises. It is also good for you to learn to do it even if it is already formalized. In my view, the point of these is about learning how to analyze algorithms in Lean. Once you are comfortable with this mindset, you can formalize anything.

[Nadim Farhat]

This should be made into a sticky or something.