I think an under appreciated part of mathematics has been contributing clean and elegant work precisely so that others could use that as a foundation for further work and new insights. This dump from Open AI seems to be the opposite. Huge and messy, incomprehensible and taken seriously only because of Lean.

There is this assumption that AI will contribute to faster progress in math but given the garbage dump of proofs which we have to take on faith are robust I wonder if the opposite is true.

My reservation could only be dismissed if AI turns out to be able to contribute fundamental new insights and pose new problems. This takes us into an area where AI progress has been slow to say the least.