Thread

1. rahidz · 1789909623 · focus · HN ↗

   Man I remember back when a psychic conned me by solving the Navier-Stokes problem.

   Also >July 4th, 2023

   1. rusk · 1789909904 · focus · HN ↗

      Did an AI do that on its own though? I heard it was human mathematicians using a sophisticated machine as a tool.

      1. mstank · 1789910235 · focus · HN ↗

         It sounds like LLMs were pretty useful to them…

         1. ModernMech · 1789911386 · focus · HN ↗

            So was Lean. Did Lean solve it?

            1. zamadatix · 1789912841 · focus · HN ↗

               Nothing is solved in isolation but credit usually goes to wherever the new work in the paper comes from instead of the whole mountain of previous mathematics or existing tools used. The most relevant of those get referenced and then this reference tree builds a tree of collective base work needed across history.

               1. ModernMech · 1789917541 · focus · HN ↗

                  Usually credit goes to the people wielding the tools, not the tools themselves.

                  1. zamadatix · 1789917654 · focus · HN ↗

                     Usually there has never been a tool which performed the part relevant to getting any credit.

                     E.g. in the first famous computer assisted proof (of the four color theorem) the computer only executed the resulting calculations defined from the new logic, it did not have part in the work needed to show those calculations could answer the problem nor did it come up with the actual calculations to do.

Unofficial Hacker News client; not affiliated with Y Combinator.