the right way to learn tactics

Stream: new members

[Victor Porton]

I took several attempts to learn Lean, and every time I stumble with tactics (especially to remember different tactics). Should I re-read everything but this time doing every exercise (that I skipped, as I usually skipped exercises when learning math, but Lean seems a different beast)? Also, I didn't try it in VS Code, not I do try to see goals interactively, and this seems to help... this (interactivity) was what I missed?

[Yaël Dillies]

Oh yes definitely! Interactivity plays a huge role in theorem proving, and maybe even in learning theorem proving.