lean/mathlib teaching

Stream: new members

[Alfredo Garcia]

Hello, i am looking for someone with experience that can help me with lean/mathlib. I had been working in some personal projects with lean for a while but there is a lot of things that i will love to know to make faster and better progress. Documentation and resources are pretty good but i have a bunch of specific questions. My goals are mostly in formalizing cryptography stuff but i am also very interested in contributing to mathlib in any area. I am not a mathematician but a software engineer. I can get funding for classes.
Another option will be to form a small team of starters to work in a common project and learn from each other. Anyone interested please let me know. Thanks (I am not sure if this message is in the right stream, let me know).

[Riccardo Brasca]

This is the good place for such a question!

My personal advice is to choose a small theorem to formalize (maybe discussing the choice here) and then start working on it. For example, can you give an example of a "cryptography stuff" you would like to formalize?

[Alfredo Garcia]

yea sure, thank you Ricardo. I am interested on pure math as well but i do have a hard time understanding mathlib.
in the other hand i did some progress in a personal project, i have some code https://github.com/oxarbitrage/salsa20, is pretty crappy by now as i made it just for learning.

[Alfredo Garcia]

so basically i tried to formalize a cryptosystem called salsa20 and then prove some theorems about it found in some papers. at the end i think the most interesting one is that when the input is specially crafted you can get collisions in the hash function.

[Alfredo Garcia]

i guess one of my main problems is that i am kind of learning functional programming at the same time

[Riccardo Brasca]

mathlib is quite hard to read, especially if you don't know the math it's basically impossible to understand (it's nothing like a textbook to learn math). But formalizing a cryptosystem seems a nice project!

[Alfredo Garcia]

yea, exactly. even if you do know the math of some basic things mathlib is written a lot different than the textbooks

[Riccardo Brasca]

Yeah, the problem is that we choose from the beginning the most general definition to avoid having to redo stuff, so in practice it's unusable to lean math. For example there are no "vector spaces" in mathlib, only a generalization of them.

[Alfredo Garcia]

yea, that makes sense, the other way around (prove a theorem, build a personal project, etc) is easier but still complex enough for me to make more serious progress. for example, i think i picked the wrong datatypes in my project so i end up with ugly statements and proofs that i will like to avoid https://github.com/oxarbitrage/salsa20/blob/main/src/rowround.lean#L125

[Alfredo Garcia]

do you think a readme will help ? my plan is to refactor that project the most i can to be written in decent lean and then use it as a base to do more proves about the same or other similar cryptosystems.