Recent advances in large language models (LLMs) have opened new avenues for accelerating scientific research. While models are increasingly capable of assisting with routine tasks, their ability to contribute to novel, expert-level mathematical discovery is less understood. We present a collection of case studies demonstrating how researchers have successfully collaborated with advanced AI models, specifically Google's Gemini-based models (in particular Gemini Deep Think and its advanced variants), to solve open problems, refute conjectures, and generate new proofs across diverse areas in theoretical computer science, as well as other areas such as economics, optimization, and physics. Based on these experiences, we extract common techniques for effective human-AI collaboration in theoretical research, such as iterative refinement, problem decomposition, and cross-disciplinary knowledge transfer. While the majority of our results stem from this interactive, conversational methodology, we also highlight specific instances that push beyond standard chat interfaces. These include deploying the model as a rigorous adversarial reviewer to detect subtle flaws in existing proofs, and embedding it within a "neuro-symbolic" loop that autonomously writes and executes code to verify complex derivations. Together, these examples highlight the potential of AI not just as a tool for automation, but as a versatile, genuine partner in the creative process of scientific discovery.

翻译：大型语言模型（LLM）的最新进展为加速科学研究开辟了新途径。尽管模型在协助常规任务方面日益成熟，但其对新颖、专家级数学发现的贡献能力尚不明确。本文通过一系列案例研究，展示了研究人员如何与先进AI模型（特别是基于Google Gemini的模型，尤其是Gemini Deep Think及其高级变体）成功协作，解决了理论计算机科学以及经济学、优化和物理学等其他领域的开放性问题，反驳了猜想，并生成了新的证明。基于这些经验，我们提炼出理论研究中有效人机协作的通用技术，例如迭代精炼、问题分解和跨学科知识迁移。虽然我们的成果主要源于这种交互式、对话式方法，但我们也重点介绍了超越标准聊天界面的特定实例。这些实例包括将模型部署为严格的对抗性评审员以检测现有证明中的细微缺陷，以及将其嵌入“神经符号”循环中，自主编写和执行代码以验证复杂推导。这些案例共同凸显了AI的潜力：它不仅是自动化工具，更是科学发现创造性过程中多才多艺的真正合作伙伴。