New to Lean

Stream: general

[Nick Gholami]

Hi, im new to Lean and Zulip so hope im doing this right. I researched Lean a bit, but cant seem to fully comprehend it. Is Lean a programming language or is it a program written in some other language? Does Lean create mathematical proofs or does it guide people who are doing so, and makes sure they dont make any mistakes or contradictions or something like that?

[Anne Baanen]

Welcome! Lean refers both to a programming language, and a compiler that lets you run code written in Lean the language. (The newest version of Lean-4-the-program is actually written in Lean-4-the-language.)

[Anne Baanen]

Lean is what is called an interactive theorem prover, which basically means that you have to write the proof yourself and Lean assists/checks it. This is in contrast to automated theorem provers, which you can hand a statement and they try to prove or disprove it automatically.

[Anne Baanen]

(Lean can actually do a little bit of automatic reasoning, but in general you have to supply more details of a proof to Lean than you would write down in a pen-and-paper proof.)

[Anne Baanen]

(Another side note: there are other programs that can read (pre-processed) Lean code and check the proofs for correctness. But a typical user interaction is with Lean-the-program.)

[Nick Gholami]

Anne Baanen said:

Lean is what is called an interactive theorem prover, which basically means that you have to write the proof yourself and Lean assists/checks it. This is in contrast to automated theorem provers, which you can hand a statement and they try to prove or disprove it automatically.

Thanks for the detailed answer, really appreciate it. Can you recommend any automated theorem provers? I'm a student and would like to create an automated theorem prover in my spare time, if possible.

Are there any tutorials or documentation for Lean I can follow. Or do I have to learn it simply by trial and error?

[Mario Carneiro]

#tpil is a good book for getting started with the concepts of lean

[Mario Carneiro]

more generally see anything on https://leanprover-community.github.io/learn.html

[Mario Carneiro]

If you want to write an automated theorem prover, I think lean would actually be a fairly good environment to do so in

[Mario Carneiro]

Most existing ATPs are probably too complicated to understand for pedagogical purposes, but I recommend the Handbook of Practical Logic and Automated Reasoning for learning the foundations of ATPs

[Alexander Bentkamp]

@Stephan Schulz has created a simple ATP for pedagogical purposes: https://github.com/eprover/PyRes. Maybe you'd be interested in playing with it.

There will also be a tutorial for PyRes next week: https://www.cs.cmu.edu/~mheule/CADE28/#events ("Practice of First-Order Reasoning")

[Huỳnh Trần Khanh]

From what I gathered there are things that first order reasoning can't capture right? Like... it can't express most of modern mathematics right?

[Mario Carneiro]

Not really, you can encode anything in first order logic, including higher order logic and DTT. It's sort of like turing completeness for mathematical formalisms - they all interpret each other

[Mac]

Anne Baanen said:

Lean is what is called an interactive theorem prover

I would note that, while this is true, one of the major goals of Lean 4 is for it to also just be a good general purpose programming language.

[duck_master]

wait @Mac how is Lean a programming language?

[Mac]

@duck_master what do you mean by that?

[Eric Rodriguez]

lean is basically a general-purpose functional programming language

[duck_master]

like with my (very small) exposure to Lean, I'm only familiar with it as a theorem prover (i.e. you type in a proof and then you either get "this is a correct proof!" or "this is a wrong proof!"). I think you meant that Lean was basically a platform to run arbitrary computer programs, and so I wondered how that would be possible if it is.

[Mac]

Well yes, you can use it that way. You can also just write a main function in Lean and compile a program into an executable.

[Mario Carneiro]

Mac is thinking more about lean 4, which is certainly aiming to be "the next haskell", i.e. to do general programming in a functional style, in addition to its use as a theorem prover

[Mario Carneiro]

Lean 3 can be used for general programming as well, but it is not very efficient so you primarily see this capability being used for tactic programming

[Eric Rodriguez]

out of curiosity, what were lean 1 and lean 2? i've seen like 0 references to either of them

[Mac]

Thanks for the addendum @Mario Carneiro . I too only used Lean 3 for theorem proving so I was not sure how much of my new knowledge of the general purpose use of Lean 4 translated back to Lean 3.

[Mario Carneiro]

Eric Rodriguez said:

out of curiosity, what were lean 1 and lean 2? i've seen like 0 references to either of them

Lean 1 is mostly lost to history, although @Jeremy Avigad can probably tell the story better than I. Lean 2 was used a fair amount, and in particular it had support for HoTT; most of @Floris van Doorn 's thesis was written in lean 2. You can find the repo at https://github.com/leanprover/lean2

[Eric Rodriguez]

woah, I never knew Lean had HoTT support apart from the "hack" that's out there; that's pretty cool

[Mario Carneiro]

Lean used to be more similar to Coq in aspirations of type theoretic generality. The versions have been progressively removing these in favor of more focus on conventional mathematics

[Mario Carneiro]

There used to be a bunch of kernel flags to change whether the pi is impredicative, what inductive types are supported, whether Prop exists and so on

[Mac]

Mario Carneiro said:

Lean 2 was used a fair amount, and in particular it had support for HoTT; most of Floris van Doorn 's thesis was written in lean 2. You can find the repo at https://github.com/leanprover/lean2

This is somewhat off-topic, but that link just made me realize HoTT stands for Homotopy Type Theory. I had always mistakenly thought it stood for Higher-order Type Theory. :rolling_on_the_floor_laughing:

[Mario Carneiro]

it wouldn't be capitalized that way if so, I guess. HOL isn't HoL

[Mac]

Which also always confused me, because by usual English standards of initials, Higher-order should be initialized H or Ho (i.e., the o in the initial would be lowercase) because the o in the actual word is lowercase (and is not, in fact, a separate word).

[Mario Carneiro]

usually all words in an acronym are capitalized except conjunctions or connective words like "of", which are either omitted or lowercase

[Mario Carneiro]

then again, I think the rules are often bent, especially if there is an opportunity for a backronym

[Mac]

Mario Carneiro said:

usually all words in an acronym are capitalized except conjunctions or connective words like "of", which are either omitted or lowercase

True, but that would make higher-order logic HL (since higher-order is one word). When abbreviating a single word with multiple letters (like with Homotopy) the other letters are usually lowercase.

[Mario Carneiro]

I'm not sure why HTT wasn't considered a good choice for homotopy type theory, maybe there is another type theory out there with the same initials?

[Kyle Miller]

(Hyphenated words are title-cased, too, in many style guides. It'd be Higher-Order Logic, since "order" is the right part of speech to be upper-cased.)

[Mac]

Kyle Miller said:

(Hyphenated words are title-cased, too, in many style guides. It'd be Higher-Order Logic.)

While that may be true, Wikipedia disagrees: https://en.wikipedia.org/wiki/Higher-order_logic :P

[Mario Carneiro]

wikipedia isn't title casing though

[Mario Carneiro]

logic is also lowercase

[Mac]

Mario Carneiro said:

wikipedia isn't title casing though

You are right, my bran must have auto corrected that XD.

[Mario Carneiro]

Here are some titles in the references:

• "Foundations Without Foundationalism: A Case for Second-Order Logic"
• "Classical Logic II: Higher Order Logic"
• "Automation of Higher-Order Logic".
• "Second-order and Higher-order Logic"

So really all variants seem to be attested

[Jeremy Avigad]

What, storytelling? Twist my arm!

There never was a Lean 1. Leo started the project in 2013 and called the first version Lean 0.1. You could only run it from the command line, but that was o.k., because it was really fast. We started the library with natural numbers and lists and so on, and Floris van Doorn developed the first version of the integers. I spent a month with Leo at Microsoft in the summer of 2014, and by then he was working on Lean 2, so my first task was to port the library from Lean 0.1. Soonho Kong started his Microsoft internship on the same day (we went through the mandatory Microsoft orientation together) and he got to work right away on developing an Emacs mode, using Flycheck for continuous checking. HoTT was all the rage at the time and Leo incorporated a HoTT mode in Lean 2, so I also started the HoTT library that summer, but then Floris and Jakob von Raumer and eventually Ulrik Buchholtz took that over. Leo worked out the details of managing structures and an algebraic hierarchy with type class inference, and I spent most of my time the following year porting the algebraic hierarchy from Isabelle, through ordered fields or so. The following spring Rob Lewis and I spent a few months visiting Jon Borwein in Newcastle, and Rob implemented the real numbers there. At the time we were more invested in being constructive wherever possible, so we encouraged poor Rob to do a constructive formalization of the real numbers, along the lines of Bishop's book.

Those were the good old days! We started moving to Lean 3 in 2017. Mario split mathlib off from core lean that summer, during the Big Proof program at the Isaac Newton Institute in Cambridge. Some of the library survived from Lean 2 --- the natural numbers, lists, integers, and the algebraic hierarchy had their origins there, but Mario rewrote (and wrote) a lot. Johannes Hölzl did a postdoc at Carnegie Mellon the following year, and added a lot. He restarted the topological library and filters from scratch and went a lot further. Then people like Patrick, Kevin, and Johan got involved, and then Jasmin Blanchette launched Lean Forward, and people kept coming and coming, and the rest is history.

(I'm probably leaving out some important bits, so I hope others will chime in.)

[Jeremy Avigad]

Oh, and I forgot about Gabriel Ebner and Sebastian Ullrich, who started contributing to Lean 3 in 2016, IIRC. They got the emacs mode for Lean 3 working, and Gabriel got Lean 3 using multiple cores. Daniel Selsam started working on Lean in 2015 or 2016, I think. Jared Roesch wrote the first VS Code extension. I am probably leaving out lots of others -- I apologize for that.

[Bowen Liu]

Has any commercial company shown interest in the project? I think if the industry got involved the pace of development might be much faster.

[Bowen Liu]

Education companies like Wiley?

[Bowen Liu]

Then there would be devoted math graduates doing this instead of mathematicians

[Bowen Liu]

with more investments and a huge professional teams

[Bowen Liu]

Maybe in the near future

[Daniel Selsam]

@Bowen Liu Several of us in Microsoft are very interested in supporting/developing a polished, universally accessible, advanced-high-school-level, AI-auto-grading proof-based math/cs course on top of Lean. We are just starting to think about possible partners and collaborators.

[Bowen Liu]

ah got ya

[Bowen Liu]

@Daniel Selsam That's very uplifting news

[Jeremy Avigad]

It occurs to me to make one correction to the story above: when Soonho Kong arrived at Microsoft in the summer of 2014, I am pretty sure it was his second Microsoft internship. He contributed a lot to the core development of the early versions of Lean. That summer, he also got Lean running in a browser, which was unheard of at the time.

[Sebastian Ullrich]

In fact he is still the top contributor after Leo in the community fork, though someone usurped him in the Lean 4 repo and Gabriel is getting close in the fork...

[Jeremy Avigad]

Here he is: https://soonhokong.github.io/. He is still a legend in my mind. You can get a sense of how intense he is from this old CMU web page: http://www.cs.cmu.edu/~soonhok/synergy-security-and-tips.html. He is the one who taught me how to use git; we used to call him the "git whisperer" because he would clean things up when we made a mess of things.

[Scott Morrison]

(Abbreviating "homotopy" as "ho" rather than "h" is standard in algebraic topology, e.g. hocolim for the homotopy colimit.)

[Martin Dvořák]

Hello! Can I get a hint regarding the Lean/mathlib tutorial?

I am stuck with the last exercise in 02_iff_if_and. I don't know how to prove two intermediates steps:
gcd a b ∣ a
gcd a b ∣ b

[Ruben Van de Velde]

Those sound like lemmas that should be available - try library_search to find them

[Martin Dvořák]

Thanks a lot! They were gcd_dvd_left and gcd_dvd_right.

[Patrick Massot]

Using those lemmas is not at all the spirit here. All exercises in the tutorials can be solved using only the lemmas mentioned in the tutorials.

[Martin Dvořák]

Unfortunately, I didn't know how to do it using the lemmas from the tutorial.

[Patrick Massot]

If you tried and couldn't succeed there is no dishonor in having a peek at the solution file.

[Martin Dvořák]

New "big problem": How can I obtain FALSE from having foo > bar and foo = bar at the same time?

[Mario Carneiro]

the easy way is ne_of_lt

[Patrick Massot]

linarith will handle that.

[Mario Carneiro]

that's the easier way :grinning_face_with_smiling_eyes:

[Martin Dvořák]

Is there an "atomic" proof term that will do it?

[Mario Carneiro]

ne_of_lt

[Patrick Massot]

Mario, we're discussing in the context of the tutorial.

[Martin Dvořák]

Thanks!

[Mario Carneiro]

I don't know what's in the tutorial. I guess linarith is the only presented solution?

[Patrick Massot]

The tutorial comes from my teaching where clearly the goal is that automation takes care of all steps where you wouldn't write anything on paper.

[Martin Dvořák]

Oh yes, linarith was mentioned at almost the beginning. If I am trying to be more low-level than the tutorial suggests, there is probably something wrong with my attitude.

[Mario Carneiro]

#tpil teaches a lower level approach to things, which is useful for understanding what is going on behind the scenes and can help with more advanced usage. I wouldn't call it wrong, but the tutorial is aimed for a different style of usage

[Patrick Massot]

It's not "wrong". What would that mean? But doing so means you would be fighting against the tutorial, but I assume you're a grown-up and you do whatever you want.

[Mario Carneiro]

In particular, given the choice between a proof by linarith and a proof by ne_of_lt in mathlib, we would usually choose the latter because it compiles faster

[Martin Dvořák]

How come it produces FALSE and not just foo \neq bar instead? It works and I am puzzled why.

[Martin Dvořák]

Maybe because neq is a function as well?

[Mario Carneiro]

because foo \ne bar is equal by definition to foo = bar -> false, so it's secretly a function taking one more argument

[Martin Dvořák]

From equality to FALSE?

[Martin Dvořák]

Very nice!

[Patrick Massot]

This whole negation stuff is covered extensively in the tutorial

[Martin Dvořák]

Is there a more idiomatic way to write by_contradiction ass if I am not going to use ass anywhere in the proof?
(case analysis ... this case will never happen ... lemme show why)

[Mario Carneiro]

as in you just want to prove false instead of the goal? That's exfalso

[Martin Dvořák]

Oh yeah, that's it! I saw it in the Natural Numbers Game but forgot about that.

[Mario Carneiro]

but I usually find it's not needed, since usually a proof of false will also be a proof of anything

[Martin Dvořák]

I think I want to use it frequently it after cases.

[Mario Carneiro]

one trick you can use if you have a proof term that is literally false is to replace exact foo with cases foo

[Patrick Massot]

This is all covered in great detail in files 7 and 7bis of the tutorial.

[Martin Dvořák]

Sorry, I am ahead of time.

[Patrick Massot]

There is nothing to be sorry about, I'm only telling you that you should not loose hope

[Martin Dvořák]

Is there a way to force Visual Studio Code to display parentheses in the "tactic state" window?
Expressions like ¬ P ↔ P = false are extremely confusing for me.

[Eric Wieser]

Are you aware you can hover over the expression to see where the parentheses are?

[Martin Dvořák]

WoW, thank you! I had no idea!

[Damiano Testa]

There is probably a more stable approach to this, but my strategy is to hover with my mouse over the various parts in the Infoview to obtain the information that I need.

In this specific case, if you hover over ¬, you will see that ¬ P highlights: this means that they go together.
If you hover over =, you will see that P = false highlights, so those also go together.
Finally, if you hover over ↔ everything highlights.

In conclusion, these are the parentheses:

(¬ P) ↔ (P = false)

[Martin Dvořák]

Yeah! Thanks a lot! This is actually very clever!

[Damiano Testa]

Sometimes it can be tricky to get the mouse to hover over the right part, but it tends to work well most of the times!

[Martin Dvořák]

What was the design decision behind assigning such a low priority to \neg ? I think that mathematicians are used to \neg having a higher priority than all other logical operators.

[Yaël Dillies]

Are you sure? I would read -a^b as -(a^b), not (-a)^b.

[Anne Baanen]

Yaël, \neg is logical negation ¬ not unary minus -

[Mario Carneiro]

Also, in this example ¬ has a high priority, not a low one

[Yaël Dillies]

Oh oops

[Mario Carneiro]

If ¬ had a low priority it would be parsed ¬ (P ↔ P = false)

[Martin Dvořák]

Oh. You are right. I was wrong.

[Anne Baanen]

Apparently the lecture notes I learned mathematical logic from, wrote ¬ϕ ↔ (ϕ → ⊥), so this level of priority is not unusual to every mathematician :)

[Patrick Massot]

I thought the definition of "mathematician" included "not having attended any course in mathematical logic". :speak_no_evil:

[Anne Baanen]

I thought specifying mathematical logic would still allow me into the cool kids' club :P

[Martin Dvořák]

Is there any shortcut for this?
intro foo, exact foo,

I use it very often!

[Yakov Pechersky]

exact id?

[Yakov Pechersky]

or exact fun x, x

[Martin Dvořák]

Wow, thanks! This is great!

[Yakov Pechersky]

The reals, as currently defined in mathlib, are not computable. So #eval doesn't work on them. What would you want the output of #eval real.cos 2 to look like?

[Yakov Pechersky]

You can do this though:

#simp real.cos real.pi -- -1
#simp real.cos (2 * real.pi) -- 1

[Taylor Belcher]

Yakov Pechersky said:

You can do this though:

#simp real.cos real.pi -- -1
#simp real.cos (2 * real.pi) -- 1

Thank you!!!

[Martin Dvořák]

I understand that false is a type. However, is true also a type? Does something like true exist in Lean?

[Eric Wieser]

docs#true

[Eric Wieser]

(note that you can send "Welcome bot" PM's with docs# links to try them out, which is often faster than searching the docs if your guesses are good)

[Kevin Buzzard]

I usually send those PMs to rss-bot

[Kalle Kytölä]

I tried and nothing special happened. Only then I understood that Eric meant that the message contains a link that I can click. (For the record, my guess was not sufficiently good for the link to exist).

But I noticed that I can equally well send the private message to myself. :privacy: How good is that? :laughter_tears:

[Kyle Miller]

Does sending a PM solve something that the Preview button doesn't? If I'm guessing a docs link, I usually click that.

image.png

[Johan Commelin]

You can even send PMs to yourself (-;