List of theorems

Stream: new members

[jakub]

Hey is there a list of lean theorems I could learn to be able to do basic algebra?

[Kevin Buzzard]

I'm pretty sure I've seen a huge textbook (500+ pages) called "basic algebra" so I think you're asking the wrong question. All standard results are in the library or are easily derivable so I think your question should be "how do I search the library to find the result I need in basic algebra" and answers include exact?, loogle, leansearch.net and so on.

[jakub]

Kevin Buzzard said:

I'm pretty sure I've seen a huge textbook (500+ pages) called "basic algebra" so I think you're asking the wrong question. All standard results are in the library or are easily derivable so I think your question should be "how do I search the library to find the result I need in basic algebra" and answers include exact?, loogle, leansearch.net and so on.

I was moreso looking for a list of lean theorems that I could memorize to do algebra proofs in lean, sort of like the small lists with a couple theorems they have in Theorem Proving in Lean 4 but more comprehensive. But I suppose no such resource exists as of yet.

[Kevin Buzzard]

And what I'm saying is that this list has size in the hundreds if not thousands so you can't memorise it. It sounds to me like you would be better off learning the #naming convention.

[jakub]

Makes a lot of sense, thank you very much.

[Kevin Buzzard]

Posting explicit examples of lemmas you're interested in knowing the names of would also be a useful way to proceed in this discussion, ie making it concrete rather than theoretical.

[jakub]

I greatly appreciate your willingness to help, but unfortunately I don't have any concrete examples at the moment. I was approaching learning Lean from the angle of acquiring a decent vocabulary of theorems which I could then use to prove things. I didn't know looking up theorems as you need them was the expected approach.

[Adomas Baliuka]

A good way to start (at least it has been for me thus far) is just pick some problems to work on. If you want to use algebra, look at some algebra homework you had (at any point in your studies) and try to formalize it. If you can't, try something easier. If it's too easy, try something more advanced...

It's nice to have informal proofs at hand because formalizing and finding the right ideas for how/why the proof works in the first place can be too much at once (at least for me). Solving problems informally ("on paper") first can help a lot. However, while surely a nice exercise, this usually means spending a lot of time not actually learning how to formalize.