isn't it sufficient of an explanation that one has occasionally wasted a ton of time trying to read an article only to discover after studying and interpreting half of a paper that one of the author's proof steps is wholly unjustified?

is it so hard to understand that after a few such events, you wish for authors to check their own work by formalizing it, saving countless hours for your readers, by selecting your paper WITH machine readable proof versus another author's paper without a machine readable proof?

▲

hexaga 2 days ago | parent [-]

If wishes were fishes, as they say.

To demonstrate with another example: "Gee, dying sucks. It's 2025, have you considered just living forever?"

To this, one might attempt to justify: "Isn't it sufficient that dying sucks a lot? Is it so hard to understand that having seen people die, I really don't want to do that? It really really sucks!", to which could be replied: "It doesn't matter that it sucks, because that doesn't make it any easier to avoid."

▲

guerrilla 2 days ago | parent | next [-]

I understand where you're coming from but it's a bad analogy. Formal proofs are extremely difficult but possible. Immortality is impossible.

▲

hexaga 2 days ago | parent [-]

I don't think it matters, to be quite honest. Absolute tractability isn't relevant to what the analogy illustrates (that reality doesn't bend to whims). Consider:

- Locating water doesn't become more tractable because you are thirsty.

- Popping a balloon doesn't become more tractable because you like the sound.

- Readjusting my seat height doesn't become more tractable because it's uncomfortable.

The specific example I chose was for the purpose of being evocative, but is still precisely correct in providing an example of: presenting a wish for X as evidence of tractability of X is silly.

I object to any argument of the form: "Oh, but this wish is a medium wish and you're talking about a large wish. Totally different."

I hold that my position holds in the presence of small, medium, _or_ large wishes. For any kind of wish you'd like!

▲

guerrilla 2 days ago | parent [-]

Those are all better analogies than the original one you gave, which didn't illustrate your as clearly as they do.

	▲	hexaga a day ago \| parent [-]
		Unavoidable: expecting someone else to do the connection isn't a viable strategy in semi-adversarial conditions so it has to be bound into the local context, which costs clarity: - Escaping death doesn't become more tractable because you don't want to die. This is trivially 'willfully misunderstood', whereas my original framing is more difficult -- you'd need to ignore the parallel with the root level comment, the parallel with the conversation structure thus far, etc. Less clear, but more defensible. It's harder to plausibly say it is something it is not, and harder to plausibly take it to mean a position I don't hold (as I do basically think that requiring formalized proofs is a _practically_ impossible ask). By your own reckoning, you understood it regardless. It did the job. It does demonstrate my original original point though, which is that messages under optimization reflect environmental pressures in addition to their content.

▲

DoctorOetker a day ago | parent | prev [-]

wishes can be converted to incentives, what if the incentives change such that formally verified proofs were rewarded more and informal "proofs" less?