Comment Comment by hn_throwaway_99 No, it's the Lean proof that's correct, it's the natural language one that has the error. parent hn_throwaway_99 25 days ago