Cornell Researcher Views Lean LLM Issues as Temporary

Alexander Terenin, Assistant Research Professor at Cornell who specializes in Bayesian models, Gaussian processes, and decision-making under uncertainty, posted that any LLM success exploiting a subtle Lean bug represents a fundamentally short-term problem. He stated that sufficiently developed future versions of Lean will contain no bugs. The only remaining failure mode, he wrote, will be stating one thing while formalizing another.