alt Hacker NewsI don't understand what you're saying. Writing lean doesn't make it easier to formulate a proof. These LLMs are writing natural language proofs then formalizing after the NL proof is done. If humans were theorizing and exploring open problems in lean for the last 15 years, we'd be moving much slower than we have been with natural language.
Funnily NL is indeed different from formal language and does different in a way that makes a difference: https://www.scientificamerican.com/article/openais-blockbust...