I want to install mathlib without any issues.

Stream: new members

[İmran Tanrikolu]

I am installing mathlib and all the necessary components in VS Code, but I keep having problems when testing Lean code. When I ask ChatGPT, it says that mathlib is installed incorrectly. Could you help me how to install it properly?

[Yaël Dillies]

Hey :wave: Can you give us more info about your setup? Are you working in a project? does it have an associate git repo? how did you create it? etc...

[İmran Tanrikolu]

example : ∀ m n : Nat, Even n → Even (m * n) :=

  fun m n ⟨k, (hk : n = k + k)⟩ ↦

    have hmn : m * n = m * k + m * k := by rw [hk, Nat.mul_add]

    show ∃ l, m * n = l + l from ⟨m * k, hmn⟩

For example, when I run the code above on VS Code...

ex11.lean:1:0Messages (1)

ex11.lean:1:0

c:\Users\sufig\.elan\toolchains\leanprover--lean4---v4.22.0-rc3\bin\lake.exe setup-file C:/Users/sufig/Desktop/MyProject/ex11.lean - failed:

stderr:
✖ [2/3] Running Mathlib.Data.Nat.Parity
error: no such file or directory (error code: 2)
file: C:\Users\sufig\Desktop\MyProject\.lake\packages\mathlib\Mathlib\Data\Nat\Parity.lean
✖ [3/3] Running setup (C:/Users/sufig/Desktop/MyProject/ex11.lean)
error: C:/Users/sufig/Desktop/MyProject/ex11.lean: bad import 'Mathlib.Data.Nat.Parity'
Some required builds logged failures:

• Mathlib.Data.Nat.Parity
• setup (C:/Users/sufig/Desktop/MyProject/ex11.lean)
  error: build failed

All Messages (1)

ex11.lean:1:0

c:\Users\sufig\.elan\toolchains\leanprover--lean4---v4.22.0-rc3\bin\lake.exe setup-file C:/Users/sufig/Desktop/MyProject/ex11.lean - failed:

stderr:
✖ [2/3] Running Mathlib.Data.Nat.Parity
error: no such file or directory (error code: 2)
file: C:\Users\sufig\Desktop\MyProject\.lake\packages\mathlib\Mathlib\Data\Nat\Parity.lean
✖ [3/3] Running setup (C:/Users/sufig/Desktop/MyProject/ex11.lean)
error: C:/Users/sufig/Desktop/MyProject/ex11.lean: bad import 'Mathlib.Data.Nat.Parity'
Some required builds logged failures:

• Mathlib.Data.Nat.Parity
• setup (C:/Users/sufig/Desktop/MyProject/ex11.lean)
  error: build failed

I get an error like this, not only on this code but on every definition and theorem I find in mathlib. ChatGPT tells me the problem is due to mathlib.

[Yaël Dillies]

İmran Tanrikolu said:

when I run the code above on VS Code...

Is the above code snippet the whole of your file? Are you sure you don't have imports?

[Yaël Dillies]

See #mwe for guidance on how to best communicate about code that doesn't work as you expect

[İmran Tanrikolu]

Yaël Dillies dedi:

İmran Tanrikolu said:

when I run the code above on VS Code...

Is the above code snippet the whole of your file? Are you sure you don't have imports?

https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html I took this code from the example in section 1.2 of the book.

[Yaël Dillies]

This code snippet in MIL isn't meant to work on its own, merely to demonstrate the difference between term-mode proofs and tactic-mode proofs

[İmran Tanrikolu]

Now I understand. So, where can I find large project code files that run on their own, for example, the proof of Fermat’s Last Theorem in Lean? How can I access such proofs? And finally, my account was suspended because of a joke I made yesterday—do you know how I can get it reopened?

[Yaël Dillies]

The canonical place to look for such projects is https://reservoir.lean-lang.org/. For example, if you look for "FLT" there, then you will quickly find https://reservoir.lean-lang.org/@ImperialCollegeLondon/FLT, which tells you the repository is https://github.com/ImperialCollegeLondon/FLT

[Rémy Degenne]

Creating new accounts to circumvent a suspension is not allowed.

[Michael Rothgang]

(And while I'm not a moderator, I strongly suspect that do so will get you instantly banned again once discovered. Just don't do that, please.)

[Eric Wieser]

do you know how I can get it reopened

All suspensions are temporary, for increasing periods with each offense. You should have received a message notifying how long your account was suspended for.