Zulip Chat Archive

Stream: general

Topic: Big Proof


view this post on Zulip Patrick Massot (Sep 03 2018 at 19:37):

I have a question for people who understand how Lean actually works. I had a very big proof that took forever to compile, and sometimes timed out. I broke that proof in two pieces, introducing a completely artificial lemma, statement how to go half way along the road. Now it's super fast. What's happening? I understand there is something called https://github.com/leanprover/lean/issues/1601 which tells me I cannot work interactively with big proofs. But I don't understand why it changes the non-interactive compilation time.

view this post on Zulip Scott Morrison (Feb 12 2019 at 05:22):

Who is planning to go to Big Proof (May 27-31, Edinburgh)? Usually flying to Europe for a week for me is insane, but I may be able to do this one. Especially if there will be some Lean people there it would be tempting.

view this post on Zulip Neil Strickland (Feb 12 2019 at 08:05):

I'm going to the Edinburgh thing.

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 08:10):

I'll be there Monday to Wednesday

view this post on Zulip Johan Commelin (Feb 12 2019 at 08:14):

If @Patrick Massot goes, maybe he will finally get an answer to his question from 3 Sep 2018 in this very thread :rolling_on_the_floor_laughing:

view this post on Zulip Rob Lewis (Feb 12 2019 at 08:45):

I'll be there.

view this post on Zulip Jeremy Avigad (Feb 12 2019 at 15:19):

I'll be there through Friday morning.

view this post on Zulip Simon Hudon (Feb 12 2019 at 15:49):

Do you guys know what you'll talk about?

view this post on Zulip Kevin Buzzard (Feb 12 2019 at 15:53):

Ursula did ask me to speak, and I said "OK, schemes/perfectoid spaces, or teaching?" and she didn't reply (yet), so I'm up in the air.

view this post on Zulip Jeremy Avigad (Feb 12 2019 at 16:09):

Not yet.

view this post on Zulip Reid Barton (May 25 2019 at 16:29):

I will also be there and I just created a stream #Big Proof 2019


Last updated: May 14 2021 at 00:42 UTC