As far (though little) as I know, that's way beyond feasible still -- lean has a ton I think, but is nowhere near covering the "seam" of mathematics -- many fu

As far (though little) as I know, that's way beyond feasible still -- lean has a ton I think, but is nowhere near covering the "seam" of mathematics -- many fundamental objects are not even defined themselves yet, so you'd have to do lots of extra work there, not to mention all the work to define your own new things. Lean is amazing (and I played around with it a bit, should do so more) but I don't suspect it's realistic to expect new theorems of this magnitude to be written in it at this point yet, doing so is a huge huge effort on top of the life-altering effort that the theorem itself requires.