Zulip Chat Archive

Stream: general

Topic: Big Proof

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.

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.

Neil Strickland (Feb 12 2019 at 08:05):

I'm going to the Edinburgh thing.

Kevin Buzzard (Feb 12 2019 at 08:10):

I'll be there Monday to Wednesday

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:

Rob Lewis (Feb 12 2019 at 08:45):

I'll be there.

Jeremy Avigad (Feb 12 2019 at 15:19):

I'll be there through Friday morning.

Simon Hudon (Feb 12 2019 at 15:49):

Do you guys know what you'll talk about?

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.

Jeremy Avigad (Feb 12 2019 at 16:09):

Not yet.

Reid Barton (May 25 2019 at 16:29):

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

Last updated: Aug 03 2023 at 10:10 UTC