Computer checked math proof has been around for quite some time, but it wasn’t considered to be up to task of checking current math research. So Peter Scholze challenged people to check a theorem he just proved. (Also because he was worried maybe he made a mistake.) After six months, it is now checked. To quote:

I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement.

It is a landmark achievement, because many thought you plain can’t do that, because infrastructure is not in place and prerequisite background knowledge is not there.

Could anyone explain this to me like I‘m a five year old? :D Thank you!

Computer checked math proof has been around for quite some time, but it wasn’t considered to be up to task of checking current math research. So Peter Scholze challenged people to check a theorem he just proved. (Also because he was worried maybe he made a mistake.) After six months, it is now checked. To quote:

It is a landmark achievement, because many thought you plain can’t do that, because infrastructure is not in place and prerequisite background knowledge is not there.