drhodes
commented
3 weeks ago | 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?
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_zeroand 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!