> it wrote 13 million lines of Lean

Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?

I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.

I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the Lean libraries.

My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!

Formalisation of the classification of finite simple groups must be on someone’s ‘moonshot’ list.

Ok, let’s get a rabid pack of agents cranking on P = NP? next!

I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.

Anyone know of a good Lean tutorial? I've played around with it a bit but never really learned it properly.

I think Anthropic might the frontier lab hiring contractors through data vendors to formalize mathematical textbooks for them at a rate of 170-200 dollars per hour. This was mainly through Alignerr which has the worst reputation for not paying their contractors. They have been hiring since February as far as I can recall. This is in addition to all the internal people they might have working on this. If they have been formalizing all this work for the past 9 months before having Claude use all this data needed to formalize FLT, then it wouldn't be Claude formalizing FLT in just 11 days. Same with the upcoming results they will claim Claude came up with, but in fact they have been hiring frontier researchers working on very niche topics through Micro1. It's all a marketing ploy before their IPO.