Zulip Chat Archive

Stream: general

Topic: new achievement

Reid Barton (Jun 27 2019 at 00:54):

Achievement unlocked: read something I proved in Lean to get the correct statement and proof for a paper I am writing

Simon Hudon (Jun 27 2019 at 01:00):

Can we see?

Reid Barton (Jun 27 2019 at 01:01):

Well the Lean version is https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/category_theory/model/category.lean#L32

Reid Barton (Jun 27 2019 at 01:02):

It's more convenient than looking in a book mostly because I know exactly where it is

Reid Barton (Jun 27 2019 at 01:06):

For the most part, once I know the statement is definitely correct, I can work out the proof (maybe taking a hint or two from the formalization)

Kevin Buzzard (Jun 27 2019 at 06:40):

You can just give a reference to the lean file for the proof

Kevin Buzzard (Jun 27 2019 at 06:41):

One could argue that this was more efficient and more accurate than the old fashioned way of trying to write down a paper proof

Kevin Buzzard (Jun 27 2019 at 06:42):

I guess the key question is what you want your readers to get from the proof. Just an indication that the result is true, or some sort of technique which they can use to prove similar results themselves?

Reid Barton (Jun 27 2019 at 09:41):

I actually needed to prove a similar result myself

Last updated: Dec 20 2023 at 11:08 UTC