5 ms·

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

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

nospice 9mo ago
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?
- rjh29 9mo ago
  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.
  - falseprofit 9mo ago
    Hey, do you mind sharing any of these other forums? I’m trying to make my way up the satire food chain.
- le-mark 9mo ago
  > 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.
  - chroma205 9mo ago
    > Being pompous and self obsessed requires none of those things. Sufficient, but not necessary
DoctorOetker 9mo ago
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
- btilly 9mo ago
  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.
  - DoctorOetker 9mo ago
    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.
    - btilly 9mo ago
      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/machine-assisted-proof-notices.pdf 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.
hexaga 9mo ago
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.
- DoctorOetker 9mo ago
  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 9mo ago
    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 9mo ago
      I understand where you're coming from but it's a bad analogy. Formal proofs are extremely difficult but possible. Immortality is impossible.
      - hexaga 9mo ago
        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!

nospice 9mo ago

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?

rjh29 9mo ago
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.
- falseprofit 9mo ago
  Hey, do you mind sharing any of these other forums? I’m trying to make my way up the satire food chain.
le-mark 9mo ago
> 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.
- chroma205 9mo ago
  > Being pompous and self obsessed requires none of those things. Sufficient, but not necessary

DoctorOetker 9mo ago

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

btilly 9mo ago
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.
- DoctorOetker 9mo ago
  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.
  - btilly 9mo ago
    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/machine-assisted-proof-notices.pdf 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.

hexaga 9mo ago

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.

DoctorOetker 9mo ago
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 9mo ago
  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 9mo ago
    I understand where you're coming from but it's a bad analogy. Formal proofs are extremely difficult but possible. Immortality is impossible.
    - hexaga 9mo ago
      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!