Getting Started With Lean Theorem Provers

Stream: general

[Jony Vale]

Hello everyone. I am trying to get leanprojects running on my Mac m2 and I am stuck on a point.

I seem to have successfully completed steps 1 through 5 on https://leanprover-community.github.io/install/macos.html as I got "successfully installed" messages for in the form of

1. “visual-studio-code was successfully installed!”
2. “Extension 'leanprover.lean4' v0.0.108 was successfully installed."

My goal is to run the code “leanproject get ImperialCollegeLondon/formalising-mathematics-2022”

On the standard Terminal of Mac. I am not sure if I need to add some symbol before that code, or if I need to download a new terminal that recognizes that code., but it doesn’t seem to work.

I am following Lecture 1 on Professor Buzzard’s course on Formalizing mathematics via this YouTube video:
https://www.youtube.com/watch?v=3XaL0tjnWSk&list=PLVZep5wTamMmRPvCLO4WVpCwkTi1F6OyF&index=1

At minute 2:00 in the video above, Professor Buzzard types “cd lean-projects/“ and then he types in the code of interest “leanproject get ImperialCollegeLondon/formalising-mathematics-2022”.

Can anyone please advise me on what to do in order to get started in this course? I would like to familiarize myself with Lean so that I can contribute to mathlib as well as understand how mathlib is organized in hopes of designing a Centralized Education Platform that I am building that I hope can stimulate mass contributions to digitizing mathematics

Note: a follow up post regarding the Centralized Education Platform will be made shortly, I should finish an interactive prototype design for the platform mid August, and though I would prefer to make the post about the platform after the prototype is made so that I can include the prototype in the post to gather feedback and hopefully find collaborators, it might be best to make an initial post before the prototype is made in case there are relevant inputs that might shape the design of the platform to include features that will facilitate such contributions.

[Scott Morrison]

Oops! leanproject is only relevant for Lean 3, but the instructions you are following from https://leanprover-community.github.io/install/macos.html are for Lean 4!

[Scott Morrison]

I would suggest you stick with Lean 4 (Lean3 is end-of-life and not taking further contributions).

[Scott Morrison]

Instead of following the instructions from Kevin's video, instead continue on to the instructions in https://leanprover-community.github.io/install/project.html

[Scott Morrison]

That will get you set up with the "mathematics in lean" project, which is a good learning resource!

[Jony Vale]

Awesome, thanks a lot! I'll try to get started with the link you provided for now, much appreciated!

[Patrick Massot]

As a general rule, following a one year old video about Lean is very unlikely to do you any good. We are moving way faster than that.

[Scott Morrison]

Particularly at the moment the transition to Lean 4, while a huge step forward, is quite disruptive, and has made lots of learning materials obsolete. We're getting there --- please rely on zulip to ask questions when you get stuck!

[Henrik Böving]

Could we maybe get some banners on the material going if it is still editable by us? Like on github projects a warning in the Readme and on websites one of these top of the page banners that inform people about this?

[Jony Vale]

Thanks a lot guys! I appreciate the advice. I'm much more of a pure math guy than a computer guy, but I am making progress. It seems I am now in the process of cloning clone https://github.com/leanprover-community/mathematics_in_lean.git. This might not be exactly what I am looking for, but ChatGPT is pretty much guiding me the whole way through. I will post if I get stuck I appreciate the support!

[Kevin Buzzard]

ChatGPT was trained up to 2021 when Lean 4 didn't really exist, so this is a dangerous approach. But the mathematics in Lean repo which you're cloning is a perfect place to start in 2023.

[Jony Vale]

Thanks for the warning Professor Buzzard! I did not think about this. However, what I did was I copied the relevant text that Scott Morrison referred me to (https://leanprover-community.github.io/install/project.html) and pasted it into ChatGPT. It spat out the following instructions which seems to have been working so far. I have successfully completed step 4 “clone the project” and now see that this might be exactly what I need as it is a PDF book that is using Lean4. Now I am in step 6 of the instructions (it just finished actually, and there are no error messages so I am tempted to move to step 7). Below and it seems to be going well. Please advise me if this will get me into trouble! I definitely dont want to ruin my computer!

Here is ChatGPT’s instructions:

Sure, let's break down the instructions step-by-step, and I'll guide you through each one.

First, ensure you have all the prerequisites installed on your Mac M2:

1. Git: If you don't have it, you can download and install it from here.
2. VS Code: Download and install it from here.
3. Lake: This tool manages Lean projects. Instructions to install it should be in the full lake documentation. Refer to that or let me know if you need help finding those details.

Now, let's follow the instructions to work on an existing project, like the Mathematics in Lean book:

1. Open Terminal: It can be found in the Applications folder or by searching in Spotlight.

2. Type the Command: If you haven't logged in since installing Lean and mathlib, type:

   source ~/.profile

   or

   source ~/.bash_profile

3. Navigate to Directory: Choose the directory where you'd like the project to live (e.g., your home directory) by using:

   cd path/to/your/directory

4. Clone the Project: Run:

   git clone https://github.com/leanprover-community/mathematics_in_lean.git

5. Enter the Project Directory: Run:

   cd mathematics_in_lean

6. Get Cache: Run:

   lake exe cache get

7. Launch VS Code: If you've set up VS Code to launch from the command line, you can type:

   code .

8. Open the Project in VS Code: If you launched VS Code from a menu, click "Open" and choose the folder mathematics_in_lean.

9. Explore: Follow the MIL instructions to explore the book and exercises.

For creating a new Lean project, you can follow the second part of the instructions provided. If you have any issues or uncertainties with any of the steps, please let me know, and I'll help you through it! It looks like you've got a very comprehensive guide, so you should be well on your way to getting everything set up.

[Patrick Massot]

I don't understand: why you are using ChatGPT instead of following reliable instructions?

[Jony Vale]

Lol, I can't remember the error I got, but something went wrong. In any case, it is all good now. I think it might have been a silly error, as ChatGPT gave me essentially the same advice as the reliable instructions. I believe that I was trying to follow Creating a Lean Project rather than follow Working on a Lean Project. Like I said though, I am now officially have everything set up.
I have the book opened inside Visual Studios along with the repository.

[Jony Vale]

I actually find the "setting up process" very cumbersome, and look forward to the day that an OS or terminal is an AI that can handle all of that kind of stuff for you by you just asking for it using plain English

[Jony Vale]

I hope I am not in the wrong stream for asking questions about problems I encounter while running code for Mathematics in Lean. I can change to a different stream or create a new one. In section 1.2 Overview, I get errors while running the first lines of code (and yes, ChatGPT is definitely not with this stuff). In particular, when I type in the code

#check 2 + 2

def f (x : N) :=
x + 3
#check f

the first check is underlined in blue. the x + 3 is underlined in red, and the f is underlined in red. Hovering over the line "x + 3", I see:

"failed to synthesize instance
HAdd ℕ Nat (?m.112 x)Lean 4
?m.112 x
a + b computes the sum of a and b. The meaning of this notation is type-dependent.

No quick fixes available"

Can anyone give some advice or point me to a relevant thread for basic questions on running Lean, please?

Note: I think that book said to copy the Mathematics in Lean folder so I can update it later, and I did this and named the new folder Jony-Lean. I can open it just as before and it has the book along with the side bar (repository?) which includes MIL folder with the files that have some code built into it.

Again, sorry for the basic question!!

[Jony Vale]

Never mind, I think I got it. needed to import a few things....my bad....

[Eric Wieser]

Can you edit your post to use #backticks?

[Jony Vale]

I'll try now! I was working inside the file S01_Getting_Started.lean which did not import anything…when I switched to the file of the section I am on S02_Overview.lean, I saw that I was missing 3 imports and an open Nat line. This eliminated the red underlined squiggly line and brought some peace. I think all is well now….I hope I am using the backticks properly, but this is the code:

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Parity
import Mathlib.Tactic

open Nat

#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

I think all is well now!

[Alistair Tucker]

Patrick Massot said:

I don't understand: why you are using ChatGPT instead of following reliable instructions?

I don't understand why the "reliable instructions" are still telling M1/M2 owners to run the x86 version of Lean using Rosetta.

[Scott Morrison]

Could someone with an M1/M2 machine please PR better instructions? I'll get there when I have one, otherwise. :-)

[Alistair Tucker]

@Jony Vale Would you like to make your first contribution sooner rather than later? If so, and if you are not using it for anything else, I suggest deleting the x86 installation of Homebrew and starting again. To that end, quit VS Code, download the Homebrew uninstall script into your home directory and run it with /bin/bash uninstall.sh -p /usr/local. Now you can go back to the Mathlib install page and follow the instructions as written for Intel Mac. Tell us what happens! I have just performed the latter step on my own M1 machine and it was successful modulo a failure to detect that VS Code was already installed. If you too end up with a working installation of Apple silicon-native Lean, please make a PR to change the install webpage here. Just strip out the M1 Macs instructions and also remove the qualifying subtitle Intel Macs. I will delete my own equivalent PR which is clearly going nowhere.