@robinhouston @Diffgeometer1 What I have not seen raised in this current crisis, if people want to call it that, is the issue of whether or not mechanised so-called proofs should be used in the first place.

The reason that, in general and as far as I know, the mathematical community has largely stayed away from tools like Lean is not because they are difficult to use. It is because a Lean program, or any other output produced by these tools, cannot communicate mathematical intent. It is like giving the source code of a video game to a player and asking them to wring what pleasure they can out of reading it. It doesn't matter how well documented or orderly the code is, it is just not the same thing. I am probably preaching to the converted in making this rather clumsy analogy, but still...

Why bother training models to output Lean proofs. It creates a massive representation gap and increasingly alienates and infuriates mathematicians. Why not just output readable proofs written for TeX? Isn't that a big enough representation gap?

Why this obsession with Lean programs? This is the crisis, that mathematicians haven't turned around to the AI community and told them to come back with readable proofs.

So called Lean certificates buy you nothing. They are barely more than a hoax. Oh, you must accept this proof because of this shiny certificate. It is borderline farcical. The last time I looked Lean hash over two thousand issues on GitHub, not all of them cosmetic.

The next thing people will be training models to convert Lean proofs back into TeX. In fact, I bet it is already happening. As I said, borderline farcical.