[compiler-devel]

I can’t help but confess some sense of satisfaction with the upheaval described in the post. Many proofs and textbooks laden with statements like “without loss of generality”, “immediately”, or “obviously” are followed by anything but. AI now counters that streak of smug by toppling some long held theorems and it’s fun to watch.

[Jtarii]

Bit weird that your first reaction to a human expressing genuine emotional pain is glee.

[compiler-devel]

I’m also a human expressing genuine emotion. Why is one more valid than the other?

[jlev1]

Your emotion isn’t invalid, it’s merely bad, assholeish, brings shame upon you. But it is “valid” in the sense that the reader of your comment can see that you are, at least, sincere in your gloating at another person’s despair.

[compiler-devel]

It's not the despair, it's the turnabout. Reading proofs containing the language that I mentioned seemed to suggest that the ideas were trivial to the author in a way that implied their superior intelligence. Now AI has come along and has, by way of counterexamples, shown theorems to be incorrect in devastating (maybe "trivial") ways. The shoe is on the other foot.

[jlev1]

Well, in all honesty, I’m sorry you had that experience (seriously). I hate feeling condescended to and I’ve also had that experience before, including from mathematicians.

When it comes to the specific phrases you mentioned, though, that really is not my understanding of the meaning of “obvious” or “trivial” or “without loss of generality”.

Without loss of generality means there is some kind of symmetry or repetition in a proof that makes certain cases redundant, so that “without loss of generality” we can assume we’re in some simpler case, such as assuming x <= y in a proof where x and y are interchangeable (and so one of them is necessarily <= the other). This is even the name of a tactic in Lean, `wlog`.

“Trivial” when I encounter or use it nearly always means something to do with zero, the empty set, the group with just one element, and so on. A proof being trivial usually means there is essentially nothing to prove (because the object in question is empty or zero or whatever).

And “obvious” definitely comes closest to what you were objecting to, and many mathematicians try to avoid it these days (along with “clear”), but even then it has a legitimate use case, namely indicating when a proof involves no new ideas. To me, this means it is fine to use it within a specified context, like in a textbook or paper, where certain techniques are being used repeatedly and routinely, or certain kinds of background knowledge are assumed. And even then it’s usually meant for proofs that don’t rely on tricks or surprises or additional insights. I’ve been stuck on trying to understand “obvious” proofs before, and it wasn’t because I was stupid or the author was smarter than me, it was because I was _missing something obvious_ (in hindsight).

The recent Jacobian conjecture counterexample, for instance, is not trivial but arguably a bit embarrassingly (for the math world) close to obvious in hindsight. I still wouldn’t actually call it obvious though.

[vouaobrasil]

Yeah I think it's weird too. But tech really does amplify narcissism because it makes us very independent from people and community. So it's really not surprising that half the people in this thread are more concerned with manufacturing discovery than they are with having a cohesive society.

[hollerith]

AI hasn't "toppled" (or found any mistakes in) any theorems, at least not any enjoying any consensus among mathematicians.

[inigyou]

It might mean you're missing some prerequisite knowledge. Unfortunately if every textbook started from square one, they'd be a million times longer.