---
title: "수학 경시대회 부등식 문제를 양화사 소거로 컴퓨터에게 풀게 하기"
published: 2025-12-28T23:10:13.000Z
canonical: https://jeff.news/article/1270
---
# 수학 경시대회 부등식 문제를 양화사 소거로 컴퓨터에게 풀게 하기

모델 이론의 양화사 소거(Quantifier Elimination)와 SageMath+QEPCAD를 이용해 경시대회 수준의 다항식 부등식 문제를 자동으로 증명하는 방법을 소개.

- 수학 경시대회에 나오는 인위적인 부등식 문제들을 **양화사 소거(Quantifier Elimination, QE)**라는 모델 이론의 정리로 컴퓨터한테 자동으로 풀게 할 수 있다는 이야기

- 핵심 아이디어: 실수 체(real closed field)에서 양화사가 포함된 논리식(∀x, ∃x)을 양화사 없는 동치 수식으로 변환할 수 있음. 예를 들어 "∃x. ax² + bx + c = 0"은 "b² - 4ac ≥ 0"과 동치인데, 이걸 일반화해서 아무리 복잡한 다변수 부등식도 기계적으로 처리 가능

- 도구는 **SageMath + QEPCAD**. `sage -i qepcad`으로 설치하고, 양화사가 포함된 수식을 넣으면 양화사 없는 동치식을 뱉어줌. 코드가 놀라울 정도로 짧음

- 예제 1: a⁴ + b⁴ = 17일 때 15(a+b) ≥ 17 + 14√(2ab) 증명 — √를 제곱으로 치환해서 다항식으로 만든 뒤 sage에 던지면 끝. 등호 조건이 (1,2)와 (2,1)뿐이라는 것까지 자동으로 확인 가능

- 예제 2: (x + 1/x)(y + 1/y)(z + 1/z) ≥ (x + 1/y)(y + 1/z)(z + 1/x) 증명 — xyz를 양변에 곱해서 다항식으로 만들고 sage에 넣으면 참임이 확인되고, 등호 조건의 기하학적 구조까지 알려줌

- 제한사항은 입력이 다항식 부등식이어야 한다는 것. √나 분수가 있으면 먼저 양변을 곱하거나 제곱해서 다항식 형태로 바꿔야 함

- 글쓴이 왈, MSE(Math StackExchange)에서 이런 문제 보면 "컴퓨터가 해줄 수 있는데"라고 댓글 달고 싶은 충동을 참고 있다가 블로그에 풀었다고 함

## 핵심 포인트

- 실수 체에서 양화사가 포함된 논리식을 동치인 양화사 없는 수식으로 변환 가능
- SageMath + QEPCAD로 몇 줄의 코드만으로 복잡한 부등식 증명
- 등호 조건까지 자동으로 확인 가능
- 입력은 다항식 형태여야 하므로 루트·분수는 사전 변환 필요

## 인사이트

수학의 '핵무기'를 경시대회 문제에 쓰는 유쾌한 오버킬. 연구자라면 이런 도구를 알아두면 시간 절약이 될 것