28
Lean and Autoformalization: some helpful links (awful.systems)
submitted 1 week ago by to c/techtakes@awful.systems
17 comments fedilink hide all child comments
 

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!

you are viewing a single comment's thread
view the rest of the comments
[–] 8 points 1 week ago (4 children)

I have looked at a few comment threads about the math proofs on Hacker News. I only got as far as business calculus about 30 years ago, so some of it was beyond me.

I noticed that some commenters have no problem with the fact that a lot of the proofs are almost incomprehensible to humans. I do not see the point of math for AI alone, since I do not think AI is or will ever be conscious.

It is another example of people thinking that our lives should be not just pro-AI, but AI-centric. To them, the AI is not here for us, but we are here to serve the AI.

  • permalink
  • fedilink
  • source
  • hideshow 4 child comments
    •
  • [–] [S] 8 points 1 week ago (3 children)

    I do not see the point of math for AI alone, since I do not think AI is or will ever be conscious.

    Rationalists (and in general those with fear/hope or a technological singularity) have the idea that once the AI is smart enough, it will be able to recursively self-improve in an exponential process. Vibe-coding hasn't made this come true, so they are trying to make it happen by shoving enough of the right sort of knowledge into the AI. Obviously being smart and being mathey go together, so if the AI just gets good enough at math, surely bootstrapping to godhood is just around the corner!

    To them, the AI is not here for us, but we are here to serve the AI.

    The techbros are giving mathematicians the humanities treatment. (I.e. they don't respect the entire profession despite its immense importance to actually understanding reality.) Before, mathematics had sort of gotten half a pass for being rigorous and adjacent to stuff techbros do respect, like computer science. But, given just half a whiff of the idea that they may no longer need human mathematicians, they are ready to accept utter slop...

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 3 child comments
    •
  • [–] 8 points 1 week ago (2 children)

    I’m not convinced that techbros respect computer science either. The bit that says ‘computer’ gives them an air of intellect and elitism by proximity, but it’s not actually a field they care to practise.

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 2 child comments
    •
  • [–] [S] 6 points 1 week ago (1 child)

    True, but its a different form of disrespect, where they outwardly steal the style and aesthetics of the discipline to try to claim its legitimacy. Like the endless "whitepapers" pumped out by cryptobros.

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 1 child comment
    •