Comment by sterlind

Using human language models for math problems is a bad idea for exactly this reason: judging correctness of proofs in English is subjective, whereas proofs in Lean are objective and easy to machine-check. Deepmind's AlphaProof was so remarkable precisely because it spoke Lean, so its proofs were verifiable. Why waste time on anything else?