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):
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