6 comments

  • olirex991 minute ago
    Seems like that anyone can now prove math conjecture. Maybe someone already prove some math problem and is not even aware of it.
  • beernet2 hours ago
    On the one-hand side, it&#x27;s really impressive how LLMs drive mathematics forward, and this pace is only accelerating very quickly.<p>At the same time, most of the proofs I&#x27;ve looked at appear super messy and chaotic to me (while still being correct of course, so it doesn&#x27;t matter). LLMs do not care about &quot;elegance&quot; the way human beings do, which is a big advantage. LLMs for mathematics is such a great fit on many levels. Can&#x27;t wait for a significant breakthrough, prove P=NP and all hell breaks loose.
    • hawtads4 minutes ago
      &gt; <i>LLMs do not care about &quot;elegance&quot; the way human beings do, which is a big advantage.</i><p>It&#x27;s just a matter of time before you can post train it for elegance too. Mathematical proofs in particular can be formally verified automatically which is a big advantage.
    • pdonis9 minutes ago
      <i>&gt; most of the proofs I&#x27;ve looked at appear super messy and chaotic to me (while still being correct of course, so it doesn&#x27;t matter)</i><p>How do you know they&#x27;re correct if they&#x27;re super messy and chaotic?
      • _jayhack_2 minutes ago
        formal verifiability e.g. vi Lean
      • KPGv27 minutes ago
        I&#x27;ve driven back roads in Ireland. Super messy and chaotic. I was still able to use a map to get to my destination.
    • dcsommer39 minutes ago
      Sure they care about elegance, or at least brevity. Minimizing tokens out, or generally &quot;token efficiency,&quot; is part of the objective function for these systems. It doesn&#x27;t mean they are perfect at it though.
      • Someone24 minutes ago
        &gt; Minimizing tokens out, or generally &quot;token efficiency,&quot; is part of the objective function for these systems.<p>First time I heard that, and I doubt it. Don’t customers pay for output tokens? If so, why would a company specifically spend time training their LLM to generate fewer?
        • yreg16 minutes ago
          So they can charge more per token and decrease the pressure on their infra.
      • senorrib37 minutes ago
        You clearly haven&#x27;t used Claude to generate code or documentation.
        • nelox32 minutes ago
          &quot;First rule in government spending: why build one when you can have two at twice the price&quot; - S.R. Hadden
          • KPGv26 minutes ago
            Personally, I&#x27;ve found city roads to be more reliable than the private roads where I live.
  • JPLeRouzic11 minutes ago
    Please, what does that mean for Maxwell equations? For electromagnetism?<p>(Wikipedia redirects Maxwell&#x27;s conjecture to Maxwell equations).
    • gjskngnf0 minutes ago
      The Maxwell conjecture is a toy problem. The existence or nonexistence of a bound on the number of equilibrium points in an electrostatic arrangement of point charges doesn’t change much. I say that as an EE but not a specialist in electromagnetism.
    • pdonis6 minutes ago
      <i>&gt; what does that mean for Maxwell equations?</i><p>Nothing. They&#x27;re still just as valid as they were before.<p><i>&gt; For electromagnetism?</i><p>In practical terms, nothing significant. It&#x27;s not going to change how anyone builds devices that use electromagnetism.
  • amelius35 minutes ago
    Ok, who gets the credit?<p>Does this work like a bug bounty program, where OpenAI pays you if you find a nice application for ChatGPT?
    • chorsestudios16 minutes ago
      No but the Clay Mathematics Institute will give you $1,000,000 if you solve one of the 6 remaining Millennium Prize Problems, and if you solve certain Erdos problems you can get $10-10,000.
      • echelon3 minutes ago
        Even if you use AI tools?
        • muglug1 minute ago
          Yes. But you’ll spend more in tokens than you’ll get back from prize money.
  • josefritzishere36 minutes ago
    This is so inelegant I can&#x27;t tell if it&#x27;s accurate or not. ...On the other hand, I can&#x27;t solve it myself.
  • jdc-pub3 hours ago
    Looks like the figures are cut off?
    • smallerize3 hours ago
      The experimental HTML view is messed up, but the actual PDF is fine.