Posted Friday October 27 2023.
I’ve been wanting to learn to use Lean4 for a while, but it’s so weird and hard. I followed the instructions on this page and ran the following command:
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
then rebooted by machine.
Next the page said I need to to install an editor like VS Code. But last I checked programming languages should not depend on an editor.
At this point if we run
lean in terminal they seem to be installed. What I would like to do is run
lean example.lean and have it return something. So, I followed the instructions on this page. It said to run
lake +leanprover/lean4:nightly-2023-02-04 new my_project math which makes a new folder called
my_project. Then I went into
my_project and ran
lake update, which “downloaded component: lean” (~200Mb). Then I ran
lake exe cache get and downloaded a bunch more files. Next we make a new folder,
my_project, and create the file
test.lean. In this file I wrote
import Mathlib.Topology.Basic #check TopologicalSpace
Then in termimal I ran the command
The output was
test.lean:1:0: error: unknown package 'Mathlib' test.lean:3:7: error: unknown identifier 'TopologicalSpace' test.lean:3:0: error: unknown constant 'sorryAx'
So clearly I did something wrong.