>>14419787I'd still like to talk to you.
I use Element (
element.io ) for communication and I can be contacted at:
{at}nylon{colon}
matrix.org(characters substituted against bots)
I'll suggest a few things before I go to bed:
Go through the natural numbers game first, if you get stuck there's a lean prover Zulip chat where you can ask for help. Then set up some axioms and set up a group, then have a go at proving various results with your group (that you already know from abstract algebra).
Also there's a lecture series on YouTube called "London Learning Lean" which has been getting recommended to me for some reason, but I can't vouch for it because I haven't watched it.
I didn't know that there would be people like you who have stumbled upon Lean by themselves - I thought it was still very niche. In any case I'll remember this, and maybe post about Lean here if I get up to anything over the summer!