Comment by afolkest

Quote from paper worth being aware of:

"Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean."