Zulip Chat Archive

Stream: new members

Topic: (no topic)


Andrew Ashworth (Feb 26 2018 at 16:14):

This message has no topic

Andrew Ashworth (Feb 26 2018 at 16:14):

yes, you need to reply to threads explicitly, but small questions need not have their own topic, it seems

Andrew Ashworth (Feb 26 2018 at 16:16):

previously people were doing @person | quote "..." and then their reply

Andrew Ashworth (Feb 26 2018 at 16:16):

this is definitely better for a larger chat room. which hopefully will happen since Lean is going to be super popular

Sebastian Ullrich (Feb 26 2018 at 16:17):

I mean, the Gitter one is already larger than I can care to follow

Andrew Ashworth (Feb 26 2018 at 16:19):

are you ferinko

Simon Hudon (Feb 26 2018 at 16:19):

I was going to ask that! It will be weird referring to people by name instead of handle

Patrick Massot (Feb 26 2018 at 16:20):

Hi everyone!

Andrew Ashworth (Feb 26 2018 at 16:20):

well, Moses isn't actually his name either, haha

Andrew Ashworth (Feb 26 2018 at 16:21):

well, this is just the new members room, I didn't want to pollute #general with off topic comments

Moses Schönfinkel (Feb 26 2018 at 16:21):

It is?

Moses Schönfinkel (Feb 26 2018 at 16:23):

Interesting. I was apparently using the "all messages" tab which somehow forwarded to New Members automatically.

Kevin Buzzard (Feb 26 2018 at 17:37):

Well this is very modern.

Kevin Buzzard (Feb 26 2018 at 17:37):

I had trouble logging in with github, I had to go back a forth a while, but we got there in the end

Sebastian Ullrich (Feb 26 2018 at 17:40):

The design isn't exactly modern :laughing: . But other than that, I like it.

Andrew Ashworth (Feb 26 2018 at 17:41):

i wonder if there's an option to customize the css styling anywhere

Sean Leather (Feb 26 2018 at 19:05):

I also had trouble registering and signing in. Had to figure out which cookies to allow.

Sean Leather (Feb 26 2018 at 19:05):

What does the gray text mean?

Sean Leather (Feb 26 2018 at 19:06):

Oh, I think I see. It's a different channel?

Andrew Ashworth (Feb 26 2018 at 19:06):

everything on zulip is filtered by topic and stream

Sean Leather (Feb 26 2018 at 19:07):

Yeah, it's confusing to see different streams interleaved on one page.

Simon Hudon (Feb 26 2018 at 19:07):

If you click on a topic, you'll only see the messages that belong to that topic

Andrew Ashworth (Feb 26 2018 at 19:08):

probably want to deselect "all messages" at the top left of your screen then

Andrew Ashworth (Feb 26 2018 at 19:09):

zulip is what i think happened when a bulletin board and irc server had a lovechild

Sean Leather (Feb 26 2018 at 19:09):

It's the #new members view that I'm on. I don't yet know what topics I'm interested in, so I'm not sure which ones to look at.

Sean Leather (Feb 26 2018 at 19:10):

I don't see a way to merge topics. That would probably help.

Andrew Ashworth (Feb 26 2018 at 19:10):

if topics share something in common they should probably be filtered at the stream level

Dan Abolafia (Mar 29 2020 at 18:16):

(deleted)

Kevin Buzzard (Apr 03 2020 at 21:28):

(deleted)

Nam (Apr 11 2020 at 18:46):

somehow that line still worked ;).

Kevin Buzzard (Apr 11 2020 at 18:47):

You just changed thread. I am surprised it worked actually!

Nam (Apr 11 2020 at 18:47):

darn. i apologize. this tool needs some time to get used to.

Lukas (Apr 11 2020 at 18:52):

Hello,

I want to proof the following case:

case mynat.succ
t b d : mynat,
dh : t * (d + b) = t * d + t * b
⊢ t * (succ d + b) = t * succ d + t * b

my idea is to rw dh to get t * succ d + t * b on the left side. I think it should work because succ d should also be a mynat.

However I get

tactic failed, there are unsolved goals
state:
case mynat.succ
t b d : mynat,
dh : t * (d + b) = t * d + t * b
⊢ t * (succ d + b) = t * succ d + t * b

Did I missunderstood something or do I have to give an additional hint in the rw step?

Kevin Buzzard (Apr 11 2020 at 18:53):

You definitely can't do rw dh

Kevin Buzzard (Apr 11 2020 at 18:53):

If dh : A = B then rw dh will only work when there is something exactly equal to A in the goal

Kevin Buzzard (Apr 11 2020 at 18:54):

i.e. you really need exactly the symbols t * (d + b) in the goal for rw dh to work.

Kevin Buzzard (Apr 11 2020 at 18:55):

If dh said something like ∀ d, t * (d + b) = t * d + t * b then you would be OK. But it doesn't.

Kevin Buzzard (Apr 11 2020 at 18:55):

dh just says that something is true for that one specific d, not all d.

Lukas (Apr 11 2020 at 18:56):

Kevin Buzzard said:

i.e. you really need exactly the symbols t * (d + b) in the goal for rw dh to work.

okay thanks,

can I somehow substitute the succ d into a new variable and then it will work - or is that the wrong direction?

Kevin Buzzard (Apr 11 2020 at 18:56):

If induction was that easy, then you would be able to prove pretty much any statement by induction.

Kevin Buzzard (Apr 11 2020 at 18:56):

you have fixed naturals t and b and d, and dh is only a statement about those fixed naturals.

Kevin Buzzard (Apr 11 2020 at 18:56):

Look, here is a proof that for every natural number nn, we have n=n2n=n^2.

Kevin Buzzard (Apr 11 2020 at 18:57):

Let's prove it by induction.

Kevin Buzzard (Apr 11 2020 at 18:57):

The base case is fine -- because 0=020=0^2.

Kevin Buzzard (Apr 11 2020 at 18:57):

Now for the inductive step, let nn be any natural at all.

Kevin Buzzard (Apr 11 2020 at 18:58):

Let's assume h : n = n^2 and try and deduce succ n = (succ n)^2

Kevin Buzzard (Apr 11 2020 at 18:58):

By your way of thinking, n is an arbitrary natural number, so we can let it be succ n and use h to prove what we want to prove.

Kevin Buzzard (Apr 11 2020 at 18:58):

That can't be how induction works though, because what we're trying to prove isn't true.

Lukas (Apr 11 2020 at 18:59):

okay thanks for the explanation

Jalex Stark (May 10 2020 at 23:45):

(deleted)

Golol (May 11 2020 at 11:44):

(deleted)

Jason Orendorff (Jun 04 2020 at 07:12):

(deleted)

Pedro Minicz (Jun 13 2020 at 19:15):

(tmp)

Michael Beeson (Jun 30 2020 at 00:29):

So, the parameter M:Type that is mentioned in the class definition doesn't get passed automatically with the members of the class, in this case Rel and p44. I need to mention M in defining test. When I've successfully defined test, and I want to use it, I have to pass M as the first argument, e.g. test M. Then it's the passed M that will be used as the type of p44. That explains why you have to pass M as an argument to test. Are these statements correct?

Kevin Buzzard (Jun 30 2020 at 07:07):

These statements are in the wrong topic (and you could move them)

Kevin Buzzard (Jun 30 2020 at 07:07):

Look at the type of Rel. It takes M as an input.

Kevin Buzzard (Jun 30 2020 at 07:08):

#check @Rel

Xavier Xarles (Jul 04 2020 at 20:33):

(deleted)

Patrick Lutz (Jul 08 2020 at 22:42):

(deleted)

Emiel Lanckriet (Jul 20 2020 at 10:55):

Install mathematics_in_lean, I wanted to start looking at the online book Mathematics in Lean. I installed Lean in VS code as they suggested, but when I run the commando leanproject get mathematics_in_lean in Git Bash, the program ask for a password this is the exact response:
Please provide password for encrypted SSH private key:
However, there is no mention of a password in the text, so what is the password or where did I go wrong?

Kevin Buzzard (Jul 20 2020 at 10:55):

I think that this might be your SSH private key, if you set up SSH keys in github

Kevin Buzzard (Jul 20 2020 at 10:56):

GitHub is asking you to authenticate, it looks like

Emiel Lanckriet (Jul 20 2020 at 10:56):

Ok, I will take a look at that.

Kevin Buzzard (Jul 20 2020 at 10:56):

Stepping back a bit -- do you have a userid at the GitHub website?

Emiel Lanckriet (Jul 20 2020 at 10:57):

Yes

Kevin Buzzard (Jul 20 2020 at 10:58):

Ok so GitHub is perhaps saying "instead of providing your github password, just let me know that you are you, because you set up an ssh key at some point". I'm not an expert, this is kind of a guess.

Filippo A. E. Nuccio (Sep 10 2020 at 11:04):

(deleted)

Malo Jaffré (Sep 28 2020 at 17:48):

(deleted)

Kevin Buzzard (Sep 28 2020 at 18:06):

(deleted)

Wrenna Robson (Nov 13 2020 at 21:43):

If I have other questions on different kata, is it better etiquette here to start a new thread or continue this one?

Jalex Stark (Nov 13 2020 at 21:57):

Wrenna Robson said:

If I have other questions on different kata, is it better etiquette here to start a new thread or continue this one?

You probably meant to post this on some particular other thread. But generally it's good etiquette to start a new topic for every "different" question. Really the point is that you want to give people the opportunity to stop paying attention to topics they don't care about, and this is easier if individual topics are small

Wrenna Robson (Nov 13 2020 at 21:58):

Thanks!

Hanting Zhang (Dec 31 2020 at 22:10):

(deleted)

Jakob Scholbach (Jan 31 2021 at 14:45):


Mark Gerads (Mar 01 2021 at 20:05):

https://github.com/leanprover-community/mathlib/pull/6484#issuecomment-788189034
bors says:

Build failed (retrying...):

Build mathlib

But I see

@github-actions
continuous integration / Build mathlib (push) Successful in 118m
Details

Does this mean that my pull request somehow conflicted with another pull request which was accepted within the time since I downloaded Mathib, in which case, I should remake the pull request? This is my best guess as of now. I am unable to see the details of the fail.
When I press

@bors
bors  Build failed
Details
Permission denied

Thus I can only guess. Hmmm. May I have permission to see the details?

Bryan Gin-ge Chen (Mar 01 2021 at 20:07):

The Build mathlib link has all the details that are needed.

In this case, the issue was with another PR #6452: https://github.com/leanprover-community/mathlib/pull/6452#pullrequestreview-601069376

Mark Gerads (Mar 01 2021 at 20:08):

I need to know how to pull any recent changes from master to my branch. Maybe I should just delete the branch and start from scratch though; 'tis a simple solution.

Bryan Gin-ge Chen (Mar 01 2021 at 20:08):

For what it's worth, the bors page doesn't actually have much useful information in this case: Screen-Shot-2021-03-01-at-3.08.13-PM.png

(Sometimes when bors crashes the log page will have some crash log details...)

Bryan Gin-ge Chen (Mar 01 2021 at 20:10):

Mark Gerads said:

I need to know how to pull any recent changes from master to my branch. Maybe I should just delete the branch and start from scratch though; 'tis a simple solution.

I think your branch is fine, but for future reference, I think git fetch origin then git merge origin/master should work.

Moritz Firsching (Mar 14 2021 at 12:54):

(deleted)

Kevin Buzzard (Apr 07 2021 at 14:56):

(deleted)

Hanting Zhang (Apr 17 2021 at 05:35):

(deleted)

Matúš Behun (Apr 21 2021 at 23:49):

what's best way to find stuff in mathlib, so far i am using grep and file hierarchy, e.g. I am looking for definition of order or linear_order

Eric Rodriguez (Apr 21 2021 at 23:50):

my favourite is example : <stuff> := by library_search, although the docs with some decent keywords can be okay

Matúš Behun (Apr 21 2021 at 23:57):

cheers, hovering with mouse over keyword helped in this case

Matúš Behun (May 06 2021 at 12:03):

What's difference between constant and variable declaration

Kevin Buzzard (May 06 2021 at 12:05):

Can you ask this question in a thread with a topic name? Or edit the topic name for your post?

Patrick Massot (May 06 2021 at 12:13):

Did you read https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections? That would be the first step.

Eric Wieser (May 06 2021 at 12:15):

Zulip admins, can we turn off "no topic" topics? https://zulip.com/help/require-topics

Rudi Cilibrasi (Nov 12 2021 at 18:52):

We can help you install lean and mathlib if you have any difficulties. I installed to reproduce Mario result above that the zero function is the 5th program in partrec hehehe

Eric Wieser (Nov 12 2021 at 19:53):

(you can edit your message above to change the "topic" so that it moves to the right place)


Last updated: Dec 20 2023 at 11:08 UTC