IneqAgent는 LLM 추론과 기호 계산을 결합해 Lean4에서 부등식을 자동으로 증명하는 에이전트 프레임워크다. 레마 단위 몬테카를로 트리 탐색으로 레마 구성, 목표 재구성, 기호 백엔드 선택을 조율하고, SOS·번스타인·연속 차분대입 등 보완적 백엔드로 로컬 증명에 쓸 정확한 증명서를 생성한다. DeepSeek-V4-Flash와 결합했을 때 네 개 벤치마크에서 186개 문제 중 175개(94.09%)를 풀어 평가된 방법 중 최고 성공률을 기록했으며, 같은 LLM 추론 비용 하에서도 Direct Agent보다 높은 성공률과 낮은 평균 비용을 보였다. 이 과정에서 Dittert 추측의 4·5차원 강화형을 Lean으로 검증하고 Holens-Djokovic (4,4) 부등식도 증명해 Merris 추측의 4차원 사례를 함께 입증했다.

• •LLM 추론과 기호 계산(SOS·번스타인 등)을 결합한 Lean4 자동 부등식 증명 에이전트
• •DeepSeek-V4-Flash 적용 시 186개 문제 중 175개(94.09%) 해결로 최고 성공률 기록
• •동일 추론 비용에서 Direct Agent 대비 더 높은 성공률·낮은 평균 비용
• •Dittert 추측 4·5차원 강화형 검증 및 Holens-Djokovic 부등식 증명 등 실제 수학적 성과 도출