Luckily for these guys the problem is famous enough that giving some kind of credit for its resolution even makes sense at all. The vast majority of published work is not like this. There’s not going to be any credit divvied up to the thousands of people who’s work was probably involved in the recent formalization of FLT, which involved formalizing 300 thousand theorems.
What's this obsession with credit. From elsewhere in the thread:
> people spending their lives trying to promote humanity
What does this even mean? Become a monk? They are credited with helping humanity.
Kevin Buzzard has reportedly been working on a more systematized (i.e. leveraging a more modern approach) and human-targeted formalization of FLT. I certainly hope that his work continues and he gets the deserved credit. Of course there is also some possibility that it won't, and that would mean you have a point after all.