getting started

Stream: new members

[Brandon Wu]

hi there! i am very new to this, and i was having some difficulty with the installation / the overall setup of lean. right now i'm trying to use it in vscode with the extension, but I'm unsure as to exactly how lean operates - do I simply make a new file with some specified extension or is it more involved?

[Kevin Buzzard]

You make a new project, as we desperately try to flag several times in the installation instructions

[Kevin Buzzard]

or you clone the tutorial project

[Brandon Wu]

my setup currently lives on my school's unix servers, so i sometimes run into trouble installing things - most recently ive been running into an error "/tmp/tmp.p0mYwop9QR/elan-init: /lib64/libc.so.6: version `GLIBC_2.18' not found (required by /tmp/tmp.p0mYwop9QR/elan-init)" when trying to install elan

[Patrick Massot]

That's a very bad omen.

[Patrick Massot]

What kind of Unix is that?

[Reid Barton]

sounds like one which is no longer as young as it once was

[Reid Barton]

"school's unix servers" is likely to be RHEL [some appallingly low number]

[Brandon Wu]

If it's relevant, I go to Carnegie Mellon and this is my school's Andrew server that I typically do all my work from. Is there no hope other than managing things locally, then?

[Reid Barton]

Well, if you already have the required build tools (cmake for Lean, the rust toolchain for elan) then it should be pretty easy to build your own binaries.

[Reid Barton]

Though I've never tried building elan

[Filippo A. E. Nuccio]

Hi all, I am a number theorist and I have recently discovered some of Kevin Buzzard's talks. I have downloaded Lean, played with the natural number game and done some of Patrick Massot's exercises... I wonder where to go now to learn/play/do stuff. For instance, how could I check if basic results about group theory are there (e.g. : finite group of order p^2 is abelian, or "quotient by the centre is cyclic==> group is abelian), or how/where can I try to prove them? Many thanks!

[Jalex Stark]

doing exercises on codewars is a nice way to learn things

[Jalex Stark]

you can answer some of your questions by navigating in mathlib to the group_theory folder

[Jalex Stark]

either by using the html docs or in your own VSCode project by going to the "target" folder

[Jalex Stark]

i guess you can also read the code on github directly

[Johan Commelin]

@Filippo A. E. Nuccio Welcome! Do you have a working Lean setup on your own computer?

[Filippo A. E. Nuccio]

Yes, I do. And thanks for the welcome.

[Johan Commelin]

Once you want to do something serious, the online web editors no longer are good enough

[Johan Commelin]

Ok, great

[Filippo A. E. Nuccio]

Jalex Stark said:

i guess you can also read the code on github directly

Thanks! I will try doing so, then. I have also tried to read a bit about "compatibility" with future/past version. Is it true that whatever we're doing in Lean 3 now will need to be redone from scratch in Lean 4?

[Johan Commelin]

In that case, I would follow the instructions for setting up a new project, add mathlib as dependency, and try to state some of your group theory lemmas

[Johan Commelin]

I don't think we'll have to redo things from scratch. But there will be some weeks where we have to solve a lot of technical porting issues.

[Johan Commelin]

Luckily we have some very good regex hackers in our community.

[Mario Carneiro]

Also I think the day is fast approaching that we get enough parser data from lean core to be able to do better than regex

[Filippo A. E. Nuccio]

Ah ok, good news. I' ll try to set up a new project, although I have not found a documentation about "basics" of group theory (e.g. what's the name for its order?) I suspect it should be at the address suggested by Jalex Stark

[Filippo A. E. Nuccio]

Thanks to both of you for your answers, I'll try my luck!

[Johan Commelin]

@Filippo A. E. Nuccio We just reuse card for the order. Note that you need to add [fintype G] to assume that your group is finite. And then fintype.card G gives you the order of the group.

[Johan Commelin]

If you have any arbitrary group... you need to deal with cardinals :sad:

[Filippo A. E. Nuccio]

@Johan Commelin Thanks! This is precisely the kind of info I'd love to see written somewhere: where should I look exactly, rather than asking everything here? I feel a huge leap between solving Patrick's exercices and opening my project from scartch

[Filippo A. E. Nuccio]

(it reminds me of the first time I tried to type a LaTeX document before discovering the Short Guide To LaTeX...)

[Jalex Stark]

asking here is not super expensive, and learning from answers here will give you intuitions on where to look

[Jalex Stark]

if you feel bad about using people's time, just commit to start answering questions once you know things :)

[Filippo A. E. Nuccio]

Indeed, that was my problem. I feel a bit bad in asking stupid things like: where do I start from? As far as I know I should:
1) Create a new project, and import mathlib (this is OK)
2) Import "all" things which I suspect I might need to speak about finite groups: here I am already puzzled
3) Learn something about types/classes/structures...: no idea at all.

[Jalex Stark]

For your 3), I find myself skimming chapter 10 of TPiL every couple of weeks and understanding more of it in proportion to how much engineering I've done between readings

[Bryan Gin-ge Chen]

There isn't a great solution right now for 2), but see the very recent in-progress "mathematics in Lean" book: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20Lean.20.2F.20mathlib.20tutorial

For 3), the standard source / reference for Lean is still "Theorem proving in Lean": https://leanprover.github.io/theorem_proving_in_lean/

[Filippo A. E. Nuccio]

@Bryan Gin-ge Chen Thanks!

[Bryan Gin-ge Chen]

(TPiL is short for "Theorem Proving in Lean" around here, so my suggestion was essentially the same as Jalex's.)

[Filippo A. E. Nuccio]

Another stupid question: is it normal that each time I create a new project, some 120 MB get downloaded? I played a bit creating projects and I realise I have used almost a GB for nothing. Not a big deal, per se, just seems a bit odd.

[Bryan Gin-ge Chen]

Yes, unfortunately. Most of that space is taken up by mathlib's .olean files, which are like the compiled version of the .lean files.

[Nam]

i'll add that Hitchhiker's Guide explains stuffs pretty well.

[Bryan Gin-ge Chen]

Yes, I like that book too. You can find it with the other course materials here: https://lean-forward.github.io/logical-verification/2020/index.html#material

[Kevin Buzzard]

@Filippo A. E. Nuccio here is some basic group theory being done in Lean: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/group/level01_extended.lean

[Filippo A. E. Nuccio]

@Nam @Bryan Gin-ge Chen Ok, thanks. I'll have a look there.

[Filippo A. E. Nuccio]

@Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

[Patrick Massot]

Filippo A. E. Nuccio said:

Thanks! This is precisely the kind of info I'd love to see written somewhere: where should I look exactly, rather than asking everything here? I feel a huge leap between solving Patrick's exercices and opening my project from scartch

Maybe I should give more context in the tutorials README (I gave it here, but it's not on GitHub). Currently there is a steady stream of people who want to learn Lean for math. This is great but the self-teaching material that exists is not yet up to this task. As a kind of urgency plaster, I translated the exercises from my first year undergraduate course where I used Lean, simply adding a couple of tactics that allow more efficiency. The course was not about learning Lean, it was about learning how to write rigorous proofs. So it stops very far from the point where you can develop new maths in Lean, and it very carefully avoid painful points, like handling inclusion maps. I simply hoped it would keep people busy for some time, and teach useful stuff while we work on https://github.com/leanprover-community/mathematics_in_lean that should ultimately contain much more.

[Kevin Buzzard]

Filippo A. E. Nuccio said:

Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

The file I linked to imports other files from that project, so yes you'd be better off downloading the entire project. But nowadays I usually work within a local copy of mathlib.

[Patrick Massot]

Filippo A. E. Nuccio said:

Another stupid question: is it normal that each time I create a new project, some 120 MB get downloaded? I played a bit creating projects and I realise I have used almost a GB for nothing. Not a big deal, per se, just seems a bit odd.

This is not a stupid question at all. Each time you create a new project, you download mathlib, with its full git history. That's about 37Mo. Then, if you don't already have them, you download compiled mathlib files. After unpacking, this adds about 80 Mo. If you already have those compiled files they are not downloaded but they are copied to your new project folder, which now weights about 120 Mo. This makes sense when you have a couple of projects that depend on different versions of mathlib, that you want to update independently (mathlib moves really fast, and a mathlib update can break your project non-trivially). But it doesn't make sense if you simply want to play with creating Lean projects. There are ways to improve on this, but limited time resources to modify leanproject. The current workflow works nicely for serious users who have a handful of projects that need to be really independent, and for people who want to play with one toy project. So improving this is very low priority. But feel free to contribute if fixing this is important to you. This is much much easier than proving things.

[Patrick Stevens]

I'll try and address the git cloning thing in https://github.com/leanprover-community/mathlib-tools/pull/47 - it's a first draft but I am going to eat now

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Filippo A. E. Nuccio said:

Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

The file I linked to imports other files from that project, so yes you'd be better off downloading the entire project. But nowadays I usually work within a local copy of mathlib.

Thanks!

[Jalex Stark]

people on this thread may like reading this community wiki page

[Filippo A. E. Nuccio]

Patrick Massot said:

Filippo A. E. Nuccio said:

Another stupid question: is it normal that each time I create a new project, some 120 MB get downloaded? I played a bit creating projects and I realise I have used almost a GB for nothing. Not a big deal, per se, just seems a bit odd.

This is not a stupid question at all. Each time you create a new project, you download mathlib, with its full git history. That's about 37Mo. Then, if you don't already have them, you download compiled mathlib files. After unpacking, this adds about 80 Mo. If you already have those compiled files they are not downloaded but they are copied to your new project folder, which now weights about 120 Mo. This makes sense when you have a couple of projects that depend on different versions of mathlib, that you want to update independently (mathlib moves really fast, and a mathlib update can break your project non-trivially). But it doesn't make sense if you simply want to play with creating Lean projects. There are ways to improve on this, but limited time resources to modify leanproject. The current workflow works nicely for serious users who have a handful of projects that need to be really independent, and for people who want to play with one toy project. So improving this is very low priority. But feel free to contribute if fixing this is important to you. This is much much easier than proving things.

Thanks, this makes everything much clearer. I now really need to start making my hands dirty with some proof, but I'll be back to the forum as soon as I have more questions or comments. I think that this issue of dowloading 120 MB really not crucial for the time being.

[Patrick Massot]

I'll try and address the git cloning thing in https://github.com/leanprover-community/mathlib-tools/pull/47 - it's a first draft but I am going to eat now

@Patrick Stevens what is the current status of that effort? I'm about to release version 0.0.6

[Patrick Massot]

Note that there is no problem releasing 0.0.7 in a couple of days if you are not ready.

[Patrick Stevens]

Sorry, I kind of forgot about it and it has some test failures I haven't explained - let me just have a quick look again

[Patrick Stevens]

Part of the problem is that it's been literally years since I coded in Python, so everything is hard again :P

[Patrick Massot]

I should have asked a more specific question. I didn't look at that PR yet because it was flagged as a draft, do you want me to look at it now?

[Patrick Massot]

Also you should probably rebase on master before doing anything else on your branch

[Patrick Stevens]

The current status is "tests are failing when I enable the new mode and I have no idea why". I just turned my new flag to default to "off" and now the only test that is failing is the one that asserts the new behaviour - so it's definitely my change that is broken - but I was hoping to finish this without having to work out how to run it locally

[Patrick Stevens]

In hindsight, quite an optimistic hope

[Patrick Massot]

The error message on Travis suggests you invented some feature of git python

[Patrick Stevens]

(fear not, I'll squash away all these ridiculous commits)

[Patrick Massot]

And also that you didn't rebase on master

[Patrick Massot]

But this is not a problem at all

[Patrick Massot]

This can wait

[Patrick Massot]

I'll release 0.0.6 now

[Patrick Stevens]

Not rebasing isn't a problem if I'm going to squash-merge anyway, right?

[Patrick Stevens]

Sure, go for it

[Patrick Massot]

Oh sorry, I didn't see your new commits.

[Patrick Massot]

Yes, we can clean up history before merging

[Patrick Massot]

My actual question is: why do you think you can pass the depth argument to Repo.clone_from like this?

[Patrick Stevens]

Its docstring contains the text " :param multi_options: See clone method", and the clone method's docstring contains the text

   :param multi_options: A list of Clone options that can be provided multiple times.  One
        option per list item which is passed exactly as specified to clone.
        For example ['--config core.filemode=false', '--config core.ignorecase',
                     '--recurse-submodule=repo1_path', '--recurse-submodule=repo2_path'

[Patrick Stevens]

Do you mind if I add "/venv" to the .gitignore? I'm finally seeing if I can run the thing myself

[Patrick Massot]

Python 3.8.0 (default, Dec  7 2019, 17:45:02)
Type 'copyright', 'credits' or 'license' for more information
IPython 7.12.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: from git import Repo

In [2]:  Repo.clone_from('https://github.com/leanprover-community/tutorials.git'
   ...: , 'test_target', ['--depth=1'])
---------------------------------------------------------------------------
AttributeError                            Traceback (most recent call last)
<ipython-input-2-e474310ae324> in <module>
----> 1 Repo.clone_from('https://github.com/leanprover-community/tutorials.git', 'test_target', ['--depth=1'])

~/.pyenv/versions/3.8.0/lib/python3.8/site-packages/git/repo/base.py in clone_from(cls, url, to_path, progress, env, multi_options, **kwargs)
   1015         if env is not None:
   1016             git.update_environment(**env)
-> 1017         return cls._clone(git, url, to_path, GitCmdObjectDB, progress, multi_options, **kwargs)
   1018
   1019     def archive(self, ostream, treeish=None, prefix=None, **kwargs):

~/.pyenv/versions/3.8.0/lib/python3.8/site-packages/git/repo/base.py in _clone(cls, git, url, path, odb_default_type, progress, multi_options, **kwargs)
    952                          v=True, universal_newlines=True, **add_progress(kwargs, git, progress))
    953         if progress:
--> 954             handle_process_output(proc, None, progress.new_message_handler(), finalize_process, decode_streams=False)
    955         else:
    956             (stdout, stderr) = proc.communicate()

AttributeError: 'list' object has no attribute 'new_message_handler'

[Patrick Massot]

This has nothing to do with leanproject, this is simply not how Repo.clone_from works (at least the version I have here).

[Patrick Stevens]

Patrick Massot said:

This has nothing to do with leanproject, this is simply not how Repo.clone_from works (at least the version I have here).

Sure, I understand the message; I simply followed what I thought were clear and simple instructions from the docstring :P but nothing is clear and simple when you haven't touched a language for years

[Patrick Massot]

No problem. I'm very happy when people want to contribute to leanproject, and there is no hurry at all. I released anyway since there was a critical bug since the appearance of an unfortunately named branch in the mathlib repository

[Patrick Massot]

And now I need to leave

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

Kevin Buzzard said:

Filippo A. E. Nuccio said:

Kevin Buzzard
Thanks. So, if I undestand the philosophy right, I should download the project group-theory-game and play there? I also suppose I should rather create an internal folder (say, with my name/initials) to avoid that if everything gets updated on GIT my work disappears?

The file I linked to imports other files from that project, so yes you'd be better off downloading the entire project. But nowadays I usually work within a local copy of mathlib.

Thanks!

I am trying to play with the group_game, and I can prove something (for central elements, right and left cosets coincide) but I don't understand the definition of "central_subgroup". I am wondering what's the policy: is there a stream to discuss that project in particular, should I throw my question at everyone in the chat? And whom should I show my partial solution to see if it is correct, should I paste it here? Thanks

[Kevin Buzzard]

Oh I didn't even write the central subgroup stuff, that was written by @Jason KY. who is probably very busy with exams right now.

[Kevin Buzzard]

and I am very busy with marking them :-/

[Kevin Buzzard]

But one thing I would definitely recommend is that if you have any questions about this then please don't ask them in this generic thread, start a new topic with title the group theory game or something. You are more likely to get answers that way. Put it in #maths if you like.

[Kevin Buzzard]

Also, feel free to write your own questions and PR them (or just post working Lean code as "issues" if you don't have a clue about github). Both Jason and I are busy with other things right now but we should get back to this in June.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Oh I didn't even write the central subgroup stuff, that was written by Jason KY. who is probably very busy with exams right now.

Oh, thanks. Very clear, then. I'll do so and I will try to understand how to "PR" them.

[Jason KY.]

Hi, Filippo
I defined the center of a group G as the set of elements of G that commutes and then I defined it to be a subgroup by proving all the subgroup axioms.
To be honest, I'm not sure if this is a good way to define this myself, I still learning myself!

[Filippo A. E. Nuccio]

Jason KY. said:

Hi, Filippo
I defined the center of a group G as the set of elements of G that commutes and then I defined it to be a subgroup by proving all the subgroup axioms.
To be honest, I'm not sure if this is a good way to define this myself, I still learning myself!

I see; I have moved the discussion to maths/group theory game-> should we continue there?

[edderiofer]

I'm struggling with the Advanced Worlds; specifically, I'm trying to apply some theorem statements to existing hypotheses to get new hypotheses to work with, but I can't figure out the syntax.

[Patrick Massot]

#mwe?

[Jalex Stark]

Hey @edderiofer ! I guess you're playing the natural number game? if you search this chat you may find a lot of discussions relevant to your problems :)

[Jalex Stark]

If you have a more specific question, you can hit the "new topic" button, give it an appropriate title, and show us the code you're struggling with

[edderiofer]

For instance, in Advanced Multiplication World 4, I do the following:
induction c with d hd generalizing b, simp, intro h,
which is fine. Now I want to use eq_zero_or_eq_zero_of_mul_eq_zero to deduce from h that a = 0 ∨ b = 0, but I can't figure out the syntax for it; have g := mul_eq_zero_iff(h), throws an error.

[Jalex Stark]

We need code that compiles, so that we can run it locally and see the same things you're seeing

[Jalex Stark]

otherwise this is a big game of telephone where everybody loses

[Jalex Stark]

Did you read the error?

[edderiofer]

Yes, but I don't understand it.

[Jalex Stark]

The errors have lots of useful information in them

[Jalex Stark]

If you want help here, you'll have to produce a #mwe

[edderiofer]

On Advanced Multiplication World Level 4 of the Natural Number Game,
induction c with d hd generalizing b, simp, intro h, have g := mul_eq_zero_iff(h),
throws an error on the last line.

[Jalex Stark]

yes, I think you said all of that already

[edderiofer]

Then I'm not sure what you want from me.

[Jalex Stark]

you could either give us a #mwe or tell us what youre error message is, I think both of those would enable progress

[Jalex Stark]

(did you notice that #mwe is a link to a page with a description of what we want?)

[edderiofer]

I get the error:

type mismatch at application mul_eq_zero_iff h term h has type a * b = 0 : Prop but is expected to have type mynat : Type state: 2 goals a : mynat, ha : a ≠ 0, b : mynat, h : a * b = 0 ⊢ b = 0

case mynat.succ a : mynat, ha : a ≠ 0, d : mynat, hd : ∀ (b : mynat), a * b = a * d → b = d, b : mynat ⊢ a * b = a * succ d → b = succ d

[Jalex Stark]

mul_eq_zero_iff is a function of several arguments, the first of which is a nat

[Jalex Stark]

try mul_eq_zero_iff _ _ h

[edderiofer]

That gets me this error:

function expected at
  mul_eq_zero_iff ?m_1 ?m_2
term has type
  ?m_1 * ?m_2 = 0 ↔ ?m_1 = 0 ∨ ?m_2 = 0
state:
2 goals
a : mynat,
ha : a ≠ 0,
b : mynat,
h : a * b = 0
⊢ b = 0

case mynat.succ
a : mynat,
ha : a ≠ 0,
d : mynat,
hd : ∀ (b : mynat), a * b = a * d → b = d,
b : mynat
⊢ a * b = a * succ d → b = succ d

[Jalex Stark]

from this part of the error function expected at mul_eq_zero_iff ?m_1 ?m_2 you can see that it wants exactly two arguments

[Jalex Stark]

so try one fewer underscore

[edderiofer]

have g := mul_eq_zero_iff _ h, gets me this error:

type mismatch at application
  mul_eq_zero_iff ?m_1 h
term
  h
has type
  a * b = 0 : Prop
but is expected to have type
  mynat : Type
state:
2 goals
a : mynat,
ha : a ≠ 0,
b : mynat,
h : a * b = 0
⊢ b = 0

case mynat.succ
a : mynat,
ha : a ≠ 0,
d : mynat,
hd : ∀ (b : mynat), a * b = a * d → b = d,
b : mynat
⊢ a * b = a * succ d → b = succ d

[Jalex Stark]

What do you think this part of the error means?

term
  h
has type
  a * b = 0 : Prop
but is expected to have type
  mynat : Type

[edderiofer]

That I need a second mynat as the second input.

[edderiofer]

have g := mul_eq_zero_iff _ _, compiles, but gives me this set of goals:

4 goals
a : mynat,
ha : a ≠ 0,
b : mynat,
h : a * b = 0,
g : ?m_1 * ?m_2 = 0 ↔ ?m_1 = 0 ∨ ?m_2 = 0
⊢ b = 0

a : mynat,
ha : a ≠ 0,
b : mynat,
h : a * b = 0
⊢ mynat

a : mynat,
ha : a ≠ 0,
b : mynat,
h : a * b = 0
⊢ mynat

case mynat.succ
a : mynat,
ha : a ≠ 0,
d : mynat,
hd : ∀ (b : mynat), a * b = a * d → b = d,
b : mynat
⊢ a * b = a * succ d → b = succ d

which isn't what I wanted.

[Jalex Stark]

right, I think you should figure out which specific mynats to fill in the underscores with

[Jalex Stark]

(it's probably a and b in some order)

[Patrick Massot]

Jalex, you're not helping by keeping answering without a #mwe

[Patrick Massot]

You know that, in the long run, you're not helping him or her.

[Jalex Stark]

I could stop replying, yeah; I guess my fear is that they'll give up on the natural number game

[Jalex Stark]

really my goal is to try to understand why people don't respond gracefully to requests for a #mwe

[Jalex Stark]

i don't have a very good model of what's going on in their head

[Jalex Stark]

but also like, I think it is interesting to have discussions with new people about how to read error messages

[Jalex Stark]

maybe we need a natural number game stream to insulate the rest of the server from specificall this sort of interaction

[edderiofer]

In my case, I'm not sure how the description I gave:

On Advanced Multiplication World Level 4 of the Natural Number Game,
induction c with d hd generalizing b, simp, intro h, have g := mul_eq_zero_iff(h),
throws an error on the last line.

doesn't constitute a MWE (or in this case, a MN-WE).

[Jalex Stark]

did you read the definition at the link?

[Jalex Stark]

for us, a #mwe is something that we can copy-paste into a local Lean instance

[edderiofer]

OK, but how do I get the list of imports if I'm playing the Natural Number Game?

[Jalex Stark]

(and yeah, "working" is a strange word, for us it means "throws the error that i'm interested in getting help with")

[Jalex Stark]

you could start by including the theorem statement

[Jalex Stark]

I can add some guidance to that link about the natural number game

[edderiofer]

That would definitely be helpful.

[Jalex Stark]

okay so what happens if you try to post the theorem statement and your proof script?

[Jalex Stark]

I think it's ~40% likely that if I copy it into my local instance, it will just work, since a lot of the natural number definitions are in core

[ROCKY KAMEN-RUBIO]

@edderiofer When we say an MWE (Minimum Working Example), we mean something we can copy and paste directly into a local Lean compiler and get the same result. It may not be obvious how to do this if Natural Number Game has been your only exposure to lean. For example, the following does not work because it's just a series of tactics.

induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff(h),

This does count, because I've included the theorem statement and imports (notice that I'm using nat instead of mynat, which is specific to NNG).

import data.nat.basic
theorem mul_left_cancel (a b c : nat) (ha : a ≠ 0) : a * b = a * c → b = c :=
begin
induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff(h),
end

[Jalex Stark]

@ROCKY KAMEN-RUBIO you're missing import tactic

[ROCKY KAMEN-RUBIO]

Thanks!

[Patrick Massot]

The case of the NNG is the easiest actually: you can copy-paste the url, eg http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=7&level=1

[edderiofer]

The following works (on https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4):

theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c :=
begin
induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff a b,
rwa g at h,

but is there a quicker way to perform the last two lines to go from h : a * b = 0 to h : a = 0 ∨ b = 0?

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

ROCKY KAMEN-RUBIO you're missing import tactic

import data.nat.basic
import tactic
theorem mul_left_cancel (a b c : nat) (ha : a ≠ 0) : a * b = a * c → b = c :=
begin
induction c with d hd generalizing b,
simp,
intro h,
have g := mul_eq_zero_iff(h),
end

[Patrick Massot]

Jalex, I think it would be good idea to mention this url "trick" in the #mwe webpage

[Jalex Stark]

you could do rwa mul_eq_zero_iff a b at h,

[Jalex Stark]

and then in fact if you replace the a and b with underscores it should figure it out for you

[edderiofer]

Ah, OK.

[Jalex Stark]

thanks for the patience here, we really want to help new people and avoid burnout, so we want to make processes to make helping new people more efficient

[edderiofer]

What if the theorem I wanted to use was a single-direction implication? You can't use rw then, can you?

[Jalex Stark]

then you want apply

[Jalex Stark]

well, apply f works if f : A \to B and B is the goal

[ROCKY KAMEN-RUBIO]

@edderiofer This might seem like a silly distinction, but getting in the habit of doing this really does speed up the process of assessing errors when your questions get more complex. It's totally understandable if you're confused this early on. Keep at it, and keep asking questions if you get stuck!

[Jalex Stark]

sometimes I do find myself using a lemma to generate an equality and then rwing that equality

[Patrick Massot]

I don't know what is explained in the game at this point, but the normal way to write this beginning of proof would be:

induction c with d hd generalizing b,
simp,
intro h,
cases (mul_eq_zero_iff a b).mp h with ha' hb,

or, even better,

induction c with d hd generalizing b,
simp,
intro h,
exact or.resolve_left ((mul_eq_zero_iff a b).mp h) ha,

[Jalex Stark]

where "normal" means "mathlib-approved"?

[Patrick Massot]

efficiency approved

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

sometimes I do find myself using a lemma to generate an equality and then rwing that equality

Technically I think NNG doesn't let you define external lemmas outside of the current tactic proof, so you would have to use a have statement or something.

[edderiofer]

I don't think .mp is explained in the game at this point?

[Jalex Stark]

yes when i said "lemma" I did mean "add somethign new to the local context with have" not "define something with the lemma keyword"

[Patrick Massot]

I have no idea what is explained here. I'm too old. I started Lean long before this game was written

[Jalex Stark]

I agree that NNG does not want you to use .mp

[Jalex Stark]

I learned about .mp by using Lean in VSCode and having it pop out of suggest or library_search sometimes

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

yes when i said "lemma" I did mean "add somethign new to the local context with have" not "define something with the lemma keyword"

Cool, just wanted to make that distinction because of the keyword lemma.

[Jalex Stark]

Patrick, is adding a local hypothesis and using rw really much less efficient than the term mode proof?

[Jalex Stark]

I guess in my mind the only time to care about that much efficiency is if you're putting code into mathlib

[Jalex Stark]

but maybe I am wrong

[Patrick Massot]

I mostly meant efficiency in writing speed.

[Jalex Stark]

well that's definitely not true if I'm the one writing :P

[Patrick Massot]

I also have another constraint from my teaching use of Lean. The ultimate goal of my course is to teach traditional math writing. Lean is only an intermediate tool. Hence I prefer having only one line of Lean for one sentence on paper. Here you would say: ab = 0 and a neq 0 hence b=0, matching the number of lines of my efficient proof.

[Jalex Stark]

interesting

[Jalex Stark]

Kevin writes a lot of "literate lean" where he uses multiple lines of Lean for one line of math

[Patrick Massot]

But on that example, I would not expect my students to write this line, this is too advanced term mode.

[Jalex Stark]

ah okay

[Jalex Stark]

making the math proof move slower seems better than making the lean move faster, for the purpose of teaching first-years

[Jalex Stark]

I guess most people here (including @edderiofer) are coming form the perspective of already being fluent in "terse" mathematical sentences

[Jalex Stark]

I made a small edit to the #mwe page. @edderiofer do you think the current state of the page would have caused you to post a link?

[edderiofer]

If "Natural Number Game" were capitalized, definitely.

[Jalex Stark]

haha thanks, fixing that now

[Jalex Stark]

okay, I added a fairly explicit example to #mwe

[edderiofer]

Yep, that works.

[Jalex Stark]

edderiofer, I think i recognize your name from /r/math and /r/mathriddles ? Have you seen this pair of riddle and Codewars question?
and this other pair, where the translation was in the other direction?

[Mario Carneiro]

Regarding #mwe generation, it would be nice if NNG had a "MWE button" that takes the user's text together with the surrounding theorem and the imports and puts it in your clipboard. Since this has to be what is being sent to lean this should not be too difficult

[Mario Carneiro]

it's still not perfect because of the mynat issue, but it should be enough for the cognoscenti

[edderiofer]

No, I haven't seen either of those pairs, but yes, you probably do recognize me from there.

[Jalex Stark]

cool, I am khanh93 on reddit, though I post a lot less so you may not recognize me

[edderiofer]

Yep, definitely don't recognize that username.

[edderiofer]

So who's going to post the MWE button feature request to GitHub?

[Jalex Stark]

well I think the biggest problem is that we don't have anyone doing active development on the NNG engine :(

[Jalex Stark]

though I guess the github project is a great place to store these desiderata

[Jalex Stark]

I think this project is the relevant one
https://github.com/mpedramfar/Lean-game-maker

[Bryan Gin-ge Chen]

The person to ping is @Mohammad Pedramfar, I think. Unless he's said he's taking a step back from development.

[edderiofer]

I thought it was this one? https://github.com/ImperialCollegeLondon/natural_number_game

[Jalex Stark]

I think, though obviously mohammad is the best person to comment, that the latter project is for the content of the game levels and the former is for the engine

[edderiofer]

Ah, OK. Well, I'm still stuck on this level, so I think I'll just go off and make food now.

[Jalex Stark]

(I'm hoping "stuck" means "still trying to think of a new idea" and not "there was a question I asked that didn't receive any attention, because everyone was talking about the meta problem of how to phrase the question")

[edderiofer]

Still trying to think of a new idea.

[Mohammad Pedramfar]

Jalex Stark said:

well I think the biggest problem is that we don't have anyone doing active development on the NNG engine :(

The latest commit was 5 days ago! :(
Is there any issue with the game? Or do you want some extra features?

[edderiofer]

Hmm. If I could prove that a is the successor of some number, since it's nonzero, this would be a lot easier, I think?

[Jalex Stark]

Mohammad Pedramfar said:

Jalex Stark said:

well I think the biggest problem is that we don't have anyone doing active development on the NNG engine :(

The latest commit was 5 days ago! :(
Is there any issue with the game? Or do you want some extra features?

hah, sorry! I was not following closely enough. Now I remember that you recently made it so that progress is saved! I think the work you're doing is very valuable :)

[Jalex Stark]

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

[Jalex Stark]

edderiofer said:

Hmm. If I could prove that a is the successor of some number, since it's nonzero, this would be a lot easier, I think?

try cases a

[Jalex Stark]

Jalex Stark said:

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

so it would have the URL of the current level plus the current proof script, and I guess also the statement of the theorem so that people who don't click the link can follow the discussion

[edderiofer]

Oh, right, I misread what cases a does in this case.

[edderiofer]

Is there a quick way to comment out a line?

[Mario Carneiro]

-- comment

[Bryan Gin-ge Chen]

ctrl+/ (or cmd+/ if you're on macOS) should be the keybind for line comment.

[Jalex Stark]

that's in VSCode, I think in the NNG you just have to type the comment character

[Jalex Stark]

there's also block comments

/-
like this
-/

[Bryan Gin-ge Chen]

Jalex Stark said:

that's in VSCode, I think in the NNG you just have to type the comment character

Oh, you're right. For some reason I thought the web editors supported it too.

[Jalex Stark]

a lot of web editors have the same keybinding

[Jalex Stark]

I use cmd-/ in jupyter and overleaf

[edderiofer]

How do I flip an equality? If I have a * b = 0 as a hypothesis, how do I turn it into 0 = a * b?

[Jalex Stark]

symmetry at h

[edderiofer]

Thanks.

[Jalex Stark]

btw it's better for the server if we have new questions in new topics.

[Jalex Stark]

mostly so that people later can read old conversations

[edderiofer]

Ah, alright.

[Mohammad Pedramfar]

Mario Carneiro said:

Regarding #mwe generation, it would be nice if NNG had a "MWE button" that takes the user's text together with the surrounding theorem and the imports and puts it in your clipboard. Since this has to be what is being sent to lean this should not be too difficult

The things that are sent to the Lean server are not limited to what can be seen on the screen. There could be hidden lines. And several of the tactics used in the NNG are redefined to work slightly differently. So it won't really be a minimal working example. It generally won't work. It would need the imports and everything.

[Mohammad Pedramfar]

Jalex Stark said:

Jalex Stark said:

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

so it would have the URL of the current level plus the current proof script, and I guess also the statement of the theorem so that people who don't click the link can follow the discussion

That's doable, but it will only be useful for Zulip. The user won't be able to actually run the text that's copied into the clipboard. Wouldn't it be confusing for the users who don't use Zulip?

[Kevin Buzzard]

@edderiofer did you get the answer to your question? I've only just arrived.

[edderiofer]

Which of my many questions? :P

(Yes.)

[Mario Carneiro]

Mohammad Pedramfar said:

The things that are sent to the Lean server are not limited to what can be seen on the screen. There could be hidden lines. And several of the tactics used in the NNG are redefined to work slightly differently. So it won't really be a minimal working example. It generally won't work. It would need the imports and everything.

I know. Unless there is a good reason to hide them (e.g. if the solution is in there), I'm thinking everything in the level file, including any hidden lines, but not the entirety of NNG.

[Jalex Stark]

Mohammad Pedramfar said:

Jalex Stark said:

Jalex Stark said:

The feature request that came up in this thread was "click a button to generate a MWE that could be copied and pasted into zulip"

so it would have the URL of the current level plus the current proof script, and I guess also the statement of the theorem so that people who don't click the link can follow the discussion

That's doable, but it will only be useful for Zulip. The user won't be able to actually run the text that's copied into the clipboard. Wouldn't it be confusing for the users who don't use Zulip?

hah, I guess around here we have some kind of bias towards zulip users :)
The text that comes out is pretty close to working, which is plenty good if you're using it to talk to people, but maybe is disheartening if you're working on your own. I agree that it's not clear whether there's a version of this that's useful on average over all users.

[Mario Carneiro]

So there is the possibility that it's not a perfect MWE but it should get close enough for people to get the gist

[Jalex Stark]

Mario Carneiro said:

So there is the possibility that it's not a perfect MWE but it should get close enough for people to get the gist

unless the people are not yet good at reading error messages

[Mario Carneiro]

I think if you want a faithful version of NNG offline you can download the repo and use vscode

[Jalex Stark]

oh yeah I forgot that is a thing

[Kenny Lau]

why can't we just use the NNG website?

[Mario Carneiro]

but my goal here is to improve the state of affairs over

induction b, apply h1 h2
it doesn't work

[Jalex Stark]

well I think the goal is to make it so that first time posters are more likely to post a complete thing

[Jalex Stark]

having them link us to the NNG website is good

[Mario Carneiro]

it also requires me to load a link, which may be more or less complicated if I'm on a phone or something

[Mario Carneiro]

having inline code is good

[Mario Carneiro]

but when people type text into NNG all the context is gone. I want some bare minimum of context to understand the question. I have no idea what world 4 level 7 is

[Reid Barton]

I think it'd be more useful to have the NNG website give the user a link to the level they're solving with their code filled in

[Reid Barton]

Then you get more of the true context (including whatever the level is supposed to be teaching, etc)

[Kevin Buzzard]

@Jalex Stark while you're here, I pushed a new version of NNG recently, and now I have a FAQ and thanks to Mohammad, save game functionality. You seemed to have some very clear visions for what this game should look like and we recently had a conversation about it; I am hoping I dealt with some of your comments in v1.3.2 but I'd be very happy to hear if you still had more.

[Kevin Buzzard]

@Mario Carneiro as of recently we can actually link directly to that level (this is new as of about last week), so it will be much easier in the future. I don't have any idea either, and when I look in the source code the worlds are called different things to what the users call them which makes life even worse :-)

[Kevin Buzzard]

Not only that, remember that I am using a modified rw, induction, cases etc, so these things are actually perhaps not appropriate for mwes in the traditional sense.

[Mario Carneiro]

My main complaint is about "raw" tactic scripts. Even if it doesn't run, seeing theorem foo : ... at the start makes things a lot easier

[Jalex Stark]

Kevin Buzzard said:

Mario Carneiro as of recently we can actually link directly to that level (this is new as of about last week), so it will be much easier in the future. I don't have any idea either, and when I look in the source code the worlds are called different things to what the users call them which makes life even worse :-)

We added some text to the #mwe page telling people to use level links when they post in zulip chat :)
(I'll think a bit on your other question.)

[Reid Barton]

I think there are weird features or hacks you can use to cause some surrounding text to be included if the user copies their text, but not sure if advisable

[Mohammad Pedramfar]

An idea I had was to put the theorem statements into the editor together with the proof, but make the first and the last line read-only. So the user can't edit the statement, but when they want to copy, they can select all of it. Unfortunately, monaco-editor, which is used in the NNG and other places with Lean on the web, doesn't have this option. One way to go around it would be to use another text editor, like Ace editor, which has this function. But that seems to be very difficult. I would need to redefine the Lean syntax and autocompletion and highlighting and everything for a new editor. Besides, this seems to be the only way Ace editor is better. Monaco editor is the web-based version of VS code, which is why things work so well.

[Reid Barton]

Maybe just have a button which has the effect of copying the user's text together with the surrounding statement/tactic?

[Bryan Gin-ge Chen]

I wrote some Lean integration for CodeMirror for my Observable notebooks which I could try to extract if there's interest.

[Mohammad Pedramfar]

Reid Barton said:

Maybe just have a button which has the effect of copying the user's text together with the surrounding statement/tactic?

Yeah, I'm starting to think adding a button that would copy the content and the statement would be the most efficient way. The main page of NNG has a link to a FAQ page describing why Lean is different than the NNG, so I guess it wouldn't be that confusing for a user when they see it doesn't work.

[Mohammad Pedramfar]

Bryan Gin-ge Chen said:

I wrote some Lean integration for CodeMirror for my Observable notebooks which I could try to extract if there's interest.

That might be useful, but I'll go with the simpler approach this time. :)
It's on github, right? Why didn't you use monaco-editor?

[Bryan Gin-ge Chen]

It's on github, right? Why didn't you use monaco-editor?

Yes, CodeMirror is on github. I remember thinking that monaco would be too heavy-weight (in terms of file-size) to include, and it also looked to be a lot of work to bundle it properly for my use-case. In the end it wasn't too hard to write a Lean integration for CodeMirror following what was already done for monaco in the lean-web-editor, since the CodeMirror API is fairly simple.

[Mohammad Pedramfar]

That's good to know. My impression was that it would be difficult to use another editor.

[Mohammad Pedramfar]

I forgot to mention it here. The button is added in the Lean-game-maker repo. It will be there in the next update of the game. It took a while since I was fixing a few bugs.