Introducing myself: Jan Engler

Stream: new members

[Jan Engler]

Hi, I am a high school student from Czech Republic. Our country has a program called Students' Professional Activities (SPA), where students study something for a year and then write a paper about it. I chose to write about constructive logic and one of the things I have to wrap my head around is type theory. While reading about it a week ago, I came across lean and I was very impressed - i'd like to use it in my work and maybe talk about the Curry-Howard isomorphism. I also believe that things like lean will be important for the future of math, which I want to participate in. I'm currently a noob both in lean and zulip, I just played NNG and am going through theorem_proving_in_lean exercises. I got stuck in chapter 4 exercise 2:

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
iff.intro (λ (a:∀ x, p x ∨ r), or.elim (a y) (λ (b: p x), or.intro_left r (λ (x:α), b) ) (λ (c:r), or.intro_right (∀ x, p x) c))
("fill this in l8r")

I have a problem with "λ (x:α), b": I want it to be a proof of ∀ x:α, p x but lean says that it has type α → p x. I am a bit confused about what how functions from types to propositions are different than general quantifiers over a term of that type. I actually don't know much about type theory yet, we only studied intuitionistic propositional logic (IPL) and a bit of model theory with my advisor, so I might just be dumb. Thanks for help in advance.

Additional questions:

1. How far can I get using only lambdas? I like the simplicity, although it may be hard to read after I type it, I'm starting to get used to it. I learned tactics in NNG and the theorem_proving_in_lean tutorial uses something very different, but I don't want to learn so much language-specific syntax that I will forget anyways. I also like how the expressions I type in are very similar to what lean prints when I type

#print (something)

so for example, when I forget how to use a certain introduction rule, I can just print the name of the rule and see what to do very simply. What do you veterans use - tactics, type mode, lambdas, or a mix?

2. Is there someone trying to formalize physics in lean, and if no, would it be theoretically possible? I will have to get way better at lean in order to play with something like that, but I'd like to know if it's a rubbish idea or something that could work. The idea is that you could declare laws of physics as axioms in some library. For example, if I had a library with analysis and things like gateaux derivatives, I could add the principle of least action, derive the Euler-Lagrange equations and then use them to solve some problems in classical mechanics. I listened to Kevin Buzzard talk about lean a lot, and he talks about it like a game: for math, making levels is stating theorem and solving levels is proving theorem, for physics making levels would be making physics problems and solving levels would be stating what the answer is and proving it. I think physics has huge issues with rigor and somehow formalizing it would surely help.

3. I also checked out the programming_in_lean tutorial, but most of the chapters seem to not be finished. When will it be finished / is there a different tutorial I can use? I wanted to learn a functional programming language for a long time anyways, and when I will be already using lean for theorem proving, I might as well use it for other stuff instead of, say, Haskell.

[Kyle Miller]

(Zulip hint: backticks let you write code blocks:

```
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
iff.intro (λ (a:∀ x, p x ∨ r), or.elim (a y) (λ (b: p x), or.intro_left r (λ (x:α), b) ) (λ (c:r), or.intro_right (∀ x, p x) c))
("fill this in l8r")
```

becomes

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
iff.intro (λ (a:∀ x, p x ∨ r), or.elim (a y) (λ (b: p x), or.intro_left r (λ (x:α), b) ) (λ (c:r), or.intro_right (∀ x, p x) c))
("fill this in l8r")

and single backticks can be used for inline code)

[Kyle Miller]

The λ (x:α), b term is a proof that ∀ y:α, p x. The α → p x notation is equivalent to ∀ y:α, p x.

[Kyle Miller]

Regarding 1, technically you can do everything using only lambdas (these are known as "proof terms"), and if you are interested in this sort of thing it is worth understanding how to write proofs directly like this. You can get a lot more done if you use tactics, too.

[Wojciech Nawrocki]

3. I also checked out the programming_in_lean tutorial, but most of the chapters seem to not be finished. When will it be finished / is there a different tutorial I can use?

If you are referring to the book here, it is quite outdated and will likely never be finished as attention slowly shifts to the upcoming version of Lean, Lean 4. A great newer resource for the current version (Lean 3) is the Hitchhiker's Guide.