Zulip Chat Archive

Stream: new members

Topic: Calculus with lean3


Icaro Costa (Jan 08 2023 at 17:51):

I am new to lean and would like to about how to work with basic calculus on lean3, more specifically about derivatives and how to import the necessary packages.

Sky Wilshaw (Jan 08 2023 at 17:58):

You should get set up with a project using mathlib by following TPIL. Then, you should be able to import the definitions of derivatives and such with import analysis.calculus.deriv.

Sky Wilshaw (Jan 08 2023 at 18:04):

If you're completely new to the language, I would recommend starting with something like the natural number game, then formalising mathematics. You can certainly work on calculus before that, but it may be challenging.

Sky Wilshaw (Jan 08 2023 at 18:05):

Notably, the natural number game runs entirely in a browser - no downloads required.

Icaro Costa (Jan 08 2023 at 18:07):

Thank you for the suggestions. Is there an easy way to downgrade lean4 to lean3 on a Linux machine?

Kevin Buzzard (Jan 08 2023 at 18:08):

Yes! You can have both versions running at once in fact (I have both versions of Lean on all my linux devices)

Kevin Buzzard (Jan 08 2023 at 18:08):

Just install Lean 3 and ignore the fact that you have Lean 4 installed.

Kevin Buzzard (Jan 08 2023 at 18:09):

https://leanprover-community.github.io/install/debian.html

Sky Wilshaw (Jan 08 2023 at 18:09):

Visual Studio Code (probably the most common Lean editor) can tell whether your project uses Lean 3 or Lean 4, you shouldn't need to set up anything complicated.

Sky Wilshaw (Jan 08 2023 at 18:09):

Installing both is perfectly fine, and it's what I've done too.

Icaro Costa (Jan 08 2023 at 18:32):

I keep getting this error for both the nightly and stable:

λ $  elan default leanprover/lean:nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2020-01-15
info: downloading component 'lean'
error: binary package was not provided for 'linux'

Is there a way to fix this? I'm on Kubuntu

Kevin Buzzard (Jan 08 2023 at 18:32):

Try updating your elan with elan self update?

Kevin Buzzard (Jan 08 2023 at 18:33):

2020 was a long time ago

Sky Wilshaw (Jan 08 2023 at 18:33):

Did you get elan through a package manager?

Icaro Costa (Jan 08 2023 at 18:33):

Sky Wilshaw said:

Did you get elan through a package manager?

Yes, I used apt to get it

Kevin Buzzard (Jan 08 2023 at 18:34):

Use the instructions I linked to above. Those are the official ones.

Sky Wilshaw (Jan 08 2023 at 18:34):

I think it's advised to install it directly, because package managers move quite slowly compared to the speed of lean development.

Kevin Buzzard (Jan 08 2023 at 18:34):

Uninstall using the package manager first.

Icaro Costa (Jan 08 2023 at 18:34):

Got it, let me try

Icaro Costa (Jan 08 2023 at 18:36):

Kevin Buzzard said:

Uninstall using the package manager first.

Alright, that worked!

Sky Wilshaw (Jan 08 2023 at 18:36):

Great! Installing with the instructions Kevin sent will also install some useful tools like leanpkg and leanproject, so they should all work now.

Icaro Costa (Jan 08 2023 at 18:39):

I think everything is working now. Thanks guys!

Patrick Massot (Jan 08 2023 at 18:43):

You should try https://leanprover-community.github.io/mathematics_in_lean/. It covers the basics and goes up to an introduction to calculus in Lean.


Last updated: Dec 20 2023 at 11:08 UTC