That paper seems to just be saying that people's benchmarks are bad. Like, yeah, obviously don't consider the problem solved if the bot used sorry or axiom. This is trivial to check for and consider a compile error. It's (literally) the same as just not allowing throwing exceptions in a program. And vacuous statements aren't actually a problem. And they claim that sometimes it makes mistakes formalizing an informal statement, but that this becomes noticeable when you try to actually prove it. This is like if it forgot a parameter when it was defining a function prototype. When it actually goes to write the function, it realizes it needed some extra information, so it'll just add it. So, again, what's the problem? This isn't the type of error that can go uncaught because it won't be able to proceed with the actual proof unless it's actually true, in which case, great, it proved a stronger statement than was asked for.

A robot may not injure a human being is not a formal statement, so it doesn't even make sense to talk about here. Maybe it decides to name `Manifold` (the concept) `HumanFinalSolution`, whatever. As long as a `HumanFinalSolution` has the same formal properties as a manifold, I can still talk about the Poincaré conjecture. For formal statements, there's a compiler. Use it. It's like if I'm writing a program and I don't want it to use null, I do `-Wnull -Werror` or whatever. The task isn't done until the build is successful. I don't have to read through all the code to make sure that it didn't do null pointer dereferences or casts because the compiler doesn't allow it.

You can literally give e.g. codex a linear algebra text like Axler and a Lean setup and ask it to formalize it without using any external libraries. Do it all from scratch. I've found it'll generally be verbose, and it might e.g. use Classical.choose where it could be avoided with more work, so it doesn't prove the absolute strongest version of a theorem (which is typical for normal math exposition too), but I haven't observed it to make any of these sorts of mistakes.

After you make all your basic definitions, you can ask it to do something like solve an actual system of linear equations with a formal proof. If all of your definitions were correct, it can easily do this with a short proof from the theory. You can even give it a couple axioms from calculus, like that some functions called sine and cosine exist or whatever, along with their derivative rules, and linearity of derivatives, chain rule, etc. without actually defining what real numbers and derivatives are, and it can likewise use that to solve linear differential equations with proofs the way a high school student that memorized all of these facts would.

I actually see this as a potentially super powerful technique for teaching because you can be explicit about what did you actually prove in class versus what was a fact that I told you and maybe pictorially or otherwise hand-wavy justified, and then proceed formally from there. I think there's a lot of potential to push logic and proof assistants down to lower levels of education.