Mathematics · Computer Science · Machine Learning · Verified Research Workflows

AI-Assisted Research

ICML 2026 AI4Research 워크숍의 논문군을 바탕으로 연구 워크플로, 수학적 증명·형식화, 반례·감사, 인간–AI 수학적 발견, 연구문제 정의, AutoML·과학·공학 자동화, 실패지식, 연구 산출물, 안전·거버넌스를 하나의 연구 지형으로 재구성한다.

Central Thesis

답변 생성기에서 검증 가능한 연구 시스템으로

가장 뛰어난 연구 에이전트는 가장 많은 정리와 아이디어를 생성하는 시스템이 아니라, 자신의 주장을 반례와 실행결과로 공격하고 인간이 의미와 책임을 판단할 수 있도록 증거와 과정을 남기는 시스템이다.

Research Scope

38공식 채택 논문

6핵심 연구축

15통합 연구질문

15미래 연구방향

검토 범위와 분석 원칙

공식 워크숍 페이지, 포스터 배정표, OpenReview와 공개 메타데이터를 교차 검토하고 연구축 중심으로 종합한다.

Coverage

전체 논문군

Research workflow, proof, formalization, auditing, ideation, AutoML, scientific discovery, safety를 포함한다.

Method

주제 중심 재구성

논문 제목 나열보다 claim–evidence 구조, verification ladder, human ownership, negative knowledge의 공통원리를 분석한다.

Caveat

재현성 유의

워크숍 연구는 초기 결과를 포함하므로 수치·주장은 독립 재현과 후속 검증이 필요하다.

전체 연구 지형

AI4Research는 생성량이 아니라 문제정의, 검증, 재현성, provenance와 인간 연구자의 과학적 소유권을 중심에 둔다.

연구 워크플로The Agentic ResearcherAgent-Native ArtifactsAtelierQUIT

증명·형식화CRC-DeriveBRIDGELean HarnessLibrary Before Proof

수학적 발견Ramanujan WorkflowCounting CyclesPeppyConvex Analysis

문제정의·지식LacunaPaperGymKnowledge MetabolismGoodPoint

AutoML·과학AIBuildAIAutoCircuitCausal AI ScientistJAXBench

실패·안전·집단추론Negative KnowledgeInteraction TaxAlphaApolloClaudini

연구질문→문제 분해→가설·정리·실험→ 코드·수치·문헌·증명도구→반례·오류 검사→인간 판단→재현 가능한 산출물

Definition

AI 연구시스템을 연구 워크플로, 연구 에이전트, harness, verification ladder, negative knowledge, human ownership의 결합으로 정의한다.

Research Workflow

AI 보조 연구 워크플로

인간, agent, 도구, verifier, memory, artifact가 순환적으로 상호작용한다.

Research Agent

연구 에이전트

현재 연구상태, 가설, 증거, 반례, 실패, 예산을 바탕으로 다음 연구행동을 선택한다.

Agentic Research

에이전틱 연구

코드·검색·증명·수치실험을 반복하며 연구상태를 갱신한다.

Research Artifact

Agent-Native Research Artifact

논리, trace, evidence를 구조화해 최종 PDF 밖의 연구과정을 보존한다.

Research Harness

연구 하니스

시스템 규칙, 도구, 상태, recovery, verifier, budget, 종료조건을 포함한다.

Verification

검증 계층

Plausibility에서 formal proof와 independent expert review까지 위험도에 따라 조합한다.

Negative Knowledge

실패지식

실패한 접근, 조건, 원인, 증거, 범위, 재사용 가능한 교훈을 구조화한다.

Human Ownership

인간 소유 연구

문제 선택, 가정, 검증기, 결과채택, 공개, 위험판단은 인간이 통제한다.

Research State

지속 연구상태

가설, 증거, 가정, 반례, 실패, 미해결 간극을 프로젝트 메모리로 유지한다.

Research workflow: W = (Human, Agents, Tools, Verifiers, Memory, Artifacts) Research state: St = (Hypotheses, Evidence, Assumptions, Counterexamples, Failures, Gaps) Agent action: at ~ πθ(a | q, St, Mt, Tools, Budget)

Problem Definition

핵심 문제는 그럴듯한 국소 결과를 검증 가능하고 재현 가능하며 실제 연구진전에 기여하는 지식으로 전환하는 것이다.

Problem A

Ideation–Execution Gap

참신해 보이는 아이디어가 구현과 실험 이후 장점을 잃을 수 있다.

Problem B

Generation–Verification Gap

생성속도가 검증속도를 앞서면 검증부채가 증가한다.

Problem C

Informal–Formal Gap

비형식 수학의 접근성과 형식증명의 엄밀성을 함께 확보해야 한다.

Problem D

Cross-Artifact Consistency

코드, 명세, 정리, 증명이 동일한 의미를 표현하는지 보장하기 어렵다.

Problem E

Proxy–True Objective Gap

싸고 빠른 proxy 평가가 최종 연구가치와 다를 수 있다.

Problem F

Task Formulation Uncertainty

무엇을 최적화할지, 어떤 문제를 먼저 풀지 자체가 불확실하다.

Problem G

Model–Harness Confounding

향상이 모델에서 왔는지 도구·prompt·search loop에서 왔는지 구분하기 어렵다.

Problem H

Scientific Knowledge Lifecycle

주장은 지지, 수정, 반증, 철회될 수 있으며 downstream 결과도 함께 갱신되어야 한다.

Research utility: U = α Novelty + β Correctness + γ Reproducibility + δ Human Utility − λ Cost − μ Error Risk − ρ Dual-Use Risk Claim requirement: For every claim ci, there exists evidence ei such that ei supports ci.

Core Concepts

분해, 도구보조 추론, persistent context, counterexample-first verification, conformal control, proof graph, adaptive fidelity가 핵심이다.

Decomposition

정의, 문헌, 가설, 코드, 반례, 증명, 감사, 인간판단을 독립 검증단위로 나눈다.

Tool-Augmented Reasoning

LLM 내부 추론을 코드, 수치계산, 기호대수, 문헌검색, proof assistant로 외부화한다.

Persistent Project Context

표기, 가설, 검증된 정리, 실패, 코드위치, 평가기준을 프로젝트 메모리로 유지한다.

Counterexample-First Verification

증명 전에 반례 탐색을 수행해 잘못된 주장을 조기에 제거한다.

Conformal Risk Control

검증기 threshold를 calibration해 잘못된 결과 수용위험을 통계적으로 제어한다.

Proof Dependency Graph

정의·보조정리·정리 사이 의존성을 그래프로 표현해 국소·전역 오류를 분리한다.

Adaptive Fidelity

초기 탐색에는 저비용 검증, 유망 후보에는 강한 검증을 적용한다.

Negative Knowledge Memory

실패한 접근을 적용범위와 증거를 가진 재사용 가능한 지식으로 변환한다.

Information Topology

멀티에이전트는 전체 해답보다 근거·반례를 제한적으로 공유할 때 다양성을 유지한다.

Knowledge Activation

정답 제공보다 좋은 질문과 구조화된 비평이 잠재지식을 활성화할 수 있다.

Research Provenance

주장마다 human, agent, model, prompt, tool, data, execution, verification을 연결한다.

Introduction

AI 연구 활용은 대화형 보조에서 도구보조 추론, 연구 워크플로, 재현 가능한 시스템, 과학적 운영체계로 발전한다.

Stage 1

대화형 보조

설명, 번역, 브레인스토밍, 문장 교정.

Stage 2

도구 보조 추론

Python, 수치실험, 기호계산, 문헌검색, 데이터 분석.

Stage 3

연구 워크플로 에이전트

문제분해, 장기메모리, 다중도구, 실패복구, 반복검증.

Stage 4

재현 가능한 연구 시스템

환경, 의사결정, artifact lineage, claim–evidence 연결.

Stage 5

과학적 운영체계

문제발견, 포트폴리오 배분, 사람–AI 역할, 지식철회 관리.

Motivation and Background

유창성의 한계, 검증부채, 인간 방향설정, 암묵지 손실, 문제정의, 지식 변화가 새로운 연구시스템을 요구한다.

유창성 ≠ 정확성

그럴듯한 정리·증명·인용은 가정, 계산, novelty, 반례를 보장하지 않는다.

검증부채

생성된 주장 수가 검증된 주장 수보다 빠르게 증가하면 연구위험이 커진다.

인간의 방향설정

AI는 넓은 탐색과 계산에 강하지만 문제선택과 의미판단은 인간이 담당한다.

연구과정의 암묵지 손실

실패실험, 폐기된 가설, parameter 선택 이유, 반례가 최종논문에서 사라진다.

문제정의의 병목

실제 연구가치는 목표함수 최적화보다 어떤 문제를 선택하고 정식화하는지에서 발생한다.

변화하는 과학지식

새로운 증거와 철회에 따라 모델 memory와 downstream 결과를 수정해야 한다.

Challenges

환각, 숨은 가정, semantic drift, verifier 한계, proxy gaming, 상태관리, 다양성 붕괴, 재현성, dual-use가 핵심 난제다.

도전과제	핵심 문제	요구되는 방향
환각된 주장과 인용	존재하지 않는 정리·논문·실험결과 생성	외부 검색, citation verification, executable evidence
숨은 가정	증명 중 암묵적으로 조건 추가	Assumption ledger, dependency audit
의미적 Drift	코드·명세·정리·설명이 서로 달라짐	Cross-artifact consistency checks
정리 약화	증명을 쉽게 만들기 위해 원래 정리 변형	Statement hash, semantic equivalence audit
Verifier 불완전성	검증기도 오류와 coverage 한계를 가짐	Verifier ensemble, calibration, human escalation
Proxy Gaming	에이전트가 싼 평가의 허점을 최적화	Adaptive external proxy
장기 상태관리	이전 가설·실패·증거를 잃음	Persistent research state
다양성 붕괴	전체 해답 공유 뒤 아이디어 수렴	Independent generation, selective communication
연구문제 오염	사전학습·검색 문헌에 답이 이미 존재	Temporal split, seed exposure audit
재현성	모델·prompt·도구 버전이 변함	Sealed artifact, environment capture
인간 인지부하	생성 결과가 검토능력보다 빠르게 증가	Risk-ranked review
평가 불일치	Benchmark 성공이 실제 연구기여와 다름	Execution and expert validation
지식철회	모델이 오래된 주장을 반복	Claim-level revision and unlearning
연구 기여도	인간과 AI 기여를 구분하기 어려움	Contribution provenance
Dual-Use	공격·악용 연구도 자동화 가능	Gated tools, risk review, controlled disclosure

Research Questions

최소요건, 연구진전, novelty, verification budget, formalization, artifact consistency, failure memory, human–AI synergy를 중심으로 정리된다.

RQ1

AI 연구 에이전트의 최소 요건은 무엇인가?

RQ2

Benchmark 점수 대신 실제 연구진전을 어떻게 측정할 것인가?

RQ3

연구 아이디어의 novelty를 어떻게 검증할 것인가?

RQ4

주장별 검증수준과 예산을 어떻게 배분할 것인가?

RQ5

비형식 추론에서 형식추론으로 언제 전환해야 하는가?

RQ6

코드·데이터·수식·증명을 어떻게 동기화할 것인가?

RQ7

실패한 연구시도를 어떻게 재사용할 것인가?

RQ8

멀티에이전트는 무엇을 언제 공유해야 하는가?

RQ9

탐색단계와 확인단계의 proxy fidelity를 자동 조절할 수 있는가?

RQ10

모델과 harness의 기여를 어떻게 분리할 것인가?

RQ11

연구문제 자체를 생성하고 미래가치를 평가할 수 있는가?

RQ12

과학주장의 수정과 철회를 downstream 결과에 전파할 수 있는가?

RQ13

인간–AI 협업의 증폭효과를 어떻게 측정할 것인가?

RQ14

AI가 발견한 위험한 연구결과를 어떻게 관리할 것인가?

RQ15

한 분야의 연구 워크플로가 다른 분야로 전이되는가?

Approaches / Methods

대표 논문을 워크플로, 검증·형식화, 수학적 발견, 문제정의·비평, AutoML·과학, 실패·안전 기준으로 필터링해 탐색할 수 있다.

Workflow

The Agentic Researcher

Sandboxed coding agent, persistent project context, 장기 연구세션을 결합한다.

Artifact

Agent-Native Research Artifacts

Logic–Trace–Evidence와 cryptographic seal로 연구과정을 구조화한다.

Human-Owned

Atelier

Human principal, manager, bounded worker·critic, durable Markdown 기록을 사용한다.

Process

QUIT

Query–Understand–Implement–Tell 단계별 artifact와 recovery를 분리한다.

Evaluation

Reasoning Is More Than the Model

Model, harness, benchmark, scorer, budget, trajectory를 분리해 평가한다.

Audit

Agent-Based Auditing

Definition–lemma–theorem dependency graph로 국소·전역 proof 오류를 탐지한다.

Risk Control

CRC-Derive

Calibration으로 잘못된 수학결과 수용위험을 통계적으로 제어한다.

Counterexample

CRAFT

True/false/uncertain 분류 뒤 실행 가능한 반례로 정리를 수정한다.

Synthesis

BRIDGE

코드, specification, theorem/proof 생성과 cross-artifact consistency를 결합한다.

Lean

Auditable Lean Harness

Prompt hash, transcript, Lean source, compile log, escape-hatch 검사를 보존한다.

Library

Library Before Proof

Compile 가능한 proof를 넘어 읽고 수정하고 재사용할 수 있는 formal library를 구축한다.

Discovery

Ramanujan Hybrid Workflow

인간 방향설정, persistent agent, symbolic·numeric guardrail로 통합적 증명을 발견한다.

Combinatorics

Counting Cycles with AI

인간 전략과 AI 조합계산을 결합해 일반 공식을 도출한다.

Optimization

Peppy

수치적 convergence certificate를 analytic Lyapunov proof로 변환한다.

Proof Simplification

Finding Simple Proofs

복잡한 dual certificate를 sparse 핵심 구조로 단순화한다.

Statistics

Mathematical Statistics Workflow

AI 아이디어를 인간이 오류수정·문헌검증해 최종 proof로 전환한다.

Research Map

Lacuna

논문, 개념, 연구방향, 문제제안을 연결해 연구공간의 빈 영역을 지도화한다.

Future Prediction

Continuous Knowledge Metabolism

Sliding window 지식상태와 미래문헌을 이용해 가설의 시간적 유효성을 평가한다.

Ideation

PaperGym

Read, grep, synthesize를 결합한 cross-domain 연구 아이디어 환경을 구축한다.

Review

GoodPoint

저자 반응의 validity와 actionability로 좋은 연구비평을 정의한다.

Task Discovery

Open-Ended Task Discovery

Generate–Select–Refine Bayesian optimization으로 문제생성과 최적화를 공동수행한다.

AutoML

AIBuildAI

ML pipeline 설계와 실험을 agentic workflow로 자동화한다.

Proxy

Adaptive Proxy Evaluation

탐색단계에 따라 평가 fidelity를 높여 proxy gaming을 줄인다.

Circuit

AutoCircuit

LLM, Bayesian optimization, evolutionary search, 회로도구를 조정한다.

Causal

Causal AI Scientist

인과결정트리, 방법선택, assumption diagnostic, self-correction을 결합한다.

QUBO

QuantumQUBO Agent

자연어 문제를 변수, 목적, 제약, penalty, test case로 분해한다.

Kernel

JAXBench

TPU Pallas kernel의 correctness와 speedup을 반복 agent 최적화로 평가한다.

Failure Memory

Negative Knowledge

실패한 접근을 typed record로 저장하고 후속 에이전트가 채택·거부 근거를 명시한다.

Multi-Agent

The Interaction Tax

전체 해답 공유가 아이디어 다양성을 빠르게 붕괴시킬 수 있음을 분석한다.

Self-Improve

AlphaApollo

Propose–Judge–Update, tool verification, 장기 memory, RL, multi-round evolution을 결합한다.

Dual-Use

Claudini

자율 연구가 adversarial attack 발견도 가속할 수 있음을 보여준다.

Unlearning

Scientific Claim Unlearning

오래된 과학주장의 표면 억제가 아닌 구조적 제거와 갱신 문제를 다룬다.

대표 연구	핵심 설계	연구적 의미
Agent-Native Research Artifacts	Logic–Trace–Evidence, compiler, cryptographic seal	논문을 정적 문서에서 감사 가능한 연구객체로 확장
CRC-Derive	Conformal calibration 기반 승인 threshold	수학 검증을 0/1 판단에서 위험제어 문제로 전환
CRAFT	Counterexample-first theorem repair	증명보다 조기 반증을 우선하는 검증전략
Ramanujan Workflow	인간 방향설정 + persistent agent + symbolic·numeric guardrail	인간 통찰과 AI 탐색의 상보성
Lacuna	문헌–개념–방향–문제제안 연구지도	연구 자동화의 핵심을 문제정의로 확장
Adaptive Proxy Evaluation	탐색단계에 따른 fidelity 증가	AutoML의 proxy–true objective gap 완화
Negative Knowledge	Failure record의 조건·근거·범위 구조화	실패를 재현성 있는 공동 연구자원으로 전환
Interaction Tax	Independent proposals vs full-solution sharing	멀티에이전트 성능의 핵심이 정보 topology임을 제시

Key Applications

수학적 발견, 증명 감사, 형식수학, AutoML, 문제정의, 인과추론, 과학 데이터 큐레이션, 하드웨어·회로 최적화로 확장된다.

수학적 발견

조합론 공식, 급수 통합구조, 수렴증명, convex analysis, symbolic calculation.

증명 감사·형식수학

Dependency audit, Lean·Rocq formalization, statement preservation, proof repair.

머신러닝 연구 자동화

Pipeline 구축, hyperparameter tuning, 알고리즘 탐색, adaptive evaluation.

연구문제 정의

Research map, lacuna 탐지, cross-domain transfer, open-ended task discovery.

인과추론

Method selection, identification assumption, diagnostic, causal estimation.

과학 데이터 큐레이션

이질적 catalog 통합, column mapping, method 분류, bibliographic validation.

하드웨어·회로·양자

TPU kernel, analog circuit, QUBO formulation, 다목적 최적화.

연구 비평·동료평가

Validity, actionability, proof audit, claim–evidence mismatch 탐지.

Open Problems

완전 검증된 발견, formalization 확장성, novelty, claim lifecycle, verifier independence, 재현성, dual-use, 실제 연구영향이 미해결이다.

완전 검증된 발견

새 정리 발견부터 formal proof와 library까지 자율 구축하는 능력은 제한적이다.

형식화의 확장성

최근 연구수학을 formal system으로 옮기려면 방대한 선행 library가 필요하다.

Novelty 검증

검색되지 않는 결과가 실제로 새로운지 판정하기 어렵다.

Claim Lifecycle

생성, 지지, 수정, 반증, 철회와 downstream 영향을 추적하는 표준이 없다.

독립 Verifier Ecology

동일 모델이 생성과 검증을 모두 수행하면 오류가 상관될 수 있다.

Proxy Validity

저비용 proxy가 실제 최종 연구가치를 얼마나 예측하는지 정량화해야 한다.

장기 연구상태 관리

수일·수개월 프로젝트에서 모델·도구·가설·artifact를 일관되게 유지해야 한다.

Negative Knowledge Governance

실패지식이 탐색을 돕는지 새로운 가능성을 차단하는지 평가해야 한다.

멀티에이전트 다양성

독립성, 정보공유, 합의 사이의 최적 통신구조가 확립되지 않았다.

Benchmark Contamination

연구문제나 유사 해답이 사전학습 데이터에 포함되었는지 확인하기 어렵다.

인간의 검증부담

AI 생성속도가 증가할수록 전문가 검토시간이 새로운 병목이 된다.

저자성과 기여도

아이디어, 실험, 코드, 검증에서 인간과 AI의 기여를 표준화해야 한다.

모델 업데이트 재현성

동일 prompt와 workflow도 checkpoint가 바뀌면 다른 결과를 낸다.

Dual-Use 안전

자동 연구시스템이 공격기술과 위험한 최적화목표를 발견할 수 있다.

실제 연구영향 평가

Benchmark 성능이 논문·정리·제품·데이터셋·장기 과학진전으로 이어지는지 평가해야 한다.

Future Directions

미래 연구시스템은 Scientific Research OS, claim–evidence graph, proof-carrying artifact, verification budget, research digital twin으로 발전한다.

1. Scientific Research Operating System

Research Question ↓ Problem Formulation Layer ↓ Hypothesis & Claim Graph ↓ Literature and Knowledge Layer ↓ Experiment / Proof / Code Tools ↓ Verifier Ecology ↓ Human Scientific Decision ↓ Artifact & Provenance Ledger ↓ Updated Scientific Memory

2. Claim–Evidence Graph

GC = (Vclaim, Vevidence, Vassumption, Vcounterexample, E)

Supports, contradicts, assumes, derives, supersedes, retracts 관계를 표현한다.

3. Proof-Carrying Research Artifact

Research Result ├─ Formal problem statement ├─ Assumption ledger ├─ Data and code ├─ Execution environment ├─ Tests and numerical checks ├─ Counterexample search log ├─ Formal proof or certificate ├─ Independent audit └─ Known limitations

4. Verification Budget Allocator

bi* = argmaxbi [RiskReductioni(bi) − λbi]

5. Counterexample Ecology

C = {Csymbolic, Cnumeric, Crandom, Cadversarial, Cformal, Chuman}

6. Research Digital Twin

Research Plan ↓ Simulated execution ↓ Expected evidence ↓ Failure and cost estimate ↓ Plan revision ↓ Real execution

7. Negative Knowledge Commons

Failure Record ├─ Problem ├─ Attempt ├─ Preconditions ├─ Failure evidence ├─ Root-cause hypothesis ├─ Applicability scope └─ Conditions for retry

8. Human-Owned Bounded Autonomy

L0 검색·설명부터 L5 승인된 연구 포트폴리오 운영까지 자율권한을 위험에 따라 계층화한다.

9. Model–Harness Co-Design

(θ*, φ*) = argmaxθ,φ U(Modelθ, Harnessφ)

10. Predictive Scientific Evaluation

현재 judge 점수보다 이후 문헌, 새로운 데이터, 후속 채택, 장기 novelty로 가설을 평가한다.

11. Retraction Propagation

ci retracted ⇒ for every cj depending on ci, Recheck(cj)

12. Collaboration Skill Measurement

Synergy(H,A) = P(H + A) − max(P(H), P(A))

13. Dual-Use Research Governance

Research Request ↓ Risk classification ↓ Tool and model permission ↓ Sandboxed exploration ↓ Independent safety review ↓ Controlled disclosure

14. Research Contribution Provenance

Contribution(ri) = (originator, editor, executor, verifier, approver)

15. Closed-Loop Research Metrics

Verified Research Yield = Verified new results / (Compute + Human time) Counterexample Efficiency = Incorrect claims removed / Verification cost Artifact Reproducibility = Independently reproduced / Attempted Collaboration Gain = P(H + A) − max(P(H), P(A))

Conclusion

AI4Research는 연구 AI의 목표를 답변 생성에서 상태관리, 실행 가능한 증거, 인간 소유, 실패지식, 변화하는 과학적 믿음으로 이동시킨다.

Shift 1

답변 생성 → 연구상태 관리

가설, 증거, 반례, 실패, 미해결 질문을 지속적으로 관리한다.

Shift 2

유창성 → 실행 가능한 증거

코드, 수치, 데이터, 반례, 형식증명으로 주장을 검증한다.

Shift 3

완전 자율성 → 인간 소유 자율성

AI는 탐색을 확장하지만 연구목표, 의미, 위험, 채택은 인간이 결정한다.

Shift 4

성공결과 → 실패지식

폐기된 가설과 복구과정도 재현 가능한 연구자원으로 보존한다.

Shift 5

단일 모델 → 시스템

실제 연구능력은 모델, harness, tool, verifier, memory의 공동결과다.

Shift 6

정적 지식 → 변화하는 믿음

새 증거와 철회에 따라 claim graph와 downstream 결과를 갱신한다.

Reliable AI-Assisted Research = Structured Exploration + Executable Evidence + Layered Verification + Auditable Artifacts + Human Scientific Judgment

Sources

공식 워크숍, 전체 논문 목록, 연구 워크플로, 형식화, 수학적 발견, 문제정의, AutoML, 안전 연구의 공개 링크.

ICML 2026 워크숍 페이지Official virtual workshop page AI4Research 공식 홈페이지Workshop scope and program 전체 포스터·논문 배정표Accepted papers and board assignments AI4Research OpenReviewWorkshop submissions The Agentic ResearcherPersistent research workflow Agent-Native Research ArtifactsLogic, trace, evidence AtelierHuman-owned bounded autonomy QUITStructured research phases SocratesQuestion-only scientific advisor SIA-WWeight-level self-improvement Reasoning Is More Than the ModelModel–harness evaluation Agent-Based AuditingMathematical proof auditing CRC-DeriveConformal risk control CRAFTCounterexample-guided theorem repair BRIDGEVerified program synthesis Auditable Lean HarnessReproducible formal proof workflow Library Before ProofReusable formal libraries PeppyAnalytic convergence proofs Finding Simple ProofsSparse proof certificates Ramanujan Hybrid WorkflowHuman–AI mathematical discovery Counting Cycles with AIHuman-guided combinatorial discovery Mathematical Statistics WorkflowPrompting and proof development LacunaResearch mapping and gap discovery Continuous Knowledge MetabolismTime-aware hypothesis generation Read, Grep, and SynthesizeResearch ideation environment GoodPointActionable scientific criticism Scientific Claim UnlearningUpdating and removing scientific claims Open-Ended Task DiscoveryProblem generation and optimization Negative KnowledgeFailure-aware shared memory The Interaction TaxInformation sharing in multi-agent research AIBuildAIAutomated ML research Adaptive Proxy EvaluationMulti-fidelity search evaluation AutoCircuitLLM-driven circuit optimization Causal AI ScientistAutomated causal inference QuantumQUBO AgentQUBO formulation and repair JAXBenchAutonomous TPU kernel optimization AlphaApolloSelf-improving deep research ClaudiniDual-use autoresearch