Almost certainly the Lean proof needs to be decoded for humans and probably also made “human intelligible”. Now maybe LLMs can also simplify arguments and make

Almost certainly the Lean proof needs to be decoded for humans and probably also made “human intelligible”. Now maybe LLMs can also simplify arguments and make sense of them for humans, but we haven’t seen that yet (unaided). (I haven’t looked at it, personally.)