Researchers from the Institute for AI Research (AIR) at Tsinghua University, led by Executive Director Professor Yang Liu, have achieved a significant breakthrough in mathematical research through a collaborative effort with Tsinghua University’s Qiu Zhen Academy. Using their self-developed AI mathematician system, AIM, the team successfully solved a challenging problem in homogenization theory via a human-AI interactive approach, producing a rigorous 17-page mathematical proof. This work systematically demonstrates the feasibility of AI evolving from a mere “mathematical problem-solving tool” into a true “research collaborator,” opening new pathways for tackling complex mathematical problems. In recent years, multimodal large models (MLLMs) have made remarkable progress—from image captioning to video understanding—yet a critical question remains: do these models truly “understand” and “reason” in complex, multi-step scenarios? To address this, Professor Liu’s team, in collaboration with Tsinghua University’s Department of Computer Science and Fudan University, introduced EscapeCraft: a 3D escape room environment designed to test whether large models can think and act like humans in real-world visual reasoning tasks. The results were revealing: models often saw doors but kept walking around walls, picked up keys but forgot how to use them, and even attempted to “grab” a sofa, reasoning it might contain a hidden compartment. These weren’t isolated failures but systematic shortcomings—evidence that “seeing” does not equate to “understanding.” Even top-tier models like GPT-4o succeeded in only a small fraction of subtasks, with the rest being coincidental or superficial. The study, available at https://arxiv.org/abs/2510.26380, was authored by Yuanhang Liu, Beichen Wang, Peng Li, and Yang Liu. 1. The "AI Dilemma" in Mathematical Research: From Competitions to Real-World Challenges While AI has made impressive strides in mathematical competitions—Gemini achieving a gold medal in the 2025 International Mathematical Olympiad, o4-mini outperforming human teams on the FrontierMath benchmark, and GPT-5-Thinking assisting in quantum computing breakthroughs—these achievements remain largely confined to short, standardized problems. Real mathematical research demands deeper, sustained reasoning, creativity, and conceptual innovation, areas where current AI systems still fall short. Existing AI tools like FunSearch and AlphaEvolve rely on programmatic problem formulation, limiting their applicability. AlphaGeometry excels in geometry but struggles beyond that domain. Even when AI provides useful insights, the construction and validation of complete, rigorous proofs still require human oversight. The core challenge lies in integrating AI into the full research lifecycle—not just as a calculator or assistant, but as a co-researcher capable of contributing to deep theoretical development. 2. Key Achievement: A 17-Page Proof in Homogenization Theory The team focused on a central problem in homogenization theory—a mathematical framework bridging materials science, fluid dynamics, and pure mathematics. Specifically, they investigated the behavior of a coupled Stokes-Lamé system when periodic fluid inclusions shrink to zero scale (ε → 0). The goal was to derive the limiting homogenized equation and rigorously prove the error estimate between the original and limit solutions. Through a human-AI collaborative process, the team not only derived the correct limit equation but also established the precise error order α = 1/2, culminating in a comprehensive 17-page proof. This result significantly exceeds the scope of prior AI-assisted mathematical work. The problem was decomposed into six sub-problems (see Figure 2), each addressed through targeted human-AI interaction. In several of the most difficult sub-problems, the AIM system made non-trivial contributions, demonstrating its ability to engage in high-level mathematical reasoning. 3. Core Methodology: Five Proven Human-AI Interaction Frameworks The team developed a systematic, repeatable framework for human-AI collaboration, offering a practical guide for future research: Direct Prompting: Using “theorem prompts” (providing key theorems and conditions), “concept guidance” (defining proof strategies), and “detail refinement” (correcting symbolic notation and local errors), the team guided AIM toward valid reasoning paths. For instance, in analyzing the “Cell Problem,” human experts provided relevant lemmas, anchoring AIM’s reasoning in solid mathematical foundations. Theory-Coordinated Application: The team packaged entire theoretical frameworks—definitions, lemmas, and inference rules—into “knowledge packages” and fed them to AIM. When proving the regularity of the Cell Problem, the team provided the full Schauder Theory package, enabling AIM to perform multi-step, coherent derivations within a well-defined system. Interactive Iterative Refinement: Following a cycle of “AI output → human diagnosis → feedback → AI revision,” the team progressively refined the proof. During error estimation, when a logical gap was detected, the human expert broke down the issue into sub-components, enabling AIM to correct and complete the proof chain. Applicability Boundary and Exclusive Domain: For tasks beyond AIM’s current capabilities—such as handling complex geometric constructions or multi-scale symbolic manipulation—humans took the lead. For example, the double-scale expansion involving precise derivative decomposition across x and y variables was manually derived by experts to ensure correctness before AI continued. Auxiliary Optimization: The team used multiple strategies to improve AI performance: leveraging the randomness of LLM outputs to explore different proof paths, constraining AI with target conclusions, and selecting the most suitable model for each task (e.g., o4-mini for framework design, DeepSeek-R1 for fine-grained details). 4. Case Study: Proving Regularity in the Cell Problem In one key case, the team provided AIM with Schauder Theory lemmas (Figure 3). The system then successfully integrated these into its reasoning, producing a correct and well-structured proof (Figure 4), showing its ability to follow and apply complex theoretical knowledge. 5. Broader Implications and Future Outlook This work goes beyond solving a single problem. It establishes a new paradigm for mathematical research: AI excels at analyzing, searching, and adapting known theories—automatically decomposing problems, reviewing literature, and optimizing existing methods. However, true theoretical breakthroughs—such as introducing new concepts, designing novel frameworks, or inventing proof paradigms—still rely on human intuition and abstract thinking. Due to AI’s tendency toward hallucination and overconfidence in incorrect conclusions, fully autonomous AI proofs remain unfeasible for now. Human verification at each step remains essential. Looking ahead, the team identifies two key research directions: enhancing AI’s ability to generate and validate novel mathematical concepts, and developing formal verification systems to ensure the reliability of AI-assisted proofs. This work marks a pivotal step toward a future where AI is not just a tool, but a trusted partner in the pursuit of mathematical discovery.