Big Proof

Stream: general

[Patrick Massot]

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]

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]

I'm going to the Edinburgh thing.

[Kevin Buzzard]

I'll be there Monday to Wednesday

[Johan Commelin]

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]

I'll be there.

[Jeremy Avigad]

I'll be there through Friday morning.

[Simon Hudon]

Do you guys know what you'll talk about?

[Kevin Buzzard]

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]

Not yet.

[Reid Barton]

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