>「何か足りないが、何かを足せば Lean化可能」
abc予想は正しいという公理を足せばLean化可能