example: (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r)

Stream: new members

[Eduardo Cavazos]

Posted a question about one of the examples in section 3.6 of TPIL to stackoverflow:

https://stackoverflow.com/q/58406492/268581

[Johan Commelin]

@Eduardo Cavazos It depends a bit on what you want. You can probably solve this by tauto if you are fine with using tactics. If you merely want to avoid the duplication, you can use have a_name : some_prop, from a_proof to state the key step once, and then use a_name in two places.

[Mario Carneiro]

Could you repost the question here? I don't think SO is used very much for lean questions.

[Kevin Buzzard]

Could you repost the question here? I don't think SO is used very much for lean questions.

@Scott Morrison has pointed out that this attitude might be hurting us, and I believe him.

[Kevin Buzzard]

I'll post an answer.

[Kevin Buzzard]

https://stackoverflow.com/a/58408366/951113

[Johan Commelin]

You've got an upvote :rolling_on_the_floor_laughing:

[Mario Carneiro]

Could you elaborate? I like SO but it's better for really big communities where the volume and number of experts is higher.

[Kevin Buzzard]

Scott says it's much better for visibility, and in one sense the fact that so much goes on here behind closed doors is harmful. The fact is that people go to SO to look at computer questions and we're never going to be "trending" there because of this

[Kevin Buzzard]

If things get bigger then we'll have people asking the same questions here week in week out and then folks might get grumpy. On SO someone asks once and then within a year the question has 100 upvotes and people can find the answer using Google

[Kevin Buzzard]

Basically I'm saying "what if it gets bigger?"

[Rob Lewis]

The Zulip archive was supposed to be a partial solution for this. Obviously it doesn't have the SEO that StackOverflow has, but at least the conversations here aren't entirely hidden. It gets a slow trickle of traffic with the same recent spike that we've seen here. Here's the graph from Google, which doesn't include hits from other search engines, but gives an idea. zulip_archive.png

[Rob Lewis]

I think it includes the page on the perfectoid project, which accounts for some of the recent spike.

[Kevin Buzzard]

Obviously it doesn't have the SEO that StackOverflow has

This understatement is exactly the point, right? I don't really know what to do about this. It would be nice to have some sort of bot here which would flag it whenever someone posted a question on SO tagged Lean. I think I ran into a twitterbot which did this for Coq once.

[Scott Morrison]

This should be pretty easy. I have scripts that are running on my machine that send messages to zulip, and that scrape MathOverflow, and it's probably just a matter of concatenating those scripts, right? :-)

[Marc Huisinga]

zulip itself seems to provide a stackoverflow bot example, although it does not poll stack overflow
https://github.com/zulip/python-zulip-api/blob/master/zulip_bots/zulip_bots/bots/stack_overflow/stack_overflow.py