Hacker News Reader

Comment by almostgotcaught | Hacker News Reader

> You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such.

people on hn love making these kinds of declarative statements (the one you responded to, not yours itself) - "for X just do Y" as a kind of dunk on the implied author they're responding to (as if anyone asked them to begin with). they absolutely always grossly exaggerate/underestimate/misrepresent the relevance/value/efficacy of Y for X. usually these declarative statements briskly follow some other post on the frontpage. i work on GPU/AI/compilers and the number of times i'm compelled to say to people on here "do you have any idea how painful/pointless/unnecessary it is to use Y for X?" is embarrassing (for hn).

i really don't get even get it - no one can see your number of "likes". twitter i get - fb i get - etc but what are even the incentives for making shit up on here.

View on HN

It feels good to be smarter than everyone else. You see your upvotes and that's good enough for an ego boost. Been there, done that.

I wish we were a bit more self-critical about this, but it's a tough problem when what brings the community together in the first place is a sense of superiority: prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right?

HN is frequently fodder for satire on other forums. Nobody thinks HN users have "refined tastes", or even that they are "smart" for that matter.

Hey, do you mind sharing any of these other forums? I’m trying to make my way up the satire food chain.

> prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right?

Being pompous and self obsessed requires none of those things.

> Being pompous and self obsessed requires none of those things.

Sufficient, but not necessary

Do selection dynamics require awareness of incentives? I would think that the incentives merely have to exist, not be known.

On HN, that might be as simple as display sort order -- highly engaging comments bubble up to the top, and being at the top, receive more attention in turn.

The highly fit extremes are -- I think -- always going to be hyper-specialized to exploit the environment. In a way, they tell you more about the environment than whatever their content ostensibly is.

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?

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."

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

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!

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

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.

I don't know why you can't accept that your analogy was bad. Learn from it and move on with your life.

Learn what? I don't agree and you haven't given reasons. I don't write for your personal satisfaction.

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

If enough care about this that can and will do something about it (making formalization easier for the average author), that happens over time. Today there's a gap, and in the figurative tomorrow, said gap shrinks. Who knows what the future holds? I'm not discounting that the situation might change.

Its super easy to change imho: one could make a cryptocurrency, using PoT: Proof of Theorem, as opposed to just proof of stake or proof of work.

What do Bitcoin etc. actually prove in each block? that a nonce was bruteforced until some hash had so many leading zero's? Comparatively speaking, which blockchain would be more convincing as a store of value: one that doesn't substantially attract mathematicians and cryptographers versus one that does attract verifiably correct mathematicians and cryptographers?

Investors would select the formal verification chain as it would actually attract the attention of mathematicians, and mathematicians would be rewarded for the formalization of existing or novel proofs.

We don't need to wait for the magic constellation of the planets 20 years from now nor wait for LLM's etc to do all the heavy lifting (although they will quickly be used by mathematics "miners"), a mere alignment of incentives can do it.

I grossly underestimate the value of the time of highly educated people having to decode the arguments of another expert? Consider all the time saved if for each theorem proof pair, the proof was machine readable, you could let your computer verify the proclaimed proof as a precondition on studying it.

That would save a lot of people a lot of time, and its not random peoples time saved, its highly educated peoples time being saved. That would allow much more novel research to happen with the same amount of expert-years.

If population of planet A would use formal verification, and planet B refuses to, which planet do you predict will evolve faster

You appear to be deliberately ignoring the point.

Currently, in 2025, it is not possible in most fields for a random expert to produce a machine checked proof. The work of everyone in the field coming together to create a machine checked proof is also more work for than for the whole field to learn an important result in the traditional way.

This is a fixable problem. People are working hard on building up a big library of checked proofs, to serve as building blocks. We're working on having LLMs read a paper, and fill out a template for that machine checked proof, to greatly reduce the work. In fields where the libraries are built up, this is invaluable.

But as a general vision of how people should be expected to work? This is more 2035, or maybe 2045, than 2025. That future is visible, but isn't here.

It's interesting that you place it 10 or 20 years from now, given that MetaMath's initial release was... 20 years ago!

So it's not really about the planets not being in the right positions yet.

The roman empire lasted for centuries. If they wanted to do rigorous science, they could have built cars, helicopters, ... But they didn't (in Rome, do as the Romans do).

This is not about the planets not being in the right position, but about Romans in Rome.

Let's see.

I could believe you, an internet stranger. And believe that this problem was effectively solved 20 years ago.

Or I could read Terry Tao's https://terrytao.wordpress.com/wp-content/uploads/2024/03/ma... and believe his experience that creating a machine checkable version of an informal proof currently takes something like 20x the work. And the machine checkable version can't just reference the existing literature, because most of that isn't in machine checkable form either.

I'm going with the guy who is considered one of the greatest living mathematicians. There is an awful lot that goes into creating a machine checkable proof ecosystem, and the file format isn't the hard bit.

20x the work of what? the work of staying vague? there is no upper limit to the "work" savings, why not be 5 times vaguer, then formal verification can be claimed to be 100x more work.

If ultimate readership (over all future) were less than 20 per theorem, or whatever the vagueness factor would be, the current paradigm would be fine.

If ultimate readership (not citation count) were higher than 20 per theorem, its a net societal loss to have the readers guess what the actual proof is, its collectively less effort for the author to formalize the theorem than it would be to have the readers guess the actual proof. As mathematicians both read and author proofs, they would save themselves time, or would be able to move the frontier of mathematics faster. From a taxpayer perspective, we should precondition mathematics funding (not publication) on machine readable proofs, this doesn't mean every mathematician would have to do it, if some hypothetical person had crazy good intuitions, and the rate of results high enough this person could hire people to formalize it for them, to meet the precondition. As long as the results are successfully formalized, this team could continue producing mathematics.

Reply on news.ycombinator.com