Alexey Sorokin, new member + Lean questions

Stream: new members

[Alexey Sorokin]

Hello everyone!

My name is Alexey Sorokin, I am an Education Specialist in Input | Output.
I am working on a project called IO Maths Academy, where we are running open to everyone math courses.

We are interested in using Lean 4 and mathlib for theorem proving in our programs. 

I got very positive feeling once I've finished Natural Number Game as it is pretty much the same as I do in categories. I wish to continue learning and using Lean and to create my own math projects.

I have several questions about difficulties that I've faced with learning Lean 4 on my own.

1) I have permanent troubles with installing mathlib for Lean 4. Following the instructions on Lean 4 website doesn't solve my problems. I need someone to help me, to show where my mistakes are. More details I can explain to the person who can help me (constant not-up-to-date mathlib with errors or problems with versions, toolchain, cache get, etc. during installation).

2) Where and to whom can I address my questions related to Lean 4 / mathlib installation and development? I am interested in adding my results to category theory packages, once I'll be able to use mathlib.

Best regards,

Alexey Sorokin

[Kevin Buzzard]

For (1) you need to post the errors. You also need to clarify if you're working with mathlib or with a project which has mathlib as a dependency. For (2) ask in this channel #new members