Where to look for theorem or tactics?

Hi, I am learning Lean4 for the purpose of LLM accelerated proof writing, thank you so so much for writing this book and posting it online open sourced. This book is easier than the other several books mentioned in the Lean4 official documentations and it comes with more examples and a more comfortable learning curve.

In short I want to let LLMs learn to master this language and freely translate between natural language and Lean4 for starter. As I am reading through this book I realize that for me the biggest issue is to "locate which tactic or theorem to use". Most of the time I know the next steps of the correct proves, yet I don't know how to express it in Lean4, same as the LLM we are training. (For example from t^2 = 0 to t = 0 when t in Real requires a tactic called pow_eq_zero and this wasn't mentioned anywhere, I looked up Cancel.Lean manually to spot it). Is it possible to formulate a quick cheatsheet that list all possible tactics and briefly discuss when they are applicable? Thanks!

Hi @jiamingkong, I'm not affiliated with this project. However, I do have a few links that may help.

Tactic resource description	Link
Comprehensive list	https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md
A list with examples	https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_C/tactics/tactics.html
Spreadsheet with usage	https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit?gid=0#gid=0
Course Tactic Reference	https://course.ccs.neu.edu/cs2800sp23/ref.html

By now you may have already found these documentation tools, but if not, pow_eq_zero and other theorems can be located quickly by using these following search engines.

Search engine name	link
lean4 docs	https://leanprover-community.github.io/mathlib4_docs/
Search by proof type	https://www.moogle.ai/
Seartch by proof type	https://loogle.lean-lang.org/

It looks like Loogle has integration with VS Code, so maybe they have an API worth exploring?