Human-AI Hybrid Mathematical Discovery Workflow: Unifying Ramanujan's 17 Series for $\boldsymbol{\frac{1}{\pi}}$

Motivation

• Known: CMF는 최근 수학 상수에 대한 공식을 발견하고 조직화하는 데 사용되어 왔으며, 2F1 hypergeometric function에서 생성된 CMF를 통해 여러 세기와 다양한 출처의 π 공식 수백 개를 하나의 family of trajectories로 축약한 바 있다. 그러나 Ramanujan의 17개 공식은 이러한 통합 시도에 저항해 왔다.
• Gap: 브루트포스 탐색으로 Ramanujan 공식들을 생성하는 trajectory를 찾는 것은 탐색 공간의 크기와 평가의 민감성(“거의 정확한” 공식도 틀린 것으로 간주됨) 때문에 계산적으로 불가능하여, 휴리스틱 기반의 human-AI 협업 접근이 필요했다.
• Why: 한 세기 동안 미해결로 남아있던 Ramanujan의 17개 공식에 대한 통합 구조를 발견함으로써 π에 대한 더 효율적인 새로운 공식 발굴 가능성을 열어주며, 동시에 재현 가능하고 검증 가능한 human-AI 수학 연구 workflow의 구체적 사례와 오픈소스 도구를 제공한다는 점에서 중요하다.
• Approach: 저자들은 group의 논문·코드·비공식 노트 등으로 학습된 persistent LLM 기반 agent인 “Ramanujan Agent”를 구축하고, symbolic/numeric 계산 guardrail과 skill.md 파일을 결합한 human-steered iterative discovery loop를 통해 Ramanujan의 17개 공식을 CMF로 통합했다.

Achievement

1. 통합 증명 도출: Ramanujan의 17개 공식 모두가 동일한 4F3(a1,a2,a3,a4;b1,b2,b3;z) generalized hypergeometric generator function으로부터 구성된 CMF의 trajectory로부터 유도됨을 증명했으며, 공식들은 시작점(hypergeometric parameter의 shift), 평가점 z, 초기조건에서만 차이가 남을 보였다.
2. workflow 방법론 제시: 인간의 steering, project-specific context를 갖춘 persistent LLM agent, symbolic/numeric guardrail, skill.md 파일을 결합한 human-AI hybrid 연구 workflow를 제안하고, agent와 skill 파일을 오픈소스로 공개했다.
3. 검증 전략 확립: 각 공식에 대해 CMF 구성과 무관하게 summand로부터 직접 유도한 recurrence와 CMF에서 유도된 결과를 독립적으로 비교하는 검증 전략을 통해 “almost exact이지만 틀린” 결과를 걸러내는 신뢰성 높은 절차를 확립했다.

How

Figure 1. Human-AI discovery loop. A researcher proposes a “hunch”; the agent converts it into symbolic or numeric exper

• 인간 연구자가 문제를 정의하고 후보 구조(“hunch”)를 제안, 결과를 해석하고 유망하지 않은 방향을 배제
• LLM 기반 agent(OpenAI Codex, GPT-5.4 High 기반)가 formula-search 코드 생성, multiprocessing 등 저수준 구현 처리, 요약·그래프 등 사람 친화적 산출물 생성, 단일 공식에서 얻은 proof-of-concept을 17개 전체로 확장
• SymPy 및 custom CMF library인 ramanujantools를 사용한 symbolic computation layer 활용
• skill.md 파일을 통해 수학적/코드베이스 배경지식, 검증 기준, "definition of done"을 계층화하여 agent에 교육
• 매 클레임에 대해 code-level(unit test, 독립적 수치 검증), math-level(edge case 확인, 문헌 인용), review-level(사람이 읽을 수 있는 리포트) 검증을 요구하는 guardrail 설계
• 최종 결과에 대해서는 summand 기반 recurrence와 CMF 기반 결과를 독립적으로 비교하는 추가 수학적 검증 수행

Originality

• 기존의 LLM-symbolic tool 결합 연구(COPRA, Draft-Sketch-Prove, LeanDojo/ReProver, Baldur, AlphaGeometry)와 달리, formal proof assistant가 아닌 human-steered, 경량화된 iterative research workflow를 통해 실제 미해결 수학 문제를 해결
• persistent LLM agent에 project-specific context(논문, 코드, 비공식 노트, 이전 실험)를 skill.md 형태로 계층화하여 교육하는 설계 원칙 제시
• 단순 공식 발견을 넘어, 100년 넘게 미해결이었던 구체적 수학 통합 문제(Ramanujan의 17개 공식)에 대해 CMF라는 기존 프레임워크를 적용해 새로운 elementary proof를 도출
• AI 실패 모드(부분 요약, 암묵적 가정 누락, 그룹 내부 용어 오해)를 체계적으로 문서화하고 이를 검증 메커니즘으로 전환한 점

Limitation & Further Study

• 특정 모델(OpenAI Codex, GPT-5.4 High)에 의존한 사례 연구로, 방법론이 model-agnostic이라 주장하나 다른 모델에서의 재현성이나 일반화 가능성에 대한 정량적 비교가 부족함
• workflow의 효율성이나 시간/비용 절감 효과에 대한 정량적 지표(예: 인간 단독 연구 대비 소요 시간)가 제시되지 않아 human-AI hybrid 접근의 실질적 이득을 판단하기 어려움
• 단일 연구 그룹, 단일 문제(Ramanujan 17 series)에 대한 사례 연구이므로 다른 수학 분야나 다른 연구 그룹에 대한 일반화 가능성 검증이 필요함
• 논문 발췌본에 4F3 CMF의 구체적 수학적 유도나 완전한 증명 세부사항이 제한적으로 제시되어 있어 수학적 엄밀성에 대한 완전한 평가가 어려움
• 향후 연구로 동일 방법론을 다른 π 공식(RISC collection 등) 및 Diophantine approximation 등 다른 실험수학 문제로 확장하는 것이 제안됨

Evaluation

총평: 단순한 AI 활용 사례를 넘어, 100년 넘게 미해결이던 구체적 수학 문제를 human-AI hybrid workflow로 실제 해결한 설득력 있는 사례 연구이며, agent 설계 원칙과 오픈소스 공개는 향후 실험수학 연구에 실질적으로 유용할 것으로 보인다.