So the boosters are making a big deal about the dump of “proofs” OpenAI has made recently, so I thought I would collect some relevant links in one place…

Stuff on autoformalization:

And some other related links:

Let me know in the comments if you have any links I should to these lists!

  • Amoeba_Girl
    link
    fedilink
    English
    arrow-up
    11
    ·
    edit-2
    2 days ago

    It’s really fucking me up the way AI boosters and friends are treating mathematics as a natural science whose goal is to uncover mathematical facts in the number mines. I’m not even staunchly opposed to platonism, but my god. That’s not even how natural science works!

    Random idiot on r/singularity

    That stance assumes we still need to fully understand the manual mechanics in order to apply the end result.

    ​Saying we lose out on the “journey” is like an 18th-century laborer complaining that the steam engine will create a society where no one has the endurance to swing a 20-pound hammer for a full 12-hour day.

    Do we lose something through abstraction? Absolutely. And I understand why people would mourn that. But do we need to have the endurance to swing the hammer to build a modern skyscraper?

    We aren’t losing the ability to do math, we are just moving up a layer of abstraction, transitioning from the laborers to the architects.

    Also look out for the new obnoxious metaphor of “what if aliens descended from the sky and handed us their science and proofs, how is this different”. First of all shut up. Secondly we should assume the aliens in this scenario have reason, intent, and the ability to communicate through language. You’re imagining they’re using the scientific method and not divination from wiggling their proboscis in the fourth dimension. Which is quite different from OpenAI’s big dump on scientific practice.

      • scruiserOP
        link
        fedilink
        English
        arrow-up
        8
        ·
        2 days ago

        Someone on Scott Aaronson’s blog suggested math will become an empirical field now, where they run “experiments” by asking AI for lean proofs.

        Scott, is this a turning point where mathematics gets off its well trodden path of logic and becomes more like an empirical science? Heck, people were arguing if math is invented or discovered, this settles it. Math is discovered – by AI! From now on forth, Mathematicians will become scientists, wielding AI as a telescope, pointed towards new and disturbing alien worlds in the Platonic realm.

        So yeah, it seems like this idiotic view is pretty popular among boosters.