I'd like to start from the bottom

Stream: general

[Daniel James]

Hi I'm currently a college freshman and as such I'm pretty sure everything being discussed in my math classes is already in mathlib. I thought it might be fun to start from nothing and just see how far I can get. I was wondering if anyone had advice on the practical logistics of this.

Is it feasible to not even link mathlib?
I think trying to write tactics myself would be a bridge too far. Are those in mathlib or built into Lean itself?
I saw that natural numbers are special cased in the compiler. Is that going to be a problem if I'm trying to write my own nat type?

If anyone has advice for the minimal reasonable base to start from it would be appreciated. Thanks!

[Mario Carneiro]

Yes you can work without mathlib. If you want to start from nothing at all you would need to set prelude and start from there, and this is not really recommended

[Mario Carneiro]

A simpler option is to just open a new namespace and make your own version of all the types

[Shreyas Srinivas]

I would suggest setting up lean from the vscode extension and starting with one of the books. You can add your own Nat type inside a namespace.

[Shreyas Srinivas]

The mathematics in lean book might be more to your liking.

[Daniel James]

I was definitely planning on working through the books before starting this.

[Daniel James]

Mario Carneiro said:

Yes you can work without mathlib. If you want to start from nothing at all you would need to set prelude and start from there, and this is not really recommended

What's in the prelude and what is the problem with not including it?

[Mario Carneiro]

Note that the Natural Number Game is specifically designed for this application: make your own natural numbers and prove all the basic theorems about them

[Daniel James]

Yeah that was what inspired it. I really enjoyed the natural number game and I want to go further.

[Mario Carneiro]

You can take a look at https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean to see what the "first file" looks like

[Mario Carneiro]

one of the biggest issues is that notation doesn't work yet so you have to write things like Eq a b instead of a = b

[Daniel James]

Ok cool. I see what sort of stuff that is. Sounds like using the prelude and just redefining all the types would be the best option

[Daniel James]

I could probably replace it later if I got really good at Lean

[Mario Carneiro]

Another problem is that if you don't define things exactly the way the prelude does, some tactics may fail because they have expectations about these definitions (like their name and type) which may not work on your types

[Nir Paz]

Also equality itself (not just the notation) is defined in the prelude, and I don't think you can really do things that basic without decent knowledge of lean to begin with

[Mario Carneiro]

You will notice that inductive is used a lot, this is where all the types come from, ultimately

[Mario Carneiro]

(or structure / class which are additional syntax on top of inductive)

[Daniel James]

I love seeing that things like this are just part of the library https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L263

[Jireh Loreaux]

Daniel, of course this is feasible, but I don't recommend it for learning. You will spend most of your time doing one of the following:

1. proving tons of absolutely trivial lemmas, so that the nontrivial lemmas are not so cumbersome to prove
2. proving nontrivial lemmas in long and complicated ways, often repeating arguments because you didn't split out all the little lemmas.

I would encourage what Mario suggested above. For any given topic (e.g., groups), import Mathlib up to, but not including, that topic, and then develop that topic from scratch.

[Daniel James]

Well I feel like part of the problem is that I haven't really done much complex math yet. (e.g. no groups)

[Jireh Loreaux]

What math are you familiar with?

[Daniel James]

I'm currently doing linear algebra and multi variable calculus

[Mario Carneiro]

I recommend reading #tpil to understand lean from the bottom (especially chapters 2, 3, 4, 7, 8)

[Yaël Dillies]

Multivariable calculus is certainly quite complex!

[Daniel James]

True. I more meant I haven't done any proof based courses yet. So there isn't as much opportunity to take results I've seen in class and write them in Lean.

[Daniel James]

Of course I can still do theorems that they state but don't prove

[Daniel James]

Mario Carneiro said:

I recommend reading #tpil to understand lean from the bottom (especially chapters 2, 3, 4, 7, 8)

I was definitely planning to read through/do the exercises from the book

[Kevin Buzzard]

If you start from the bottom then to do multivariable calculus you'll have to make the real numbers and it's probably not unreasonable to suggest that this will take many months.

[Daniel James]

Kevin Buzzard said:

If you start from the bottom then to do multivariable calculus you'll have to make the real numbers and it's probably not unreasonable to suggest that this will take many months.

I don't have any real expectations about how far I'd get. I just wanted to try and see what I can get done.

[Kevin Buzzard]

I once tried it and got as far as making the rationals and showing they're a field, but I got exhausted checking the order axioms. So nowhere near the reals really.

[Daniel James]

Haha ok. Well I won’t expect to get to far.