11 ms·

What would it cost to make a team of mathematicians do the same?

• dist-epoch 12d ago
  More importantly how many years it would take.
• nearbuy 12d ago
  The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.
• margorczynski 12d ago
  Buzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.
  • jascination 12d ago
    1kk? Why not say 1M?
    • emil-lp 12d ago
      You mean why not say £ 1MM?
  • traes 12d ago
    It's true that his goal was not the full thing, but it was also not merely a Lean verified proof. From the blog post linked in the toptext: > The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof.
  • VLM 11d ago
    Not a similar comparison in that one project was to produce a plan to extend the limits and goals of mathematics in general while in the process of answering "Is it true, circle yes or no". The other project circled "yes" but the output is not ... progress toward goals oriented. Its like using AI to do your homework in the middle of a class. Yes, in the short term, that solves the problem of completing your homework. But it creates an entirely new problem of if you never did the homework how do you intend to pass the rest of the class or the remainder of college curriculum? A lot of cheaters ... don't. A project has a long term path for permanent progress across an entire field. An oracle answers a question, sometimes cryptically, then progress in the field permanently ceases. The value of a research project to determine if a Turing Machine halts with a T or a F on the tape is, to some extent, did it get a T or an F on the tape, but much more so the value is the tendrils of the rest of the field of mathematics pushing into the project at the start and then pushing out to enrich the rest of the field of mathematics at the end. On the other hand if you have a project to run that Turing machine and see if it ever halts with a T or F as the proof, the result is completely sterile and WRT advancement of the rest of the field the actual result is kinda irrelevant. No postdoc is going to take the skills learned and move on to a position somewhere else and apply those new skills toward advancing something else in the field or describing a new goal or new way to look at the world. We'll get a popular science article about "oh it turns out the answer is indeed 'T'" and thats it. Sterile. Personally I always thought the theorem proving turing machine would indeed terminate with a "T" and indeed it did. That's nice, and I bet the result settled a lot of bar bets. Aside from that, it will have minimal impact on progress in the field compared to the human project that's actually advancing the field. Possibly people will be able to parse the 13 million lines of whatever into useful progress elsewhere in the field, possibly not. It'll be hard to get funding for it. OTOH its early days. Might end up useful in the end.
• well_ackshually 12d ago
  1 million dollars reinvested in the economy by a bunch of math nerds that need to buy food, get housing, pay for services, or 300k in Anthropic's pocket? I wonder which one makes society better off, hmmmm, very complicated question, nobody can answer that.
  • cindyllm 12d ago
    [dead]