Suggestion: Prizes for completing sections of the proof.

Stream: FLT

[zooby]

I see that the grant for this project is one million pounds (or there abouts). There's about 100 nodes in the dependency graph to complete. My idea is to offer £10,000 prize for each node completed. This would surely speed things along a bit? Otherwise what is the money going to be used for?

[Kim Morrison]

It pays Kevin's Imperial salary (or thereabouts) for 5 years, so that he doesn't have teaching and administrative duties, and can work solely on the project.

[Kim Morrison]

Also -- the dependency graph as it exists at the moment is a tiny fraction of what it will become.

[Kevin Buzzard]

Re speeding things up a bit: there's no hurry right now :-) Things will speed up a bit when I have time to work on the project! The money doesn't all go to me by the way, the university top slices 50% of it, so that's 500K already gone :-)

[zooby]

OK. I revise my suggestion to £100 prize and a free t-shirt that says "I completed a FLT node". :blush:

[Patrick Massot]

There is a much more important point you don’t realize: the people who are competent to complete non-trivial nodes do not need a prize to want to do it.

[Rida Hamadani]

This reminded me of San Serriffe's hexadecimal dollars. :smile_cat:

[zooby]

Patrick Massot said:

There is a much more important point you don’t realize: the people who are competent to complete non-trivial nodes do not need a prize to want to do it.

So Kevin, Patrick is saying to prove you're competent you must prove it by giving away the million pounds :grinning_face_with_smiling_eyes:. Happily as a non competent person I will be happy to accept the money :wink:

[Kevin Buzzard]

All other projects have happened in their own time with no monetary rewards. Experience shows that the moment you start paying people to prove theorems, stuff can get quite complicated quite quickly, and I prefer the simple life.

[Kalle Kytölä]

Indeed. Not only is this completely missing how research funding works, but it also bears no relevance to the progress in FLT formalization, which is what the project and this stream are supposed to be about. (Sorry, this is of course evident to basically everyone, and I just got trolled.)

There are of course important issues to resolve (by the scientific community as a whole) regarding incentives for formalization --- particularly related to the recognition and careers of those who make valuable contributions to such projects. By applying for and getting a research grant of this kind for a formalization project, Kevin has obviously made the prospects a lot better for all those who do formalization of mathematics! We don't need people telling him how to manage his research grant, we need others who care about formalization to also do many kinds of things to advance formalization.

[Chris Birkbeck]

Attribution is part of the reward here and that will definitely happen.

[Eric Rodriguez]

I'd love to see some Knuth checks in the Lean community :)

[Kevin Buzzard]

It's OK, Knuth is checking!

---

Hi Kevin,
Thanks for your excellent article about "Mathematical reasoning and
the computer" in the recent BAMS.
You might be interested in an article with a similar title and flavor
that I wrote with Marshall Hall about 60 years ago, when computers
were a bit newer on the scene! Of course the results we could achieve
then are nowhere near as impressive as the recent works that you
describe. But even then, there was a similar pattern: With a computer
we could go a step further than was possible by hand, and then we
were lucky enough to see how to generize the computer's discoveries
to infinitely many larger cases.
The paper appeared in a supplement to the American Mathematical Monthly
volume 72 (February 1965), on pages 21--28 of a separately paged
supplement. That supplement, entitled Computers and Computing,
was number 10 in a series of occasional publications called the
Herbert Ellsworth Slaught Memorial Papers. (It was reprinted, with
an addendum, as Chapter 1 of my Selected Papers on Discrete Mathematics.)
Best regards, Don

[Luigi Massacci]

Out of curiosity, I had heard somewhere that he doesn’t use email any more; is it an urban legend or did you receive that as a letter?

[Kevin Buzzard]

Maybe he doesn't use email any more, but someone else sent me the email with subject "message from Prof Knuth" and I know from previous interactions I've had with Knuth that it's genuine.

[zooby]

Censorship. :mask:

[Yaël Dillies]

Truth is Kevin did originally apply for a bigger grant which was going to cover other people working on the project. But that grant didn't go through

[Oisin McGuinness]

Knuth quoted from @Kevin Buzzard 's post:

The paper appeared in a supplement to the American Mathematical Monthly
volume 72 (February 1965), on pages 21--28 of a separately paged
supplement.

See here on JStor: https://www.jstor.org/stable/2313307

(Knuth replies are fun to get; in the paper days, he once sent back my original note, with marginal entries commenting in very faint pencil, plus the cheque for one issue not previously reported. Some minor correction to his lovely GraphBase book, IIRC...)

[Martin Dvořák]

Patrick Massot said:

There is a much more important point you don’t realize: the people who are competent to complete non-trivial nodes do not need a prize to want to do it.

I'd say people who are already employed in academia don't need any prize money. Bounties might nevertheless give opportunity to some unemployed mathematicians.

The real problem, as pointed out before, is that grant money cannot be spent in unregulated ways.