Tsinghua's AI mathematician is here, advancing from initial ideas all the way to formal theorems and contributing to the completion of an 84-page paper on quantum algorithms.

This time, the AI mathematician isn't just here to solve practice problems.

Previously, the team led by Professor Liu Yang, Dean of the Institute for AI Industry Research (AIR) at Tsinghua University, released an agent system for mathematical research —

AIM.

Unlike many previous agents that focus solely on problem-solving, AIM does not only answer mathematical questions — it also attempts to participate in earlier stages of scientific research:

It can help researchers expand their thinking, organize theorems, generate proof drafts, and pass these outputs to human researchers for further review.

Recently, centered around AIM, Wang Yanqiao, a joint-training student of AIR and Qiuzhen College, and Assistant Professor Liu Jinpeng from Qiuzhen College completed a cutting-edge quantum algorithm research with deep AI participation —

Sign Embedding Quantum Algorithms for Matrix Equations and Matrix Functions.

This research started from a vague intuition: can rational approximation become a design principle for quantum algorithms?

During the research process, AI first helped human researchers lay out all candidate approaches, then humans filtered directions, audited assumptions, and revised derivations. In subsequent stages, AIM participated in theorem organization, proof draft generation, and complexity analysis.

Ultimately, the research team proposed the Sign Embedding Quantum Algorithms, resulting in an 84-page quantum algorithm paper.

It can be said that compared to previous work which mainly solved open mathematical problems given by researchers, this time AIM began to participate in the formulation of research questions and direction exploration.

How was this achieved?

AI's Mathematical Capability is Evolving from "Problem-Solving" to "Research"

In recent years, AI has continuously made progress in mathematical reasoning, algorithm search, conjecture verification, and proof assistance.

Most existing cases focus on relatively well-defined tasks: a proposition to be proved or refuted, an objective function to be optimized, or a search space that can be executed and scored by a program.

However, in real cutting-edge mathematical research, important breakthroughs often occur before the formal emergence of theorems.

Researchers may first have a vague intuition, a cross-domain analogy, or an unformed technical preference, and then gradually determine what problem it should be transformed into, which assumptions to adopt, which route to follow, and ultimately what family of theorems to form.

This stage is often difficult to evaluate with standard answers or a single numerical indicator, but it directly affects the value and direction of the research.

Focusing on the question of "whether AI can assist in problem formulation", this research provides a relatively complete observation sample:

AI and AIM are placed in a research closed-loop supervised by human researchers, participating in both exploration and derivation, while receiving continuous auditing, revision, and integration.

From a Meta-Idea to an Auditable Family of Theorems

It is worth noting that the research did not start from a precisely defined quantum algorithm theorem, but originated from a macroscopic intuition proposed by a human researcher:

Rational approximation has advantages in processing step-type functions, especially the sign function. Can this idea be used as a design principle for quantum algorithms?

In the early exploration stage, through interaction with general AI models, researchers expanded this intuition into a set of candidate research directions and comparison dimensions.

Subsequently, human researchers screened based on mathematical taste, technical feasibility, and potential contributions, and gradually focused on the "Sign-Embedding" route.

As part of the human-machine collaborative research system in subsequent stages, AIM helped organize the selected route into auditable theorem objectives and derivation materials.

The final quantum algorithm paper totals 84 pages. The figure below shows the role AI/AIM played in the formation of this paper.

It should be noted that the functions of route expansion, candidate direction organization, and comparison completed by general AI dialogue in the early stage have been further solidified into systematic capabilities in the subsequent AIM v2.

In other words, this case not only demonstrates a specific research process, but also reflects the evolution of AIM from interactive assistance to support for a more complete scientific research workflow.

Human-Machine Collaborative Workflow: AI High-Throughput Exploration Under Human Value Gating

From the perspective of AI research, the focus of this study is not to demonstrate "fully automatic mathematical discovery", but to present a traceable, auditable, and reusable human-machine collaborative process.

The entire process can be summarized as five links.

Divergent Route Expansion: Human researchers provide core meta-ideas or macroscopic scientific intuitions, and AI expands them into multiple candidate problems, technical routes, and cross-domain connections, helping researchers to quickly perceive the surrounding research space.

Human Value Gate: Facing the candidate branches generated by AI, human researchers screen and focus based on academic judgment, problem value, and technical feasibility, determining which directions are worthy of further investment.

Theorem Formation and Derivation: After the main route is determined, AIM helps transform high-level ideas into auditable materials such as theorem statements, lemma decompositions, proof drafts, and complexity expressions.

Complexity Audit and Repair: In quantum algorithm research, a correct proof does not automatically mean sufficient algorithm contribution; whether the assumptions are natural, whether the access model is reasonable, and whether the complexity is too loose all require repeated checks. The process of repair, optimization, or reconstruction can still be completed with the help of AI/AIM's derivation, comparison, and rewriting capabilities, but key judgments and final confirmations must be undertaken by human researchers.

Validation and Integration: All mathematical statements, proofs, assumptions, complexity estimates, and contribution descriptions must ultimately be verified, selected, revised, and integrated by human researchers before they can be included in public papers.

Connecting Discovery, Derivation Generation, and Prudent Review

In general, the significance of AIM is not to replace human mathematicians to complete research independently, but to improve exploration density and derivation efficiency in a human-supervised loop.

AI/AIM can quickly expand candidate routes, organize connections between related concepts, and generate reviewable proofs and complexity drafts;

Human researchers are responsible for deciding which routes have research value, which assumptions are acceptable, and which derivations need to be repaired.

This collaborative mode makes the research process closer to "high-throughput candidate generation + human value gating + AI-assisted audit and repair + human final integration".

Its advantage is not that the AI's output directly becomes the final conclusion, but that it transforms the originally inexhaustible route exploration, connection organization, and local derivation into intermediate materials that can be checked, compared, and revised step by step.

For AI4Math and AI Scientist research, this also suggests that the feedback signal in theoretical research is often not an experimental score, but a mathematical judgment.

The system needs to support long-term memory, route management, assumption recording, complexity audit, and refutation check, enabling human researchers to more effectively control the direction, discover errors, and stabilize the final results.

Sign Embedding Quantum Algorithms

As a technical achievement formed by this collaborative process, the "Sign Embedding Quantum Algorithms" proposed by Wang Yanqiao and Liu Jinpeng target a class of matrix equation and matrix function problems, including Sylvester, Lyapunov, Riccati equations, as well as objects such as matrix square root, inverse square root, and geometric mean.

These problems are fundamental in numerical linear algebra, control theory, dynamical systems, and scientific computing.

For readers from non-quantum backgrounds, the core idea of this paper can be understood as: first compress multiple types of structured matrix problems into the sign function or sign projection of an expanded matrix,

Then implement the corresponding objects through quantum algorithm primitives such as rational approximation and shifted inverse. This "embedding first, then approximating" route provides a unified organization method for multiple seemingly different problems.

The technical contributions of this quantum paper include: establishing usable assumptions and complexity formulations under more general input conditions such as non-normal and non-diagonalizable inputs;

Advancing the output from a single vector state to matrix block encoding that can be called by downstream quantum circuits; and forming a more systematic quantum linear algebra framework for operator output through scaling, rebalancing, and complexity auditing of the shifted inverse implementation layer.

Human Judgment and AI Productivity in Theoretical Research

In general, this research presents a more realistic way for AI to participate in mathematical research:

AI can help researchers expand routes, organize associations, draft proofs, and conduct preliminary complexity analysis faster, thereby reducing the explicit cost of some basic derivations and local explorations in theoretical research.

But at the same time, whether the research direction is worthy of in-depth exploration, whether the assumptions are natural and reasonable, and whether the results have sufficient theoretical value still depend on the professional judgment and continuous review of researchers.

As agents can quickly generate a large number of candidate routes, proof drafts, and technical descriptions, the focus of theoretical scientists' work may also shift.

After the partial cost of tedious derivation is reduced, researchers can devote more energy to direction selection, problem definition, assumption supervision, and result auditing.

In other words, judging "what problems are really worth studying" and identifying routes that seem reasonable on the surface but have hidden conditions, technical loopholes, or insufficient contributions will become a more critical capability.

This also provides important enlightenment for the subsequent development of AIM. What is worth further strengthening in the future is not only the single-point proof or local derivation capability, but also the systematic capability that supports the entire scientific research process:

For example, recording and comparing different research routes, explicitly managing key assumptions, retaining auditable derivation traces, discovering hidden conditions and complexity loopholes, and supporting researchers to complete subsequent repairs, optimizations, and reconstructions with AI assistance.

This case shows that the value of AI in cutting-edge theoretical research is gradually extending from local task assistance to a more complete research process.

AIM integrates capabilities such as route expansion, association discovery, proof drafting, and audit feedback, enabling AI's generation and derivation capabilities to better serve human researchers' direction judgment and mathematical supervision.

Such a collaborative method provides new possibilities for improving the efficiency of theoretical research and expanding research horizons.

Related Links

AIM System Application Report: From Meta Idea to Advanced Mathematical Discovery: Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms (https://arxiv.org/abs/2606.24899)

Quantum Algorithm Paper: Sign Embedding Quantum Algorithms for Matrix Equations and Matrix Functions (http://arxiv.org/abs/2604.25333)

AIM repo: https://github.com/TheoryFoundry/AIMv2AIM

blog: https://ai-mathematician.net

This article is from the WeChat official account "QbitAI", authored by the Tsinghua AIR team, and republished with authorization from 36Kr.