Zulip Chat Archive

Stream: sphere eversion

Topic: Confusing blueprint

Patrick Massot (Sep 04 2022 at 19:52):

Tonight I wanted to apply the updating lemma. But I found the Lean statement very confusing. So I returned to the blueprint and I was shocked to see that I wrote an extremely confusing statement there, which was then faithfully translated to a confusing Lean statement. I remember having edited the structure of that statement several times because I wanted one lemma stating the two properties I needed about updating. I guess the first version had sloppy but still arguably correct quantifiers and then I decided to use an itemize environment which pushed the situation over the edge. You may want to pause here, go read that lemma in the blueprint, and try to guess what I meant to write.

Patrick Massot (Sep 04 2022 at 19:54):

Yes, the positive η\eta isn't meant to depend on gg. What happens in the real world in such situations is that the statement is wrong but the proof is correct, and readers are then expected to fix the statement (consciously or not). The fun thing is that Lean doesn't fix the statement alone, but it is very convenient to take the correct proof into a proof of the correct statement. No line of the corrected proof is new.

Last updated: Dec 20 2023 at 11:08 UTC