GPT-5.6이 프롬프트로 볼록 최적화의 30년 공백을 메움 — 148분 만에 convex optimization 격차 해소, Lean 검증 완료

TL;DR: 단 148분 세션에서 OpenAI의 CDC 증명에 쓰인 프롬프트를 모방해 GPT-5.6 Sol Pro가 1996년 이후 막혀 있던 볼록 최적화의 복잡도 격차를 메우는 증명을 제시했고, 그 결과는 Lean으로 형식 검증됐다. 저자는 UC Berkeley IEOR 교수(응용수학 박사)이며 preprint와 Lean repo는 본문 하단에 링크.

📌 무슨 일이 있었나

TL;DR: In a single 148 min session, with a prompt modeled after the one OpenAI used to prove CDC, GPT 5.6 Sol Pro supplied a proof that closed a complexity gap in convex optimization that has existed since 1996. The result was formally verified in Lean. Links to everything and thoughts on AI capabilities are at the bottom of this post.

Disclosure: I am the author of the preprint and Lean repository linked below. I have a PhD in applied mathematics and am a teaching prof in IEOR at UC Berkeley. The result has not yet been peer reviewed.

Following the recent announcement that GPT-5.6 Sol Pro had produced a proof of the Cycle Double Cover Conjecture, I adapted the prompting methodology used in that project to a problem in convex optimization. After 148 minutes of uninterrupted work, GPT-5.6 Sol Pro produced the main argument for a lower bound that I had been unable to prove myself (and a lot of my past work has been proving complexity lower bounds in different settings).

The problem concerns deterministic zeroth-order convex optimization: Let B_d be the Euclidean unit ball in ℝᵈ, and consider all convex, 1-Lipschitz functions f: B_d → ℝ. An algorithm may query any point x ∈ B_d, and receives only the exact real number f(x), no other information (but the algorithm "knows" that f is convex and Lipschitz). The algorithm is otherwise completely unrestricted, and can use unlimited computation and memory. These function-value-only problems arise naturally when an objective is evaluated through a physical experiment or simulator. One can imagine choosing d engineering parameters and observing only the cost returned by the simulation. If evaluations are expensive (think of measuring a physical system), the natural question is how many are fundamentally required. This is formalized as oracle complexity. Specifically, this is the oracle complexity of convex optimization under an exact function value oracle.

Let Q(d, ε) denote the worst-case number of queries required to find

💬 Reddit 디스커션 핵심

프롬프트 구성과 솔의 역할

yes, I did! I basically had 5.6 Sol synthesize existing closely related work and their approaches, the past ideas I had, with OpenAI's prompt that had a lot of the presumably important mechanisms for how exactly the agent should act. Especially from the "results that do not count" section onwards is a lot of input from Sol. A major reason for the added length though is also the nature of the problem; Just the description of the problem and pointing to a couple existing results already put me at a couple pages. With this kind of complexity result what exactly fulfills the specifications of what is needed can be nuanced (so later there is also a lot more of "what doesn't count", and there are two major components to any proof namely the function class to use and the adversarial oracle strategy, about which you then need to prove things with convex geometry machinery, so that all adds to the length). Also, this gap could have in principle been closed from either direction, which also adds a bit (though you can probably read between the lines that I was trying to push much more for a lower-bound, since an algorithm matching order d complexity would have been extremely surprising, since that would mean you can optimize without gradients just as fast as you optimize with them, which would be shocking given that so much practical optimization happens with gradients)

메모리/이전 대화 활용도

Kind of yes and no. In the prompt I basically just throw all reasonable approaches at it, without making a big distinction for what to explore most, and these approaches would all be reasonable for someone who knows the area. Sol helped me with the prompt as well, for which I gave it the CDC prompt, some ideas and specifications, a crystal clear problem description, and then modified things slightly myself after. One thing I do wonder is how much it accessed memory of previous chats, since as mentioned I had worked with 5.5 and 5.4 on this previously, and the main construction is not so different from something I discussed there. But, the function class max of affine functions that worked in the end was also in my prompt, so I'm not totally sure.

🧠 이게 왜 중요한가

• LLM 수학 증명 실용화: 148분이라는 짧은 시간에 기존 박사급 연구자도 못 푼 lower bound를 제시
• 프롬프트 엔지니어링의 힘: OpenAI의 CDC 증명용 프롬프트 구조를 차용 → 동일 계열 문제에서 재현 가능성 시사
• Lean 형식 검증: 사람이 읽기 어려운 증명을 기계적으로 검증 → 신뢰성 보강
• 자율 연구 보조 시대: AI가 "무엇을 시도할지"까지 정하는 단계로 진입, 인간은 "문제 정의 + 검증"에 집중

🔗 출처

• Reddit 원본: /r/math 스레드
• GeekNews: 토픽 #31570

---

본 글은 ICBM2 자동화 시스템으로 발행되었습니다. 발행 시각: 2026-07-19 21:30 KST.