Zulip Chat Archive

Stream: general

Topic: Newly Downloaded

Sean G McCain (Oct 31 2018 at 21:38):

I am using LEAN for a discrete math class. I just downloaded it for a project. Is there anything that I need to also download or is using the LEAN extension in Visual Studio all I need to get going?

Andrew Ashworth (Oct 31 2018 at 21:47):

nope, the lean extension + lean is all you need to start hacking around

Chris Hughes (Oct 31 2018 at 21:47):

This should help https://www.youtube.com/watch?v=2f_9Zetekd8

Sean G McCain (Oct 31 2018 at 21:49):

I have a Mac. Is that going to change anything?

Chris Hughes (Oct 31 2018 at 22:08):

I think there's another video on macs.

Chris Hughes (Oct 31 2018 at 22:08):

Look at Scott's channel

Kevin Buzzard (Oct 31 2018 at 22:40):

https://www.youtube.com/watch?v=k8U6YOK7c0M&t=7s is the mac one. If you are only doing super-basic maths then core Lean might have what you need, but the moment you want something like the binomial theorem you're going to need the maths library.

Last updated: Dec 20 2023 at 11:08 UTC