yesnoerror releases AutoformBot, a multi-agent system that translated 26 graduate math textbooks into Lean 4

Very interesting work here! Lots of rough edges (misformalizations, etc) but it points the way to a landscape of possibility! What will be really interesting is to see if it's possible to actually teach out of such books (and of course clean things up as you go)... [It's possible that the AI took so many shortcuts that it really doesn't represent the difficulty of some proof, etc; still, experiments like these can give a lot of useful information.]