New user: how to check a lean theorem from the CLI?

Stream: lean4

[ekelsiote]

Hi, I have created a new project using lake, and added Mathlib as a dependency. I can do the simple Hello World print function example which runs with:

lake update
lake build
lake run myproj

but I'm interested in checking a theorem. For example I have:

import Mathlib.Topology.Basic

#check TopologicalSpace

or

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

I don't know how to 'run' either of these. When I try the above commands I get a linker error about a missing main function. I can't see anything in the documentation. I know there's the LSP integration for my editor (nvim), but first I just want to check it via the CLI.

How do I do this? I tried everything.

Thanks

[Kim Morrison]

Can you show us your lakefile.toml? You want a lean_lib there, not a lean_exe.

[ekelsiote]

Hi, thanks:

name = "llll"
version = "0.1.0"
defaultTargets = ["llll"]

[[lean_exe]]
name = "llll"
root = "Main"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[ekelsiote]

I now tried:

name = "llll"
version = "0.1.0"
defaultTargets = ["llll"]

[[lean_lib]]
name = "llll"

[[require]]
name = "mathlib"
scope = "leanprover-community"

with

import Mathlib
import Mathlib.Topology.Basic

universe u

variable (X : Type u)

open Set

#check (univ : Set X)

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

#check TopologicalSpace

I now see the output:

$ lake build
⚠ [7118/7119] Built llll
info: llll.lean:10:0: univ : Set X
info: llll.lean:15:0: easy : 2 + 2 = 4
warning: llll.lean:17:8: declaration uses 'sorry'
info: llll.lean:20:0: hard : FermatLastTheorem
info: llll.lean:22:0: TopologicalSpace.{u} (X : Type u) : Type u
Build completed successfully (7119 jobs).

Does that mean it worked? Is lake build the main command then to check the proof validity?

Thanks

[ekelsiote]

Also: is there a way to have a main that executes but also do theorem checking?

[Ruben Van de Velde]

Yes, it worked

[Ruben Van de Velde]

You can run lake build directly, but for theorem proving you'll generally want to use an editor that shows the infoview, such as vs code

[Niels Voss]

To be clear, #check just checks to make sure the proof exists in the environment and has compiled properly, and then prints out its type. It isn't what we would consider "checking" proof validity. In this case, #print axioms hard would give you a list of axioms that the statement depends on. Lean is not secure against adversaries, but for practical purposes #print axioms is probably the closest thing to checking proofs.

[Michael Rothgang]

Lean is not secure against adversaries

There are tools (lean4lean and friends) that can check against most practical exploits. Yes, at some point your bets are off (the attacker writing to proc/mem/manipulating your lean executable/ you name it), but there is good defense against your typical "here's a bunch of Lean code, check that it really does what it says".

[Henrik Böving]

(the attacker writing to proc/mem/manipulating your lean executable/ you name it)

both of these situations are pretty trivial to handle by using modern Linux sandboxing capabilities and a good verifier architecture

[ekelsiote]

Thanks Ruben & others. I think lake build then is what I want. I'll now setup an infoview in nvim and cross check it with the lake build output. Thanks still learning about lean.