## Stream: new members

### Topic: getting started

#### Brandon Wu (May 07 2020 at 20:19):

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 (May 07 2020 at 20:23):

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

#### Kevin Buzzard (May 07 2020 at 20:23):

or you clone the tutorial project

#### Brandon Wu (May 07 2020 at 20:31):

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 (May 07 2020 at 20:39):

What kind of Unix is that?

#### Reid Barton (May 07 2020 at 20:43):

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

#### Reid Barton (May 07 2020 at 20:46):

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

#### Brandon Wu (May 07 2020 at 20:53):

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 (May 07 2020 at 20:58):

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 (May 07 2020 at 20:58):

Though I've never tried building elan

#### Filippo A. E. Nuccio (May 08 2020 at 14:33):

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 (May 08 2020 at 14:35):

doing exercises on codewars is a nice way to learn things

#### Jalex Stark (May 08 2020 at 14:36):

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

#### Jalex Stark (May 08 2020 at 14:37):

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

#### Jalex Stark (May 08 2020 at 14:38):

i guess you can also read the code on github directly

#### Johan Commelin (May 08 2020 at 14:40):

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

#### Filippo A. E. Nuccio (May 08 2020 at 14:40):

Yes, I do. And thanks for the welcome.

#### Johan Commelin (May 08 2020 at 14:40):

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

Ok, great

#### Filippo A. E. Nuccio (May 08 2020 at 14:41):

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 (May 08 2020 at 14:41):

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 (May 08 2020 at 14:42):

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 (May 08 2020 at 14:42):

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

#### Mario Carneiro (May 08 2020 at 14:43):

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 (May 08 2020 at 14:44):

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 (May 08 2020 at 14:44):

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

#### Johan Commelin (May 08 2020 at 14:47):

@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 (May 08 2020 at 14:47):

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

#### Filippo A. E. Nuccio (May 08 2020 at 14:49):

@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 (May 08 2020 at 14:50):

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

#### Jalex Stark (May 08 2020 at 14:52):

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

#### Jalex Stark (May 08 2020 at 14:53):

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

#### Filippo A. E. Nuccio (May 08 2020 at 14:55):

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 (May 08 2020 at 14:57):

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 (May 08 2020 at 14:57):

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 (May 08 2020 at 14:58):

@Bryan Gin-ge Chen Thanks!

#### Bryan Gin-ge Chen (May 08 2020 at 15:00):

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

#### Filippo A. E. Nuccio (May 08 2020 at 15:01):

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 (May 08 2020 at 15:04):

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 (May 08 2020 at 15:05):

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

#### Bryan Gin-ge Chen (May 08 2020 at 15:06):

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 (May 08 2020 at 15:07):

@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 (May 08 2020 at 15:07):

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

#### Filippo A. E. Nuccio (May 08 2020 at 15:10):

@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 (May 08 2020 at 16:29):

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 (May 08 2020 at 16:41):

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 (May 08 2020 at 16:50):

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.

#### Patrick Stevens (May 08 2020 at 18:11):

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 (May 09 2020 at 13:01):

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!

#### Filippo A. E. Nuccio (May 09 2020 at 13:04):

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.

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 (May 09 2020 at 13:52):

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 (May 09 2020 at 13:52):

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

#### Patrick Stevens (May 09 2020 at 14:15):

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 (May 09 2020 at 14:15):

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

#### Patrick Massot (May 09 2020 at 14:20):

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 (May 09 2020 at 14:21):

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

#### Patrick Stevens (May 09 2020 at 14:29):

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 (May 09 2020 at 14:29):

In hindsight, quite an optimistic hope

#### Patrick Massot (May 09 2020 at 14:31):

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

#### Patrick Stevens (May 09 2020 at 14:32):

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

#### Patrick Massot (May 09 2020 at 14:33):

And also that you didn't rebase on master

#### Patrick Massot (May 09 2020 at 14:33):

But this is not a problem at all

This can wait

#### Patrick Massot (May 09 2020 at 14:33):

I'll release 0.0.6 now

#### Patrick Stevens (May 09 2020 at 14:33):

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

Sure, go for it

#### Patrick Massot (May 09 2020 at 14:34):

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

#### Patrick Massot (May 09 2020 at 14:34):

Yes, we can clean up history before merging

#### Patrick Massot (May 09 2020 at 14:35):

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

#### Patrick Stevens (May 09 2020 at 14:37):

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 (May 09 2020 at 14:45):

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

#### Patrick Massot (May 09 2020 at 15:06):

Python 3.8.0 (default, Dec  7 2019, 17:45:02)
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 (May 09 2020 at 15:06):

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 (May 09 2020 at 15:07):

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 (May 09 2020 at 15:10):

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 (May 09 2020 at 15:11):

And now I need to leave

#### Filippo A. E. Nuccio (May 12 2020 at 11:48):

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 (May 12 2020 at 11:54):

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 (May 12 2020 at 11:54):

and I am very busy with marking them :-/

#### Kevin Buzzard (May 12 2020 at 11:56):

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 (May 12 2020 at 11:59):

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 (May 12 2020 at 12:01):

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. (May 12 2020 at 12:19):

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 (May 12 2020 at 12:20):

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 (May 12 2020 at 19:27):

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.

#mwe?

#### Jalex Stark (May 12 2020 at 19:29):

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 (May 12 2020 at 19:29):

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 (May 12 2020 at 19:29):

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 (May 12 2020 at 19:30):

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

#### Jalex Stark (May 12 2020 at 19:30):

otherwise this is a big game of telephone where everybody loses

#### edderiofer (May 12 2020 at 19:32):

Yes, but I don't understand it.

#### Jalex Stark (May 12 2020 at 19:32):

The errors have lots of useful information in them

#### Jalex Stark (May 12 2020 at 19:32):

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

#### edderiofer (May 12 2020 at 19:32):

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 (May 12 2020 at 19:32):

yes, I think you said all of that already

#### edderiofer (May 12 2020 at 19:33):

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

#### Jalex Stark (May 12 2020 at 19:34):

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 (May 12 2020 at 19:34):

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

#### edderiofer (May 12 2020 at 19:34):

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 (May 12 2020 at 19:35):

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

#### Jalex Stark (May 12 2020 at 19:35):

try mul_eq_zero_iff _ _ h

#### edderiofer (May 12 2020 at 19:36):

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 (May 12 2020 at 19:37):

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 (May 12 2020 at 19:37):

so try one fewer underscore

#### edderiofer (May 12 2020 at 19:38):

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 (May 12 2020 at 19:39):

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 (May 12 2020 at 19:40):

That I need a second mynat as the second input.

#### edderiofer (May 12 2020 at 19:41):

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 (May 12 2020 at 19:41):

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

#### Jalex Stark (May 12 2020 at 19:42):

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

#### Patrick Massot (May 12 2020 at 19:44):

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

#### Patrick Massot (May 12 2020 at 19:45):

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

#### Jalex Stark (May 12 2020 at 19:45):

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

#### Jalex Stark (May 12 2020 at 19:45):

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

#### Jalex Stark (May 12 2020 at 19:46):

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

#### Jalex Stark (May 12 2020 at 19:46):

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

#### Jalex Stark (May 12 2020 at 19:47):

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

#### edderiofer (May 12 2020 at 19:48):

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 (May 12 2020 at 19:49):

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

#### edderiofer (May 12 2020 at 19:50):

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

#### Jalex Stark (May 12 2020 at 19:51):

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

#### Jalex Stark (May 12 2020 at 19:51):

you could start by including the theorem statement

#### Jalex Stark (May 12 2020 at 19:52):

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

#### Jalex Stark (May 12 2020 at 19:53):

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 (May 12 2020 at 19:53):

@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 (May 12 2020 at 19:54):

@ROCKY KAMEN-RUBIO you're missing import tactic

Thanks!

#### Patrick Massot (May 12 2020 at 19:55):

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 (May 12 2020 at 19:55):

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 (May 12 2020 at 19:55):

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 (May 12 2020 at 19:55):

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

#### Jalex Stark (May 12 2020 at 19:55):

you could do rwa mul_eq_zero_iff a b at h,

#### Jalex Stark (May 12 2020 at 19:56):

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

Ah, OK.

#### Jalex Stark (May 12 2020 at 19:57):

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 (May 12 2020 at 19:58):

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

#### Jalex Stark (May 12 2020 at 19:59):

then you want apply

#### Jalex Stark (May 12 2020 at 20:00):

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

#### ROCKY KAMEN-RUBIO (May 12 2020 at 20:00):

@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 (May 12 2020 at 20:00):

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

#### Patrick Massot (May 12 2020 at 20:01):

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 (May 12 2020 at 20:02):

where "normal" means "mathlib-approved"?

#### Patrick Massot (May 12 2020 at 20:02):

efficiency approved

#### ROCKY KAMEN-RUBIO (May 12 2020 at 20:02):

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 (May 12 2020 at 20:03):

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

#### Jalex Stark (May 12 2020 at 20:03):

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 (May 12 2020 at 20:03):

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

#### Jalex Stark (May 12 2020 at 20:04):

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

#### Jalex Stark (May 12 2020 at 20:04):

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

#### ROCKY KAMEN-RUBIO (May 12 2020 at 20:04):

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 (May 12 2020 at 20:05):

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

#### Jalex Stark (May 12 2020 at 20:05):

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

#### Jalex Stark (May 12 2020 at 20:05):

but maybe I am wrong

#### Patrick Massot (May 12 2020 at 20:06):

I mostly meant efficiency in writing speed.

#### Jalex Stark (May 12 2020 at 20:07):

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

#### Patrick Massot (May 12 2020 at 20:07):

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.

interesting

#### Jalex Stark (May 12 2020 at 20:08):

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

#### Patrick Massot (May 12 2020 at 20:08):

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

ah okay

#### Jalex Stark (May 12 2020 at 20:09):

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

#### Jalex Stark (May 12 2020 at 20:10):

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

#### Jalex Stark (May 12 2020 at 20:11):

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 (May 12 2020 at 20:12):

If "Natural Number Game" were capitalized, definitely.

#### Jalex Stark (May 12 2020 at 20:16):

haha thanks, fixing that now

#### Jalex Stark (May 12 2020 at 20:19):

okay, I added a fairly explicit example to #mwe

Yep, that works.

#### Jalex Stark (May 12 2020 at 20:21):

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 (May 12 2020 at 20:22):

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 (May 12 2020 at 20:23):

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

#### edderiofer (May 12 2020 at 20:24):

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

#### Jalex Stark (May 12 2020 at 20:27):

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

#### edderiofer (May 12 2020 at 20:30):

Yep, definitely don't recognize that username.

#### edderiofer (May 12 2020 at 20:31):

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

#### Jalex Stark (May 12 2020 at 20:31):

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

#### Jalex Stark (May 12 2020 at 20:32):

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

#### Jalex Stark (May 12 2020 at 20:32):

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

#### Bryan Gin-ge Chen (May 12 2020 at 20:32):

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

#### Jalex Stark (May 12 2020 at 20:33):

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 (May 12 2020 at 20:34):

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

#### Jalex Stark (May 12 2020 at 20:34):

(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 (May 12 2020 at 20:42):

Still trying to think of a new idea.

#### Mohammad Pedramfar (May 12 2020 at 20:51):

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 (May 12 2020 at 20:52):

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 (May 12 2020 at 20:53):

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 (May 12 2020 at 20:53):

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 (May 12 2020 at 20:53):

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 (May 12 2020 at 20:55):

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 (May 12 2020 at 20:56):

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

#### edderiofer (May 12 2020 at 20:56):

Is there a quick way to comment out a line?

#### Mario Carneiro (May 12 2020 at 20:56):

-- comment

#### Bryan Gin-ge Chen (May 12 2020 at 20:57):

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

#### Jalex Stark (May 12 2020 at 20:57):

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

#### Jalex Stark (May 12 2020 at 20:58):

/-
like this
-/


#### Bryan Gin-ge Chen (May 12 2020 at 21:00):

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 (May 12 2020 at 21:02):

a lot of web editors have the same keybinding

#### Jalex Stark (May 12 2020 at 21:02):

I use cmd-/ in jupyter and overleaf

#### edderiofer (May 12 2020 at 21:02):

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 (May 12 2020 at 21:03):

symmetry at h

Thanks.

#### Jalex Stark (May 12 2020 at 21:04):

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

#### Jalex Stark (May 12 2020 at 21:04):

mostly so that people later can read old conversations

Ah, alright.

#### Mohammad Pedramfar (May 12 2020 at 21:22):

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 (May 12 2020 at 21:28):

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 (May 12 2020 at 21:32):

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

#### edderiofer (May 12 2020 at 21:42):

Which of my many questions? :P

(Yes.)

#### Mario Carneiro (May 12 2020 at 21:46):

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 (May 12 2020 at 21:46):

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 (May 12 2020 at 21:47):

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 (May 12 2020 at 21:47):

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 (May 12 2020 at 21:48):

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

#### Jalex Stark (May 12 2020 at 21:49):

oh yeah I forgot that is a thing

#### Kenny Lau (May 12 2020 at 21:49):

why can't we just use the NNG website?

#### Mario Carneiro (May 12 2020 at 21:49):

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

 induction b, apply h1 h2 
it doesn't work

#### Jalex Stark (May 12 2020 at 21:50):

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

#### Jalex Stark (May 12 2020 at 21:50):

having them link us to the NNG website is good

#### Mario Carneiro (May 12 2020 at 21:51):

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 (May 12 2020 at 21:51):

having inline code is good

#### Mario Carneiro (May 12 2020 at 21:52):

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 (May 12 2020 at 21:56):

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 (May 12 2020 at 21:57):

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

#### Kevin Buzzard (May 12 2020 at 21:57):

@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 (May 12 2020 at 21:58):

@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 (May 12 2020 at 21:58):

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 (May 12 2020 at 21:59):

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 (May 12 2020 at 21:59):

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 (May 12 2020 at 22:02):

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 (May 12 2020 at 22:30):

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 (May 12 2020 at 22:32):

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 (May 12 2020 at 22:32):

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

#### Mohammad Pedramfar (May 12 2020 at 22:37):

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 (May 12 2020 at 22:39):

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 (May 12 2020 at 22:52):

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 (May 13 2020 at 00:59):

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

#### Mohammad Pedramfar (May 22 2020 at 21:14):

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.

Last updated: May 12 2021 at 22:15 UTC