lean3 and lib on linux

Stream: new members

[Conrad]

hi guys,i am new to be here,i want to get leandojo and its lib3 in my virtual linux environment in docker.I've aliready get leandojo,but i don't know how to get its lib3,can you give me some advice?

[Notification Bot]

This topic was moved here from #announce > lean3 and lib on linux by Scott Morrison.

[Scott Morrison]

@Conrad, welcome! I've just moved your message here.

[Scott Morrison]

What do you mean by "lib3"?

[Conrad]

i mean a library that matchs with leandojo or lean3

[Conrad]

mathlib

[Conrad]

Scott Morrison said:

What do you mean by "lib3"?

hi bro,do you have few minutes to help me? @Scott Morrison

[Kaiyu Yang]

Hi @Conrad, resources related to LeanDojo can be found at leandojo.org. The first step would be working through Getting Started. Also, for questions specific to LeanDojo, you're welcome to ask here.