Can't create new project

Stream: lean4

[Icaro Costa]

Input:

leanproject new chain-rule

Output:

error: toolchain 'leanprover/lean4:nightly' does not have the binary `/home/icaro/.elan/toolchains/leanprover--lean4---nightly/bin/leanpkg`
Command '['leanpkg', 'new', 'chain-rule']' returned non-zero exit status 1.

[Henrik Böving]

We don't use leanproject in Lean 4 our tool is called lake (as in "Lean Make") and yhou create a new project with lake new

[Icaro Costa]

Henrik Böving said:

We don't use leanproject in Lean 4 our tool is called lake (as in "Lean Make") and yhou create a new project with lake new

Ok thanks. Now, how do I add the Mathlib package into the project?

[Henrik Böving]

require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

What are you planning to do with mathlib4? It is not nearly close to being finished porting

[Icaro Costa]

Henrik Böving said:

require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

What are you planning to do with mathlib4? It is not nearly close to being finished porting

I just started learning about this language, and I was following ChatGPT instructions on how to write the nth derivative of a function. However, from the looks of it, I was getting an inconsistent walkthrough. How do I write a derivative on it of nth order?

[Sky Wilshaw]

If you want to reason about derivatives you need to work with lean 3 until the port of mathlib is finished.

[Sky Wilshaw]

We still don't have the definition of the real numbers, let alone derivatives, in mathlib4.

[Hanting Zhang]

:fear: Like in the mathematical sense? mathlib4 is not done porting so derivatives don't exist

[Icaro Costa]

oh... so how would I do that on lean3?

[Sky Wilshaw]

What I mean is that derivatives have a definition, and that definition is not yet written in mathlib4.

[Sky Wilshaw]

You can get started with the web editor

[Hanting Zhang]

Also following ChatGPT is probably not the best way to learn Lean 4. Do you know about #FPIL and #TPIL?

[Hanting Zhang]

If you want to learn lean 3, the discussion is better suited for #new members