331
OpenAI Is Pissing Off a Bunch of Mathematicians—Again (www.wired.com)
submitted 1 week ago by to c/technology@lemmy.world
88 comments fedilink hide all child comments
you are viewing a single comment's thread
view the rest of the comments
[–] 25 points 1 week ago (3 children)

Also all ML models have some accuracy less than 100%, that means you can’t trust it. The whole point in the proof is perfection

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

    The proofs are written in Lean so, like in all mathematics, you don't have to trust the person because you can independently verify the proof.

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 1 child comment
    •
  • [–] 4 points 1 week ago

    That's not how Lean works.

    1. implementation of Lean is buggy.
    2. having a Lean Theorem/Proof only proves they are connected to the axioms
    3. Lean is not enough to personally verify the proof. We can see that even now with the stolen C+D Navier proof, where OpenAi paper - as we know since yesterday - is... possibly false (well, we know that the lean code does not match the paper, let the mathematicians cook).
  • permalink
  • fedilink
  • source
  • parent