Michael Shaw

Stream: new members

[Michael Shaw]

Hi! I'm a High School Junior preparing to transition into senior year. I acknowledge I'm extremely out of my depth here and I have a lot to do before I can hope to succeed. I was first hazed into Lean from an article a smarter peer sent me (https://apurvanakade.github.io/courses/lean_at_MC2020/index.html) which I didnt understand at the time before the name resurfaced as a possible internship/guided study over the summer by a local college professor (who has worked in this area in the past). My main goal this summer is to get a basic grasp of the syntax and possibly write a solution to an IMO problem.

In terms of my understanding, I have completed most of the natural numbers game with only a few major challenges/topics of confusion. I hope I will be able to eventually contribute or at least develop my own understanding.

[Kevin Buzzard]

I recommend that you choose an IMO problem and just get going on it, and ask a bunch of questions in #new members (even getting started might be difficult, but we all have to start somewhere)

[Johan Commelin]

Also, it's probably best to avoid the geometry problems for now. You need a good grasp of mathlib to be able to even state those. Inequalities / number theory should be easier to get started with.

[Kevin Buzzard]

@Michael Shaw if you want to start on something easier than IMO problems, Stan Polu, David Renshaw and Kunhao Zheng have collected a bunch of more straightforward mathematical Lean puzzles in their miniF2F repo. This is not a straight Lean repo, it contains problems in a variety of theorem provers, so it has to be installed slightly differently to a standard Lean repo. Here's how to do it (on the command line, assuming a working leanproject environment):

git clone git@github.com:openai/miniF2F.git
cd miniF2F/lean/
leanproject get-mathlib-cache

and now you can fire up VS Code (e.g. by typing code . on the command line or opening VS Code and then using "open folder" and opening miniF2F/lean) and then in the src/test directory there are a ton of questions you can try.

[Michael Shaw]

Thank you! I'll start with reviewing the syntax from the Lean introduction pdfs before going with miniF2F repo and then looking at inequality/number theory problems. I appreciate the support!

I also just registered for codewars and am taking a look at how the system works, if there are any simple ones to work off of I would love a link or name!

[Kevin Buzzard]

oh codewars is another good way to get started, except that you shouldn't ask for spoilers here or online in general. I'm sure Stan won't mind you asking for spoilers for his F2F questions, as long as his AI's aren't using google to look for answers :-)

[Michael Shaw]

alright! I wasn't looking for answers, just some of the simpler kata to start off.

[Julian Berman]

If you care for another newbie's opinion I tried the codewars stuff and I found it a bit difficult to use to learn Lean

[Julian Berman]

It's not necessarily "on-ramp"-y, you kind of can refresh or browse the list of questions but some I found personally quite hard without some guidance... I find Kevin's material to be a lot easier of a way for me to actually internalize lean because they're written sequentially, so you might want to try https://github.com/ImperialCollegeLondon/formalising-mathematics at some point too

[Michael Shaw]

oh ok! I think i'll look through that first and the documents. personally I'm just trying to come up with simple axioms that can be proven easily and trying to conceptualize how proofing works. also need some more practice with the syntax. im not sure how close the syntax used in natural number game is to the one in the compiler.

[Kevin Buzzard]

How proofing works is what we're all about here.

[Michael Shaw]

thats true.

I just came up with a simple problem for myself to play around with similar in style to the natural number game. probably too simple but I dont know. basically i was watching a show and the characters wanted to buy a ticket for each of them by pooling their money. however, I noticed that their cash individually was less than the individual ticket price. so basically that gave me the idea to prove the simple idea if A<=T B<=T prove A+B<=2T. obviously this is just a simple problem that has been proved before but i want to try solving it just to have an opportunity to practice writing and using the syntax.

[Mario Carneiro]

do you know how to state it?

[Michael Shaw]

I think it is - lemma [some name for the theorem] (a b t : mynat) : a ≤ t ∧ b ≤ t → a + b ≤ 2t :=

[Scott Morrison]

Almost: you can't just write 2t.

[Michael Shaw]

that is true, noobie mistake. i think i should write t+t then?

[Scott Morrison]

Also, generally we write lemmas with multiple hypotheses as a ≤ t → b ≤ t → a + b ≤ 2t rather than using ∧. It's the same, but easier to work with.

[Scott Morrison]

Presumably you have multiplication defined on mynat, so hopefully you can write 2 * t.

[Michael Shaw]

ohhh i see that makes sense. i think the first step to solving this would be to break it down into two separate hypotheses. I'm mostly working off the basic lean tactics I remember from natural number game so I still need to do some research. Going to go study for my AP exams though, I appreciate all the support you guys are offering!

[Hanting Zhang]

: o
Oh this is cool. Did you attend MC20? @Apurva Nakade is also around working on surreal numbers I believe.

[Michael Shaw]

I didn't. I received the article from a friend under the context that we were both super into math. That being said I'm pretty average at math compared to them. I looked at the article then forgot about it due to a lack of understanding of the syntax and overall ideas only to be drawn back in as a research project and through the natural number game. Now that I finally understand the syntax and purpose of lean I can really get into the page.

[Hanting Zhang]

Ah, my bad.

[Michael Shaw]

you're fine!

[Hanting Zhang]

When I started I proved some "easy" things about the Fibonacci sequence, which wasn't actually easy and learned a lot from that. You could try doing some too if you think it could be a good starting point

[Michael Shaw]

that makes sense! Right now I'm just thinking about math wherever it comes up and then working on it. I think I'll do most of the heavy work over the summer since I have finals soon.

[Hanting Zhang]

And bonus points because if you want to try you also get to experience the PR process for mathlib, which is kind of daunting but isn't that bad once you do it once

[Hanting Zhang]

Yeah take whatever's comfortable for you! I'm definitely feeling the finals as well

[Michael Shaw]

Just took a look and that is a pretty impressive task. Its like they say: starting is the hard part. I feel like it'll be exciting once I take the first step.

[Michael Shaw]

Right now I think my main obstacle is my weak math base since I'm still working through high school level math so that makes understanding the concepts a bit difficult.

[Michael Shaw]

I'm just messing around right now, making up simple lemmas to solve through. I already followed all the install steps and have VS Code with my first project. How do I find the list of theorems available? I'm not sure if the natural number game uses the same theorems as the library.

[Julian Berman]

Some theorems are in what's called Lean core, which is what ships with Lean itself, and more are in mathlib, which is the meat of Lean's math library, and there are a lot of them :).

Usually vscode's autocomplete is one way to find them.

You'll definitely find some old friend theorems from NNG -- e.g. if you put in a file #check nat.add_assoc you'll see that theorem (it's defined in Lean core for natural numbers)

[Julian Berman]

(Or if you type nat.mul_ and just wait there you should see a bunch of theorems come up that you can browse through about multiplication)

[Michael Shaw]

Oh I missed this message for some reason. Thank you very much for this information! So just to be clear there is no drop down library similar to the style implemented with the NNG but rather mostly reliant on autocomplete?

[Mario Carneiro]

A drop down library like NNG for mathlib would be huge, there are tens of thousands of theorems to choose from

[Mario Carneiro]

autocomplete narrows it down by name / topic

[Mario Carneiro]

You can also use the search bar in the docs (see e.g. docs#nat.mul_assoc)

[Scott Morrison]

Using the search tool in mathlib, using regular expressions, is perhaps the most powerful theorem-finding tool, but it does rely on you learning how names are assigned in mathlib, which is a nontrivial undertaking!

[Michael Shaw]

oh that makes sense! I have seen the page in github on naming conventions (because i have the ambitious goal of making a PR on an IMO problem which personally is pretty daunting at a high school level especial given my average performance in math). regular expressions is another topic of research parallel to lean in terms of my work this summer so given time I might invest some work into that area.

I appreciate all the dedication and patience you guys are expressing because I am not the easiest student.

[Michael Shaw]

I'm not sure whether I should start a new topic or if I'm counting my eggs before they are hatched but how do I check if the IMO problem I plan to formalize has already been completed. is the mathlib IMO folder up to date? https://github.com/leanprover-community/mathlib/tree/master/archive/imo

I'll ask for guidance once I make some headway and PR process if I can get anywhere with it.

[Mario Carneiro]

The only reason the master branch would not be up to date is if there are any PRs in the works, so you should double check the PR list to make sure your theorem isn't waiting for review. But I don't think there have been any IMO PRs in a while

[Scott Morrison]

(Also, when I said to use regular expressions, really all I meant is that if you are hoping that both XXX and YYY appear in a theorem name, you can search for XXX.*YYY which just means XXX, then an arbitrary string of characters, then YYY. More complicated regular expressions are only rarely helpful. :-)

[Michael Shaw]

I understand. From what I can tell, the theorem naming conventions are mostly the same as NNG except that the theorems have a prefix corresponding to the type of variable/constant you are working with such as int.add/mult/etc vs nat.add/mult/etc

[Bryan Gin-ge Chen]

Perhaps you've already seen this, but there's some more detail on mathlib's naming conventions here: #naming

[Michael Shaw]

Thank you for letting me know!

[Kunhao Zheng]

I'm very happy to see that you've been interested in miniF2F @Michael Shaw ! Now you can directly open the folder miniF2F instead of miniF2F/lean through VS Code.

We've just added some more statements in AMC 12A/B level. These are very good exercises to step into lean after you've finished the tutorials. Also, if you are stuck on some of them, looking at the other proofs might help: we've got some proofs found by GPT-f, like this one induction_ineq_nsqlefactn. Hope you can enjoy it! And don't hesitate to open a pr if you solve any of them that doesn't have proof.

[Jiekai]

theorem induction_ineq_nsqlefactn
  (n : ℕ)
  (h₀ : 4 ≤ n) :
  n^2 ≤ n! :=
begin
  induction n with d hn, -- cursor here
  {

  },
end

2 goals
case nat.zero
h₀ : 4 ≤ 0
⊢ 0 ^ 2 ≤ 0!

case nat.succ
d : ℕ,
hn : 4 ≤ d → d ^ 2 ≤ d!,
h₀ : 4 ≤ d.succ
⊢ d.succ ^ 2 ≤ (d.succ)!

I'm trying this one and I'm confused about the first goal. :thinking:

[Johan Commelin]

@Jiekai Doe you have something like pow_two that you can rw with?

[Jiekai]

Something like simp only [sq] in the original proof?

[Jiekai]

I'm confused about the 4 ≤ 0 part. If a goal has false condition (Should I call the h₀ part condition?), does that mean the goal is true?

[Johan Commelin]

Ooh, I had not even looked at your assumptions yet. But sure, false.elim can prove anything, given a proof of false.

[Jiekai]

I think I'm doing this induction wrong :fear:

[Johan Commelin]

Yes, this way it will be somewhat painful to deal with the cases n = 2 and n = 3.

[Johan Commelin]

Maybe you don't even want to use induction...

[Jiekai]

proposition a:
4^2 <= 4! [proof by computing]

proposition b:
if n^2 <= n! and n >= 4
then (n+1)^2 <= (n+1)!  [proof omitted]

Combine proofs of prop a and prop b as the final proof.
I would like to translate the this to lean. Any hints please

[Jiekai]

Johan Commelin said:

Ooh, I had not even looked at your assumptions yet. But sure, false.elim can prove anything, given a proof of false.

I vaguely remember something relevant is in NNG.

[Johan Commelin]

I think there is a lemma docs#nat.exists_eq_add_of_le

[Johan Commelin]

You can use that to turn your statement about n into a statement about m+4.

[Johan Commelin]

After that, use induction on m.

[Jiekai]

Thanks! Let me try that.

[Johan Commelin]

But you can also prove that $(n+2)(n+3) \ge 2(n+3) \ge n+4$. (Instead of that prop b).

[Kritixi Lithos]

Jiekai try something like the following. There should also be a way with cases' or match instead of the if-statement, but I couldn't get it working anyways
if h₁:4 ≤ n then begin sorry end else by apply false.elim (h₁ h₀)

wait never mind this runs into the same problem again with the induction

[Jiekai]

Johan Commelin said:

I think there is a lemma docs#nat.exists_eq_add_of_le

theorem induction_ineq_nsqlefactn
  (n : ℕ)
  (h₀ : 4 ≤ n) :
  n^2 ≤ n! :=
begin
   have t0: nat.exists_eq_add_of_le h₀,
end

  invalid type ascription, term has type
    ∃ (k : ℕ), n = 4 + k : Prop
  but is expected to have type
    Sort ? : Type ?

Why the type error?

[Jiekai]

The tutorials seem to have few induction exercises. This puzzle seems nice to include.

[Johan Commelin]

@Jiekai Write have t0 :=. You need := instead of :.

[Jiekai]

then how should I handlet0 : ∃ (k : ℕ), n = 4 + k into

k : ℕ
n = 4 + k

[Johan Commelin]

@Jiekai tactic#cases or tactic#obtain.