Post #4200327

@escape_velocity@functional.cafe good job, you got me to double and triple check my sources because I don't want to spread misinformation okay so I'm going to assume you're saying all this because you know this person and respect their work and so want to defend them and, that's great, I sincerely believe they've done a lot of good work and are continuing to do so now by helping get this issue resolved but you're doing so by insisting they chose to be a colossal smug dick by publicly publishing a high-status "proof" they knew was buggy without mentioning that it's buggy, which somehow proves some sort of brilliant point. That makes them sound... awful and obnoxious? Is this what I was misinformed about, by assuming that they were posting in good faith and wouldn't deliberately lie about something this important? When YanYablonovskiy says (before apologizing for getting too stressed about it) "It (the bug) was hiding in plain sight sure, and it took a day of maybe believing it, but what if it was a month? What if news came out that had to be backtracked and expressly blamed on Lean?", this person clearly believed that the original proof was meant to be real and not a bug report. I cannot find any evidence, anywhere, aside from your surprising assertions, that this began as either some sort of cruel prank or a haha funny bug report that everyone was in on. The same user says "it would be a bit strange to lie" about the nanoda point of confusion, so clearly doesn't think OP was trying to cause problems on purpose. The discussion threads also show people expressing frustration that of course the LLM had to come up with something so non-minimal and then apologize for it coming across as being mad at OP, who didn't do anything wrong; I certainly wouldn't say OP didn't do anything wrong if I thought they were pulling a stupid stunt and wasting everyone's time! The discussion threads ALSO include people linking to the very social media post that also originally drew my attention!, and they quibble about some of the technical details but no-one disputes the fundamental premise, that a) a proof was posted, and b) THEN noticed to have a bug. kiranandcode, who posted a reduced version of the bug for triage purposes, describes as having found it while REVIEWING OP's proof. That does not sound like someone who already knew going in that it obviously had a soundness bug. The hypothesis that OP sincerely did not know about the verification bug seems a lot more charitable to a fellow human being, but, maybe it's not the human being you're trying to defend here after all... you sound a little too invested in the idea an LLM won't ever trick you or your friends. I deliberately didn't draw attention to anyone's names in my post, they're all just "someone" (and continuing to call OP "OP" here), because shaming whoever got tricked is not the point. It's learning the lesson that you, yes you, can be tricked that matters. But of course, if OP clarifies that they were lying for a stunt, I will gracefully concede that they're just kind of a dick. After going over all the sources, I concede that there's a gap between "the proof is posted to github" and "people begin discussing the bug" that I can't account for, and maybe OP was quite clear in a place I can't see that they were just being kind of a dick?