From Meta Idea to Advanced Mathematical Discovery -- Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms

arXiv cs.LG Papers

Summary

This paper presents a case study of human-AI co-discovery in mathematics, where AI assisted in expanding an intuition about sign-embedding quantum algorithms into a formal framework and proofs, with human judgment guiding route selection.

arXiv:2606.24899v1 Announce Type: new Abstract: AI-assisted mathematics is often evaluated on solving predefined problems. In practice, however, many important advances begin earlier, when a vague research intuition is transformed into a concrete problem, a promising route, and a theorem family worth proving. This report studies that stage through a case study that led to sign-embedding quantum algorithms for matrix equations and matrix functions, foundational primitives in quantum linear algebra and operator-output quantum algorithms. The project began with a human-originated intuition that rational approximation is especially effective for jump-type functions such as the sign function, and might therefore serve as a design principle for quantum algorithms. Rather than merely assisting after the problem was fixed, AI-assisted exploration, including workflows later integrated into the agentic AI-mathematician system AIM, played a key role in expanding this intuition into a route map, comparing candidate formulations, and converging toward sign embedding as the central framework. AIM then helped connect a known matrix-sign identity to wider classes of matrix equations and matrix functions, and drafted proof and complexity calculations. The decisive scientific judgments remained human: selecting which human-AI-expanded routes were worth pursuing, rejecting a Cayley-trapezoidal approximation when its validity required a hidden condition, and refining the Sylvester implementation from a coarse quadratic-gap query route to the final factorized and scaled analysis. The report argues that human-AI co-discovery workflows, with systems such as AIM as important components, are most valuable not as standalone theorem provers, but as research partners for problem formation, connection discovery, derivation, and skeptical review inside a human-gated research loop.
Original Article
View Cached Full Text

Cached at: 06/25/26, 05:06 AM

# From Meta Idea to Advanced Mathematical Discovery Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms
Source: [https://arxiv.org/html/2606.24899](https://arxiv.org/html/2606.24899)
###### Abstract

AI\-assisted mathematics is often evaluated on solving predefined problems\. In practice, however, many important advances begin earlier, when a vague research intuition is transformed into a concrete problem, a promising route, and a theorem family worth proving\. This report studies that stage through a case study that led to sign\-embedding quantum algorithms for matrix equations and matrix functions, foundational primitives in quantum linear algebra and operator\-output quantum algorithms\. The project began with a human\-originated intuition that rational approximation is especially effective for jump\-type functions such as the sign function, and might therefore serve as a design principle for quantum algorithms\. Rather than merely assisting after the problem was fixed, AI\-assisted exploration, including workflows later integrated into the agentic AI\-mathematician systemAIM, played a key role in expanding this intuition into a route map, comparing candidate formulations, and converging toward sign embedding as the central framework\.AIMthen helped connect a known matrix\-sign identity to wider classes of matrix equations and matrix functions, and drafted proof and complexity calculations\. The decisive scientific judgments remained human: selecting which human\-AI\-expanded routes were worth pursuing, rejecting a Cayley\-trapezoidal approximation when its validity required a hidden condition, and refining the Sylvester implementation from a coarse quadratic\-gap query route to the final factorized and scaled analysis\. The report argues that human\-AIco\-discovery workflows, with systems such asAIMas important components, are most valuable not as standalone theorem provers, but as research partners for problem formation, connection discovery, derivation, and skeptical review inside a human\-gated research loop\.111AIM is available at[https://github\.com/TheoryFoundry/AIMv2](https://github.com/TheoryFoundry/AIMv2)\.

Keywords:AI\-assisted mathematical discovery; human\-AI co\-discovery; problem formation; sign\-embedding quantum algorithms; complexity auditing\.

11footnotetext:Corresponding authors:[lipeng@air\.tsinghua\.edu\.cn](https://arxiv.org/html/2606.24899v1/mailto:[email protected]),[liuyang2011@tsinghua\.edu\.cn](https://arxiv.org/html/2606.24899v1/mailto:[email protected])\.## 1 Introduction

![Refer to caption](https://arxiv.org/html/2606.24899v1/image1.png)Figure 1:From a fixed\-target proof pipeline to a human\-gated research\-loop workflow\. The workflow studied in this report begins before a theorem is fixed: AI helps expand a human\-originated idea into candidate routes and proof\-verification loops, while human judgment controls route selection and final audit\.AI\-assisted mathematical discovery has recently moved from a long\-term aspiration to an active research practice\. AI systems have contributed to construction search\[[32](https://arxiv.org/html/2606.24899#bib.bib5)\], algorithm discovery\[[8](https://arxiv.org/html/2606.24899#bib.bib7)\], conjecture testing\[[29](https://arxiv.org/html/2606.24899#bib.bib8)\], and formal or informal proof assistance\[[36](https://arxiv.org/html/2606.24899#bib.bib6),[16](https://arxiv.org/html/2606.24899#bib.bib9),[22](https://arxiv.org/html/2606.24899#bib.bib2),[23](https://arxiv.org/html/2606.24899#bib.bib3),[9](https://arxiv.org/html/2606.24899#bib.bib10)\]\. Most notably, OpenAI recently reported an AI\-generated disproof of a central conjecture in discrete geometry related to Erdős’s unit\-distance problem, marking a significant milestone for AI in mathematics\[[29](https://arxiv.org/html/2606.24899#bib.bib8)\]\. These results suggest that AI can now contribute to mathematical discovery in problems of recognized importance\. At the same time, many of the most visible successes still fit a relatively familiar pattern: the mathematical target is specified in advance, and the AI system is asked to search, optimize, prove, or refute within a predefined problem space\.

This leaves open an earlier and less benchmark\-friendly question:Can AI assist not only in solving mathematical problems, but also in forming them?In advanced research, important progress often begins before a theorem is stated\. A researcher may start from an intuition, a technique, or a vague analogy, and must decide what problem it should become, which route is promising, what assumptions are natural, and what final result would count as a meaningful contribution\. This stage is difficult to evaluate because its intermediate products are not final proofs, executable programs, or numerical scores\. They are formulations, route maps, analogies, assumptions, proof skeletons, and complexity claims whose value depends on mathematical judgment\.

This report studies that earlier stage through a case study in human\-AI co\-discovery\. The underlying mathematical project develops*sign\-embedding quantum algorithms*for matrix equations and matrix functions\[[37](https://arxiv.org/html/2606.24899#bib.bib1)\]\. These problems are foundational in matrix analysis, scientific computing, and quantum linear algebra, and they also serve as central targets for operator\-output quantum algorithms\. The goal is not merely to estimate scalar quantities, but to output quantum\-accessible representations, or block\-encodings, of matrix\-valued objects such as the solution of a Sylvester equation, a principal square root, a matrix geometric mean, or a stabilizing solution of a continuous\-time algebraic Riccati equation\. In simple terms, the sign\-embedding strategy places the desired matrix object inside the sign or sign\-projector of a larger matrix, approximates the sign function by rational functions, and implements the resulting shifted inverses using quantum algorithmic primitives\.

The project did not begin with this sign\-embedding framework already fixed\. It began with a broader human\-originated research intuition:Can rational approximation be used more systematically in quantum algorithms?The intuition came from a simple observation: rational approximation is often especially powerful for jump\-type or nearly discontinuous functions, with the sign function as a guiding example\. From this starting point, many routes were possible, including contour\-integral algorithms, rational block\-encodings, rationalQSVT, spectral projectors, non\-normal filters, matrix\-equation solvers, preconditioners, and reusable rational\-approximation libraries\. Thus, the first research task was not proof search for a fixed statement, but the formation and selection of a route that could support a meaningful theorem family\.

We analyzed this route\-formation stage through direct human\-AIinteraction together with later agentic AI\-mathematician systemAIM\[[22](https://arxiv.org/html/2606.24899#bib.bib2)\]\. AI\-assisted exploration was valuable because it made the surrounding research space denser\. It generated candidate directions, compared formulations, organized connections to numerical linear algebra, and helped turn vague possibilities into theorem\-shaped programs\. In the early phase, most of this exploration was carried out through direct human\-AI dialogue rather than through a dedicated built\-in module; related route\-expansion capabilities were later integrated into theAIMworkflow\. Figure[1](https://arxiv.org/html/2606.24899#S1.F1)summarizes the resulting shift from a fixed\-target proof pipeline to the human\-gated research\-loop workflow studied in this report\.

The sign\-embedding route emerged from the interaction betweenAI\-expanded search and human mathematical judgment\.AIdid not merely assist after the problem was fixed: it helped enlarge and structure the candidate space from which the final problem emerged\. Nor was the route selected autonomously byAI\. The human researcher judged that the sign function matched the original rational\-approximation intuition, and that a classical Higham matrix\-sign identity for the Sylvester equation, already known to the researcher, offered a concrete bridge from matrix equations to operator\-output quantum algorithms\.AIMthen helped expand this anchor point into a broader connection graph, linking sign and sign\-projector identities to square roots, geometric means, stable subspaces, and Riccati equations\. Once the sign\-embedding route became central,AIMfurther helped draft theorem statements, proof skeletons, derivations, complexity calculations, and skeptical objections for human audit\.

The case also illustrates why problem formation and technical validation are tightly coupled in mathematical research\. In quantum algorithms, a theorem may be formally correct but still weak as an algorithmic contribution if its assumptions are unnatural, its access model is unrealistic, its block\-encoding normalization is poor, or its query\-complexity bound is too loose\. For this reason, proof development and complexity auditing were intertwined throughout the project\. SomeAI\-expanded routes were rejected after hidden assumptions were found\. Some first\-pass complexity analyses were repaired into sharper algorithmic statements\. The final result was not simply a proof of a fixed claim, but a theorem family shaped by repeated human\-AIexploration, audit, and refinement\.

The main lesson is that the useful unit of AI\-assisted mathematical discovery can be larger than a single proof attempt\. In this case, the unit was an evolving research question: a broad intuition became a route map through human\-AIinteraction; the route map was filtered by human judgment; one route became a framework; the framework generated theorem targets; and those targets were repeatedly checked, repaired, and sharpened\.AIMwas most valuable not as a standalone theorem prover, but as a connection expander, derivation assistant, and skeptical reviewer inside a human\-gated co\-discovery loop\. Its outputs were treated as candidate material, useful for exploration and drafting but never as evidence of correctness; mathematical statements, assumptions, proofs, algorithms, complexity estimates, and contribution claims entered the manuscript only after human review\.

##### Contributions\.

This report makes three main contributions\. First, it documents a human\-gatedAIresearch workflow for the problem\-formation stage of mathematical research, whereAIMis one component of a broader human\-AIco\-discovery process and where the central task is not simply proving a fixed theorem but turning a broad intuition into auditable theorem targets\. Second, it explains how a rational\-approximation intuition was expanded into a route map and then converged toward sign embedding through human\-AIexploration and human value judgment\. Third, it extracts reusable workflow lessons for other derivation\-heavy mathematical projects, including route ledgers, assumption ledgers, complexity\-audit checklists, and skeptical\-review prompts\.

## 2 Related Work

##### AI\-assisted mathematical discovery\.

AI has recently shown increasingly strong capabilities in mathematical discovery\. Existing systems have contributed to construction search, algorithm discovery, conjecture testing, and proof assistance\. Representative examples include FunSearch, which uses language models and external evaluators to discover mathematical constructions\[[32](https://arxiv.org/html/2606.24899#bib.bib5)\]; AlphaTensor, which discovered faster matrix\-multiplication algorithms\[[8](https://arxiv.org/html/2606.24899#bib.bib7)\]; AlphaGeometry and AlphaProof, which demonstrate progress on mathematical reasoning and theorem proving\[[36](https://arxiv.org/html/2606.24899#bib.bib6),[16](https://arxiv.org/html/2606.24899#bib.bib9)\]; neural theorem\-proving and formal\-verification infrastructure\[[30](https://arxiv.org/html/2606.24899#bib.bib13),[18](https://arxiv.org/html/2606.24899#bib.bib14),[7](https://arxiv.org/html/2606.24899#bib.bib15)\]; and recent AI\-generated progress on discrete geometry reported by OpenAI\[[29](https://arxiv.org/html/2606.24899#bib.bib8)\]\. Our earlier work onAIMstudies an agentic AI\-mathematician system for long\-horizon frontier mathematical research\[[22](https://arxiv.org/html/2606.24899#bib.bib2)\], and a related case study shows howAIMcan act as a human\-AI partner in advancing an open problem in homogenization theory\[[23](https://arxiv.org/html/2606.24899#bib.bib3)\]\. These developments suggest that AI systems are beginning to contribute to mathematical discovery in problems of recognized importance\. However, many of the most visible examples still start from a relatively well\-specified mathematical target: a conjecture to test or refute, a construction to improve, an algorithmic objective to optimize, or a proof task to complete\. The present report focuses on an earlier stage: how AI can help transform a broad research intuition into a concrete mathematical problem and a theorem family worth pursuing\.

##### AI Scientist and automated research workflows\.

A related line of work studies AI systems that automate larger portions of the research process\. The AI Scientist treats idea generation, experiment design, execution, paper writing, and review as components of a \(partially\) automatable scientific pipeline\[[27](https://arxiv.org/html/2606.24899#bib.bib4)\]\. This line of work is important because it moves beyond isolated task solving and asks whether AI can participate in the full cycle of research production\. Most existing AI\-Scientist\-style systems\[[27](https://arxiv.org/html/2606.24899#bib.bib4),[12](https://arxiv.org/html/2606.24899#bib.bib11),[10](https://arxiv.org/html/2606.24899#bib.bib12)\], however, are evaluated in domains where experiments provide relatively direct feedback: a proposed idea can be implemented, run, scored, and compared with baselines\. The mathematical setting studied in this report is different\. Here, the key feedback is not an experimental score but mathematical judgment: whether a route is meaningful, whether its assumptions are natural, whether a proof sketch is valid, and whether a complexity statement is strong enough to constitute a real contribution\. In this sense, our case study gives an independent mathematical counterpart to AI\-Scientist\-style research automation: it examines whether AI can help shape the research problem itself when progress is guided mainly by theoretical derivation rather than empirical evaluation\.

##### AIMand human\-AI mathematical collaboration\.

This report builds directly on our previous work onAIM, an agentic AI\-mathematician framework designed to support long\-horizon mathematical research\[[22](https://arxiv.org/html/2606.24899#bib.bib2)\]\.AIMorganizes mathematical work around exploration, verification, refinement, and memory\. In the homogenization case study,AIMwas used as a mathematical partner in a technically demanding project, with human researchers retaining control over conceptual decisions and final validation\[[23](https://arxiv.org/html/2606.24899#bib.bib3)\]\. Other human\-AI mathematical workflows similarly emphasize expert control over conceptualization, validation, and final acceptance, while AI systems accelerate local exploration, proof development, literature search, and theory building\[[20](https://arxiv.org/html/2606.24899#bib.bib16),[39](https://arxiv.org/html/2606.24899#bib.bib17)\]\. The present report extends this line of work in a different direction\. Rather than focusing mainly on AI as a proof partner after a problem is already chosen, we use direct human\-AIinteraction andAIMto examine how AI can participate in problem formation: expanding a human\-originated rational\-approximation intuition into candidate routes, helping compare those routes, and supporting the convergence toward the sign\-embedding quantum\-algorithm framework\.

##### Quantum algorithms, block\-encodings, and matrix sign functions\.

The technical background of the companion mathematical project comes from quantum algorithms and matrix analysis\. Quantum linear\-system algorithms initiated the study of quantum procedures for linear\-algebraic problems\[[13](https://arxiv.org/html/2606.24899#bib.bib20),[6](https://arxiv.org/html/2606.24899#bib.bib21)\]\. Linear\-combination\-of\-unitaries \(LCU\) methods, quantum signal processing, qubitization, and quantum singular value transformation \(QSVT\) provide general tools for implementing matrix transformations in the block\-encoding model\[[4](https://arxiv.org/html/2606.24899#bib.bib23),[24](https://arxiv.org/html/2606.24899#bib.bib24),[25](https://arxiv.org/html/2606.24899#bib.bib25),[11](https://arxiv.org/html/2606.24899#bib.bib22)\]\. Beyond singular\-value\-based approaches, linear combination of Hamiltonian simulation \(LCHS\) is a significant quantum algorithm for non\-unitary and non\-normal problems, with improved state\-preparation costs, near\-optimal parameter dependence, refined integral kernels, Laplace\-transform eigenvalue transformations, and PDE\-oriented extensions\[[3](https://arxiv.org/html/2606.24899#bib.bib34),[2](https://arxiv.org/html/2606.24899#bib.bib35),[1](https://arxiv.org/html/2606.24899#bib.bib36),[28](https://arxiv.org/html/2606.24899#bib.bib37),[33](https://arxiv.org/html/2606.24899#bib.bib38),[26](https://arxiv.org/html/2606.24899#bib.bib39),[15](https://arxiv.org/html/2606.24899#bib.bib40),[38](https://arxiv.org/html/2606.24899#bib.bib41)\]\.Generic contour\-integral block\-encoding algorithms for matrix functions and recent operator\-output algorithms for Sylvester, Lyapunov, geometric\-mean, and Riccati\-type problems provide the closest quantum\-algorithmic context\[[35](https://arxiv.org/html/2606.24899#bib.bib26),[34](https://arxiv.org/html/2606.24899#bib.bib27),[21](https://arxiv.org/html/2606.24899#bib.bib31)\]\. The companion sign\-embedding work studies a structured operator\-output setting: instead of only estimating scalar quantities or preparing solution states, it aims to output block\-encodings of matrix\-valued objects such as Sylvester\-equation solutions, matrix square roots, geometric means, and Riccati solutions\[[37](https://arxiv.org/html/2606.24899#bib.bib1)\]\. On the classical side, matrix\-sign methods provide identities connecting sign functions, Sylvester equations, invariant subspaces, matrix roots, geometric means, and algebraic Riccati equations\[[14](https://arxiv.org/html/2606.24899#bib.bib18),[17](https://arxiv.org/html/2606.24899#bib.bib28),[19](https://arxiv.org/html/2606.24899#bib.bib19),[31](https://arxiv.org/html/2606.24899#bib.bib29),[5](https://arxiv.org/html/2606.24899#bib.bib30)\]\. This report does not rederive that technical theory; instead, it analyzes how the sign\-embedding route was formed, audited, and refined through a human\-gatedAIresearch workflow in whichAIMserved as one component\.

## 3 Human\-Gated AI Research Workflow

The workflow has five stages after the human researcher supplies the initial meta idea\. Figure[2](https://arxiv.org/html/2606.24899#S3.F2)gives the process view, while Table[1](https://arxiv.org/html/2606.24899#S3.T1)gives the corresponding protocol view\.

### 3\.1 Stage Protocol

Stage 1 is expansive, Stage 2 is selective, Stage 3 develops theorem\-shaped material, Stage 4 tests whether the theorem is algorithmically meaningful, and Stage 5 prevents generated material from entering the manuscript without human control\. Table[1](https://arxiv.org/html/2606.24899#S3.T1)summarizes the protocol\.

##### Stage 1: divergent route expansion\.

The initial route expansion was carried out through direct human\-AIdialogue, which expanded a broad theme rather than solved a fixed problem, producing a route map around rational approximation\.

##### Stage 2: human value gate\.

The human researcher selected the sign route\. The reason was not thatAIMhad proved it superior, but that it matched two human value criteria: rational approximation is naturally strong for jump\-type functions, and the matrix sign has classical identities that can compress several structured problems into one reusable template\.

##### Stage 3: theorem formation and derivation\.

Once the sign route was selected,AIMhelped produce theorem statements, lemma decompositions, proof skeletons, and complexity derivations\. It was especially useful for turning a high\-level mathematical idea into detailed proof material that could be audited\.

##### Stage 4: complexity audit and repair\.

Complexity auditing changed theorem targets\. A first\-pass theorem may prove implementability but still be algorithmically unattractive\. In this project, query complexity, output normalization, shifted\-inverse conditioning, coefficient weights, and precision allocation were not secondary bookkeeping details; they determined which formulation was worth keeping\. When an argument failed the audit, the theorem target, implementation route, or analytic approximation was repaired rather than simply copied into the manuscript\.

##### Stage 5: validation and integration\.

The final stage was human\-led\.AIMcould suggest corrections, act as a skeptical reviewer, and help rewrite exposition\. The human researcher decided which claims were true, useful, and appropriately stated\.

Human meta ideaStage 1divergent routeexpansionStage 2human valuegateSelected routeand theorem targetsStage 3theorem formationand derivationStage 4complexity auditand repairStage 5validationand integrationhuman\-approvedartifact

Figure 2:Human\-gated AI research workflow\.
Table 1:Protocol for the human\-gatedAIresearch workflow\.

### 3\.2 Development Trajectory

The development trajectory was not a straight line from prompt to proof: First, the human researcher began with a meta idea: rational approximation often has advantages for jump\-like functions, so it might support new quantum algorithm designs\. Second, human\-AI interaction carried out Stage 1 divergent route expansion by turning the idea into a large set of candidate directions\. Third, the human researcher applied the Stage 2 human value gate and chose sign embedding, because of the sign function itself and because Higham’s matrix\-sign identity for Sylvester equations suggested a concrete algebraic bridge\. Fourth,AIMhelped connect this known identity to a broader network of square\-root, geometric\-mean, stable\-subspace, and Riccati identities\. Fifth,AIMassisted with Stage 3 theorem formation and derivation by drafting theorem statements, proof skeletons, and complexity calculations\. Sixth, Stage 4 complexity audit and repair exposed proof and complexity problems, including an invalid early contour route and a loose Sylvester complexity route\. Finally, Stage 5 validation and integration stabilized the manuscript around the log\-sinc approximation, structure\-aware shifted inverse implementation, and nodewise rebalancing\.

The main contribution of the broader human\-AIresearch workflow was to accelerate route expansion, connection discovery, theorem formation, derivation, and skeptical review after the human researcher had supplied the starting ambition and continued to control the value gate\. Within that workflow,AIMwas most clearly responsible for the later connection\-discovery, theorem\-formation, derivation, complexity\-review, and skeptical\-review stages\.

### 3\.3 Map of AIM’s Role in the Companion Paper

Figure[3](https://arxiv.org/html/2606.24899#S3.F3)complements the stage protocol by showing where the human\-AIresearch workflow entered the companion sign\-embedding paper\[[37](https://arxiv.org/html/2606.24899#bib.bib1)\]\. Whereas Figure[2](https://arxiv.org/html/2606.24899#S3.F2)and Table[1](https://arxiv.org/html/2606.24899#S3.T1)describe the abstract process, Figure[3](https://arxiv.org/html/2606.24899#S3.F3)maps that process onto the 84\-page mathematical manuscript\. The vertical strip represents the manuscript from front matter to appendices, with section heights roughly proportional to page spans\. The colors indicate the dominant development mode of each portion: human\-originated material,AIM\-inspired and human\-AIMco\-development,AIM\-generated material that was substantially rewritten by the human researcher, and human\-led correction or optimization\.

The figure should be read as a development map, not as a quantitative allocation of scientific credit, difficulty, or novelty\.AIMwas especially useful for connection expansion, theorem\-shaped drafting, and first\-pass derivation\. Human control was most important at the human value gate, audit, optimization, and integration stages\.

![[Uncaptioned image]](https://arxiv.org/html/2606.24899v1/image6.6.png)

Figure 3:Section\-level development map of the 84\-page sign\-embedding paper\[[37](https://arxiv.org/html/2606.24899#bib.bib1)\]\. The vertical strip represents the manuscript from front matter to appendices, with section heights roughly proportional to page spans\. Colors indicate the dominant development mode of each portion\. The map is descriptive rather than quantitative: it is not intended to assign scientific credit, difficulty, or novelty\.

## 4 Mathematical Setting

This section gives the mathematical background needed for the case study\.

### 4\.1 Operator\-Output Block\-Encoding Algorithms

The companion project studies*operator\-output*quantum algorithms\[[37](https://arxiv.org/html/2606.24899#bib.bib1)\]\. The output is not only a number or a quantum state\. It is a block\-encoding of a matrix\-valued object\. A unitaryUUis a block\-encoding of a matrixXXwith normalizationβ\\betaand errorε\\varepsilonif

‖\(⟨0a\|⊗I\)​U​\(\|0a⟩⊗I\)−Xβ‖≤ε\.\\left\\\|\(\\langle 0^\{a\}\|\\otimes I\)U\(\|0^\{a\}\\rangle\\otimes I\)\-\\frac\{X\}\{\\beta\}\\right\\\|\\leq\\varepsilon\.\(1\)The normalizationβ\\betamatters\. A theorem that gives a correct block\-encoding but with a very largeβ\\betamay be much less useful for later quantum procedures\. Therefore the quality of the algorithm depends on the target error, the number of oracle queries, the shifted\-inverse conditioning, and the final block\-encoding normalization\.

### 4\.2 Sign Embeddings for Structured Matrix Problems

The motivating example is the Sylvester equation

For

M=\[AC0−B\],M=\\begin\{bmatrix\}A&C\\\\ 0&\-B\\end\{bmatrix\},\(3\)a classical matrix\-sign identity gives, under half\-plane separation,

sign⁡\(M\)=\[I2​X0−I\]\.\\operatorname\{sign\}\(M\)=\\begin\{bmatrix\}I&2X\\\\ 0&\-I\\end\{bmatrix\}\.\(4\)Thus the solutionXXis an off\-diagonal block ofsign⁡\(M\)\\operatorname\{sign\}\(M\)\[[14](https://arxiv.org/html/2606.24899#bib.bib18)\]\.

The same philosophy appears elsewhere:

K​\(A\)=\[0AI0\],sign⁡\(K​\(A\)\)=\[0A1/2A−1/20\],K\(A\)=\\begin\{bmatrix\}0&A\\\\ I&0\\end\{bmatrix\},\\qquad\\operatorname\{sign\}\(K\(A\)\)=\\begin\{bmatrix\}0&A^\{1/2\}\\\\ A^\{\-1/2\}&0\\end\{bmatrix\},\(5\)and for a Hamiltonian matrixHHassociated with a continuous\-time algebraic Riccati equation,

Π−=I−sign⁡\(H\)2,X=Π21​Π11−1\.\\Pi\_\{\-\}=\\frac\{I\-\\operatorname\{sign\}\(H\)\}\{2\},\\qquad X=\\Pi\_\{21\}\\Pi\_\{11\}^\{\-1\}\.\(6\)The quantum problem is not to rediscover these classical identities\. It is to compile them into operator\-output quantum algorithms with explicit assumptions, query complexity, and block\-encoding normalization\.

### 4\.3 Non\-Normal Regimes and Complexity\-Relevant Formulation

For normal matrices, spectral language is often sufficient\. For non\-normal matrices, it can hide invalid proof steps\. The final project therefore used field\-of\-values and strip\-resolvent certificates\. For a matrixTT, define

H​\(T\)=T\+T∗2,W​\(T\)=\{x∗​T​x:‖x‖=1\}\.H\(T\)=\\frac\{T\+T^\{\*\}\}\{2\},\\qquad W\(T\)=\\\{x^\{\*\}Tx:\\left\\lVert x\\right\\rVert=1\\\}\.\(7\)A representativeFoVgap regime assumes

H​\(A\)⪰μ​I,H​\(B\)⪰μ​I,H\(A\)\\succeq\\mu I,\\qquad H\(B\)\\succeq\\mu I,\(8\)whereas a broader strip\-resolvent regime assumes

γΩa​\(M\):=supz∈Ωa‖\(z​I−M\)−1‖<∞,Ωa=\{z∈ℂ:\|Re⁡z\|≤a\}\.\\gamma\_\{\\Omega\_\{a\}\}\(M\):=\\sup\_\{z\\in\\Omega\_\{a\}\}\\left\\lVert\(zI\-M\)^\{\-1\}\\right\\rVert<\\infty,\\qquad\\Omega\_\{a\}=\\\{z\\in\\mathbb\{C\}:\|\\operatorname\{Re\}z\|\\leq a\\\}\.\(9\)This shift from informal spectral statements to explicit resolvent certificates was an important human\-audit step\. It prevented proof sketches from silently assuming normality or diagonalizability\.

The implementation layer introduces another pressure\. A rational approximation to the sign function produces sums of shifted inverses\. But a rational formula is not yet a quantum algorithm: each shifted inverse must be block\-encoded, combined throughLCU, and charged to the final error and normalization\. This is why complexity auditing became part of problem formation rather than a final accounting step\.

## 5 Case Study: From Rational Approximation to Audited Theorem Family

The case study is best understood through concrete episodes\. Each episode shows a division of labor: what human\-AIinteraction orAIMgenerated, what the human researcher judged or repaired, and how the final theorem target changed\.

### 5\.1 Route Expansion and Convergence to Sign Embedding

After having a meta idea, AI was helpful in brainstorming\. And the useful outputs of the early human\-AIinteraction were series of related divergent problems\. Starting from the broad theme of rational approximation in quantum algorithms, the dialogue produced candidate formulations and comparison axes rather than a single theorem statement\. This expansion turned a vague idea into a comparison set\. It also showed that the project could easily become too broad\. The human researcher therefore had to choose a route that was not only plausible, but capable of generating a differentiated theorem family\.

The currentAIMv2 system has since integrated this route\-expansion capability\. In a laterAIMv2 reproduction, the system produced the following representative list of candidate directions:222In the early experiments of this project, divergent expansion was carried out through direct human\-AIdialogue rather than through a dedicated built\-in module\. In the currentAIMv2 system, this route\-expansion capability has since been integrated\. The list reported here is a representativeAIMv2 reproduction, not a verbatim transcript of the earliest exploration\.

1. 1\.rational block\-encodings of matrix functions via shifted resolvents;
2. 2\.quantum algorithms for Lyapunov, Sylvester, and Riccati equations using rational Krylov ideas;
3. 3\.spectral projectors and invariant subspaces via rational filters;
4. 4\.quantum rational preconditioners as output objects;
5. 5\.matrix sign, polar decomposition, and stable subspace computation;
6. 6\.rational approximations for non\-Hermitian matrix functions and pseudospectral filters;
7. 7\.quantum contour/rational algorithms for matrix equations with separable kernels;
8. 8\.operator\-valued model reduction, such as Gramians and transfer functions;
9. 9\.rational approximation as a compiler from classical numerical linear algebra to block\-encodings;
10. 10\.certified rational approximation libraries forQSVTand block\-encoding algorithms\.

The sign route was selected for two human reasons\. First, it matched the original observation that rational approximation can be especially effective for jump\-type functions\. Second, the researcher already knew Higham’s sign identity for Sylvester equations, which made the route concrete rather than merely suggestive\.AIM’s contribution was to expand the connection graph around this known identity\. It helped organize the fact that sign and sign\-projector identities also appear in principal roots, geometric means, stable subspace computation, and Riccati theory\.

The result was a framework slogan:

structured matrix problem⟶sign embedding⟶rational sign approximation\\displaystyle\\longrightarrow\\text\{sign embedding\}\\longrightarrow\\text\{rational sign approximation\}⟶scaled shifted inverses⟶operator\-output block\-encoding\.\\displaystyle\\longrightarrow\\text\{scaled shifted inverses\}\\longrightarrow\\text\{operator\-output block\-encoding\}\.This was not yet a theorem\. It was a research target generator\.

### 5\.2 Known Identity, Expanded Connection Graph

AIMdid not independently discover the Higham sign identity\. The human researcher knew the Sylvester identity \([4](https://arxiv.org/html/2606.24899#S4.E4)\)\.AIM’s role was different: it helped expand and organize nearby classical connections\. This changed the identity’s role in the project\. It was no longer only a classical trick for one equation; it became the seed of a reusable quantum\-algorithmic template\.

This episode illustrates a common pattern in the workflow\. Human expertise supplied an anchor point that was already mathematically meaningful\.AIMthen generated adjacent structures and helped test whether the anchor could become a framework\. The human value gate determined which adjacent structures were worth retaining\.

### 5\.3 Method Repair: From Cayley–Trapezoidal Sign Approximation to Log\-Sinc

One of the most important proof\-level repairs occurred in the sign\-approximation layer\. In an early version,AIMdeveloped a Cayley–trapezoidal rational–resolvent approximation of the matrix sign\. This route was attractive because it fit the rational\-resolvent philosophy and produced plausible shifted\-inverse formulas\.

The human audit found a problem: the proof relied on an additional nontrivial inversion\-contour\-validity condition that was not stated in the generated argument\. In other words, the route was not merely missing a small detail; its validity under the desired assumptions was not yet justified\.

The project therefore changed methods\. Rather than patching the Cayley–trapezoidal route with a hidden or restrictive assumption, the analytic core moved to a log\-sinc construction\. The final approximation uses the sign integral

sign⁡\(M\)=1π​∫−∞∞ex​\(\(M−i​ex​I\)−1\+\(M\+i​ex​I\)−1\)​𝑑x,\\operatorname\{sign\}\(M\)=\\frac\{1\}\{\\pi\}\\int\_\{\-\\infty\}^\{\\infty\}e^\{x\}\\left\(\(M\-\\mathrm\{i\}e^\{x\}I\)^\{\-1\}\+\(M\+\\mathrm\{i\}e^\{x\}I\)^\{\-1\}\\right\)\\,dx,\(10\)and discretizes the real line at geometric nodes

tk=ek​h,k=−K,…,K\.t\_\{k\}=e^\{kh\},\\qquad k=\-K,\\ldots,K\.\(11\)This log\-sinc route had two advantages\. Analytically, it gave a cleaner proof under strip\-resolvent control\. Algorithmically, its geometric nodes matched the scaled shifted\-inverse families used later\. This episode is a central example of why human audit was essential:AIMgenerated a plausible analytic route, but the human researcher determined that the route did not meet the intended theorem assumptions and replaced it\.

### 5\.4 Sylvester Complexity Audit: Query Complexity and Normalization

The clearest complexity episode occurred for the ordinary Sylvester equation in theFoVgap regime\. A first\-passAIM\-assisted implementation analysis led to aμ−2\\mu^\{\-2\}\-type query route\. The reason was that it treated the augmented sign resolvents too directly and the implementation is not multiplexing\. Under theFoVgap, the augmented strip\-resolvent constant for

M=\[AC0−B\]M=\\begin\{bmatrix\}A&C\\\\ 0&\-B\\end\{bmatrix\}can scale likeO​\(μ−2\)O\(\\mu^\{\-2\}\), because the off\-diagonal block of\(z​I−M\)−1\(zI\-M\)^\{\-1\}contains a product of two shifted resolvents\. A direct augmented\-resolvent implementation therefore leads to a coarse query target\.

The human complexity audit changed the theorem target by using the block factorization and scaled multiplexing

\[\(z​I−M\)−1\]12=\(z​I−A\)−1​C​\(z​I\+B\)−1\.\\left\[\(zI\-M\)^\{\-1\}\\right\]\_\{12\}=\(zI\-A\)^\{\-1\}C\(zI\+B\)^\{\-1\}\.\(12\)After log\-sinc discretization and scaled multiplexing, this leads to the scaled Sylvester representation

XK,h=∑k=−KKh​tk2​π​\(1\+tk\)2\(\\displaystyle X\_\{K,h\}=\\sum\_\{k=\-K\}^\{K\}\\frac\{ht\_\{k\}\}\{2\\pi\(1\+t\_\{k\}\)^\{2\}\}\\Big\(\(1\+tk\)\(A−itkI\)−1C\(1\+tk\)\(B\+itkI\)−1\+\(1\+tk\)\(A\+itkI\)−1C\(1\+tk\)\(B−itkI\)−1\)\.\\displaystyle\(1\+t\_\{k\}\)\(A\-\\mathrm\{i\}t\_\{k\}I\)^\{\-1\}C\(1\+t\_\{k\}\)\(B\+\\mathrm\{i\}t\_\{k\}I\)^\{\-1\}\+\(1\+t\_\{k\}\)\(A\+\\mathrm\{i\}t\_\{k\}I\)^\{\-1\}C\(1\+t\_\{k\}\)\(B\-\\mathrm\{i\}t\_\{k\}I\)^\{\-1\}\\Big\)\.\(13\)The scalarLCUcoefficient weight

ΛK,hsyl=∑k=−KKh​tkπ​\(1\+tk\)2\\Lambda\_\{K,h\}^\{\\mathrm\{syl\}\}=\\sum\_\{k=\-K\}^\{K\}\\frac\{ht\_\{k\}\}\{\\pi\(1\+t\_\{k\}\)^\{2\}\}\(14\)remains bounded under the relevant mesh choices\. The inverse calls are then made to shifted families forAAandBB, each withFoVconditioningO​\(μ−1\)O\(\\mu^\{\-1\}\)\. Thus the query complexity to theAAandBBoracles becomesμ−1\\mu^\{\-1\}\-type up to logarithmic factors, rather than the coarseμ−2\\mu^\{\-2\}\-type direct augmented\-resolvent route\.

A key nuance is that this improvement concerns*query complexity*\. The output block\-encoding normalization is a separate quantity\. In the plainFoVheadline theorem, the normalization still has anO​\(μ−2\)O\(\\mu^\{\-2\}\)scale, while refined banded\-overlap regimes improve it toO​\(μ−1\+τ​μ−2\)O\(\\mu^\{\-1\}\+\\tau\\mu^\{\-2\}\), and in the Hermitian or narrow\-band case this becomesO​\(μ−1\)O\(\\mu^\{\-1\}\)\. This distinction between query complexity and output normalization was itself part of the human audit\.

Nodewise rebalancing records more refined information through profiles

\(1\+tk\)​‖\(A±i​tk​I\)−1‖≤ρA,k±,\(1\+tk\)​‖\(B±i​tk​I\)−1‖≤ρB,k±,\(1\+t\_\{k\}\)\\left\\lVert\(A\\pm\\mathrm\{i\}t\_\{k\}I\)^\{\-1\}\\right\\rVert\\leq\\rho\_\{A,k\}^\{\\pm\},\\qquad\(1\+t\_\{k\}\)\\left\\lVert\(B\\pm\\mathrm\{i\}t\_\{k\}I\)^\{\-1\}\\right\\rVert\\leq\\rho\_\{B,k\}^\{\\pm\},\(15\)and an overlap sum

Θρsyl:=∑k=−KKh​tk2​π​\(1\+tk\)2​\(ρA,k−​ρB,k\+\+ρA,k\+​ρB,k−\)\.\\Theta\_\{\\rho\}^\{\\mathrm\{syl\}\}:=\\sum\_\{k=\-K\}^\{K\}\\frac\{ht\_\{k\}\}\{2\\pi\(1\+t\_\{k\}\)^\{2\}\}\\left\(\\rho\_\{A,k\}^\{\-\}\\rho\_\{B,k\}^\{\+\}\+\\rho\_\{A,k\}^\{\+\}\\rho\_\{B,k\}^\{\-\}\\right\)\.\(16\)This changed the theorem from “a rational sum can be implemented” to “the sign\-embedded rational sum can be implemented with factorized, scaled, and profile\-aware shifted inverse families\.” That is a stronger and more useful algorithmic statement\.

### 5\.5 Square Roots: Derivation byAIM, Optimization by Human Audit

The extension stage separated two kinds of value\. For square roots, geometric means, and continuous\-time algebraic Riccati equations \(CARE\),AIMwas effective at turning high\-level sign\-embedding ideas into theorem\-shaped material: augmented matrices, recovery formulas, proof skeletons, rational formulas, and implementation decompositions\. The square\-root module best illustrates the additional role of human audit and optimization\.

The basic embedding is

K​\(A\)=\[0AI0\],sign⁡\(K​\(A\)\)=\[0A1/2A−1/20\]\.K\(A\)=\\begin\{bmatrix\}0&A\\\\ I&0\\end\{bmatrix\},\\qquad\\operatorname\{sign\}\(K\(A\)\)=\\begin\{bmatrix\}0&A^\{1/2\}\\\\ A^\{\-1/2\}&0\\end\{bmatrix\}\.\(17\)AIMcould help derive the corresponding positive\-shift rational formulas\. Applying the log\-sinc rule reduces the inverse\-square\-root output to a single family

AK,h−1/2=2​hπ​∑k=−KKtk​\(A\+tk2​I\)−1\.A^\{\-1/2\}\_\{K,h\}=\\frac\{2h\}\{\\pi\}\\sum\_\{k=\-K\}^\{K\}t\_\{k\}\(A\+t\_\{k\}^\{2\}I\)^\{\-1\}\.\(18\)A plain shifted\-inverse analysis would track

\(1\+tk2\)​‖\(A\+tk2​I\)−1‖≤O​\(μ−1\),\(1\+t\_\{k\}^\{2\}\)\\left\\lVert\(A\+t\_\{k\}^\{2\}I\)^\{\-1\}\\right\\rVert\\leq O\(\\mu^\{\-1\}\),and therefore suggests anO​\(μ−1\)O\(\\mu^\{\-1\}\)\-scale normalization\. The human audit identified the stronger profile

ρksq=1\+tk2μ\+tk2\.\\rho\_\{k\}^\{\\mathrm\{sq\}\}=\\frac\{1\+t\_\{k\}^\{2\}\}\{\\mu\+t\_\{k\}^\{2\}\}\.\(19\)With this profile, the relevant overlap sum scales as

∑k=−KK2​h​tkπ​\(1\+tk2\)​ρksq=O​\(μ−1/2\)\.\\sum\_\{k=\-K\}^\{K\}\\frac\{2ht\_\{k\}\}\{\\pi\(1\+t\_\{k\}^\{2\}\)\}\\,\\rho\_\{k\}^\{\\mathrm\{sq\}\}=O\(\\mu^\{\-1/2\}\)\.\(20\)Thus the square\-root theorem target changed from a plainO​\(μ−1\)O\(\\mu^\{\-1\}\)normalization to the optimal\-orderO​\(μ−1/2\)O\(\\mu^\{\-1/2\}\)normalization for the inverse\-square\-root output\. This is the cleanest extension example whereAIMwas valuable for derivation, while the human researcher was decisive in recognizing that the theorem could and should be sharpened\.

### 5\.6 Continuous\-Time Algebraic Riccati Equations \(CARE\): Analogy Control

The continuous\-time algebraic Riccati equations \(CARE\) modules show the value and risk of analogy\.AIMwas useful in expanding the sign\-embedding framework to these cases and in drafting the corresponding algebraic and implementation details\. But the human audit had to determine where analogy was legitimate and where additional conditions were needed\.

For CARE, the target is not a single off\-diagonal sign block\. One uses the Hamiltonian matrix

H=\[A−G−Q−A∗\],Π−=I−sign⁡\(H\)2,H=\\begin\{bmatrix\}A&\-G\\\\ \-Q&\-A^\{\*\}\\end\{bmatrix\},\\qquad\\Pi\_\{\-\}=\\frac\{I\-\\operatorname\{sign\}\(H\)\}\{2\},and extracts the stabilizing solution through

X=Π21​Π11−1\.X=\\Pi\_\{21\}\\Pi\_\{11\}^\{\-1\}\.This requires a sign stage, a projector\-block extraction stage, and a projector\-inversion stage\.AIMhelped organize this Hamiltonian sign\-projector narrative and generated proof skeletons\. Human audit required explicit assumptions: half\-plane separation, strip\-resolvent control, and an invertibility gap forΠ11\\Pi\_\{11\}\. The surviving CARE module was therefore more cautious and more accurate than a direct analogy from Sylvester\.

## 6 Artifacts for an Auditable Workflow

The workflow became reliable only after AI\-generated material was converted into auditable artifacts\. In this case study, three artifacts were most useful: an episode ledger recording accepted, repaired, and rejected outputs; a complexity\-audit checklist for query cost and normalization claims; and an adversarial review prompt for exposing hidden assumptions\.

### 6\.1 Episode Ledger

Table[2](https://arxiv.org/html/2606.24899#S6.T2)summarizes the main episodes\. The ledger records not only what was adopted, but also what was repaired or rejected\.

Table 2:Case ledger for the sign\-embedding project\.

### 6\.2 Complexity\-Audit Checklist

The complexity\-audit checklist operationalizes Stage 4 at the level of a single theorem or algorithmic module\. Its purpose is not merely to verify that a rational formula can be written down, but to decide whether the formula survives as a useful quantum algorithm after oracle access, shifted\-inverse conditioning,LCUweights, precision allocation, and block\-encoding normalization are all charged explicitly\. The complexity audit asks whether those hypotheses actually support the claimed query cost and output normalization\.

Before accepting a complexity statement, we should check that:

1. 1\.Which shifted inverse primitive is being used, and what conditioning parameter does it require?
2. 2\.Is the claimed improvement about query complexity, output normalization, or both?
3. 3\.What is the normalization of every input block\-encoding before multiplication orLCUcombination?
4. 4\.What is the coefficient weight in theLCUconstruction, and does it remain controlled after scaling?
5. 5\.Are deterministic rational\-approximation error and inverse\-implementation error separated until the final theorem?
6. 6\.Are inverse errors allocated before or after multiplication by normalization factors?
7. 7\.Does the bound use a uniform worst\-case inverse norm, or can it use a nodewise profile?
8. 8\.Does the algorithm require coherent access to a family of branch circuits, not merely separate existence of each branch?
9. 9\.Does the final theorem state the form that a later user of the block\-encoding would actually need?

### 6\.3 Skeptical Review Protocol

The most useful review prompt was adversarial:

> Assume the argument below is wrong or incomplete\. Identify the strongest reasonable mathematical objections\. Focus on hidden assumptions, invalid norm inequalities, non\-normal matrix issues, block\-encoding normalization mismatches, precision allocation, access\-model ambiguity, and overclaims\. For each objection, propose a concrete fix or state why the claim should be weakened\.

This style of review was especially useful for catching hidden assumptions inLCUaccess models, ambiguity between scaled and unscaled error conventions, and overconfident extensions from one sign embedding to another\. However, skeptical review was still a heuristic\. A model\-generated objection was a candidate objection, not a proof of failure\. It had to be checked by the human researcher\.

## 7 Failure Modes and Controls

The case revealed several recurring failure modes\.

1. F1\.Superficial analogy\.AIMcould connect rational approximation, sign functions, projectors, and block\-encodings in many plausible ways\. Some connections were too generic to support a theorem\. The control was the human value gate: a route had to generate a reusable framework, not merely an analogy\.
2. F2\.Hidden analytic conditions\.The early Cayley–trapezoidal sign route omitted a nontrivial inversion\-contour\-validity condition\. The control was to ask exactly where the contour argument used invertibility and whether that condition followed from the desired assumptions\.
3. F3\.Non\-normal slippage\.Some proof sketches drifted toward spectral language that is unsafe for defective matrices\. The control was to restate claims usingFoVgaps, strip\-resolvent constants, or explicit projector certificates\.
4. F4\.Loose complexity\.First\-pass estimates often used a worst\-case conditioning parameter uniformly over all shifted nodes\. The control was manual recomputation of leading costs and a comparison among direct, factorized, scaled, and profile\-aware implementations\.
5. F5\.Error\-budget mismatch\.Approximation error, inverse\-implementation error, andLCUsynthesis error were sometimes merged too early\. The control was to keep deterministic and implementation errors separate until the final theorem\.
6. F6\.Overclaiming novelty\.Output of AIM sometimes made results sound more general, sharper than the evidence supported\. The control was human sign\-off for every contribution claim and every description of the AI role\.

The common control was to treatAIMoutput as a candidate\. It could accelerate the work, but it did not certify the work\.

## 8 Limitations and Future Directions

This report is a case study, not a statistical evaluation of AI\-assisted mathematics\. It analyzes one derivation\-heavy project and extracts workflow mechanisms from it\. The lessons should therefore be read as transferable patterns rather than universal claims\.

The workflow also has clear limitations\. Natural\-language derivations are not proofs by default\. A plausible argument can hide an assumption, use an invalid inequality, or conflate incompatible conventions\. AI\-generated complexity estimates can be directionally useful while still being asymptotically loose\. AI systems also cannot reliably judge novelty without careful literature verification and human standards of significance\. Finally, natural\-language skeptical review is not formal verification; it can reveal likely problems, but it cannot certify correctness\.

A promising future direction is a hybrid research environment\. Natural\-language AI can support exploration, drafting, and adversarial review\. Proof assistants can check selected local lemmas, such as block\-sign identities, resolvent factorizations, numerical\-range inequalities, and coefficient\-sum estimates\. Specialized complexity\-audit agents could maintain ledgers for oracle calls, normalizations, inverse precision,LCUweights, ancilla overhead, and final output normalization\.

For quantum algorithms, one useful next tool would be an assumption\-aware complexity ledger\. Whenever a theorem statement changes, such a system would update the assumptions, identify which proof modules depend on them, and recompute the effect on query complexity and block\-encoding normalization\. This would not replace human judgment, but it would make the human gate sharper\.

## 9 Conclusion

The sign\-embedding quantum\-algorithm project shows a specific way that a human\-AIco\-discovery workflow, withAIMas an important component, can accelerate mathematical research\. This acceleration occurred in significant part because the workflow began before the theorem was fixed\. A human researcher supplied the initial meta idea; human\-AIinteraction expanded the candidate space; the human researcher selected sign embedding as the valuable route;AIMhelped generate connections, theorem drafts, proof sketches, complexity expressions, and skeptical objections; and the human researcher verified, repaired, optimized, and integrated the surviving artifacts\.

The most accurate division of labor is therefore not "AI proved the theorem" or "the human merely checked it"\. Early human\-AIinteraction was useful when the task was to enlarge a mathematical neighborhood and generate candidate routes\.AIMwas strongest when the task was to connect a known identity to adjacent structures, draft theorem\-shaped statements, and produce first\-pass proof and complexity calculations\. The human researcher was decisive when the task required research judgment: originating the meta idea, selecting the sign route, rejecting a contour\-based proof with hidden validity conditions, separating query complexity from output normalization, and optimizing theorem targets through scaled and profile\-based implementations\.

The main lesson is that the unit of AI\-assisted mathematical research is often larger than a single proof attempt\. In derivation\-heavy fields such as quantum algorithms, the useful unit is an evolving research question: a broad direction that becomes a selected problem, then a theorem family, and finally a proof\-and\-complexity\-audited manuscript artifact\. In this case, discovery began while the right theorem targets were still being formed\.

## Acknowledgements

We thank Yanxing Huang and Yuanhang Liu for their valuable assistance during the early exploration ofAIM, and Yiqi Zhu, Xuanyu Lei, and Hanwei Fan for helpful early discussions on human\-AI interactive workflows\.

## References

- \[1\]D\. An, A\. M\. Childs, L\. Lin, and L\. Ying\(2026\)Laplace Transform–Based Quantum Eigenvalue Transformation via Linear Combination of Hamiltonian Simulation\.SIAM Journal on Computing55\(2\),pp\. 376–409\.External Links:[Document](https://dx.doi.org/10.1137/24M1720160),2411\.04010Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[2\]D\. An, A\. M\. Childs, and L\. Lin\(2026\)Quantum Algorithm for Linear Non\-unitary Dynamics with Near\-Optimal Dependence on All Parameters\.Communications in Mathematical Physics407\(1\),pp\. 19\.External Links:[Document](https://dx.doi.org/10.1007/s00220-025-05509-w),2312\.03916Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[3\]D\. An, J\. Liu, and L\. Lin\(2023\)Linear Combination of Hamiltonian Simulation for Nonunitary Dynamics with Optimal State Preparation Cost\.Physical Review Letters131\(15\),pp\. 150603\.External Links:[Document](https://dx.doi.org/10.1103/PhysRevLett.131.150603),2303\.01029Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[4\]D\. W\. Berry, A\. M\. Childs, R\. Cleve, R\. Kothari, and R\. D\. Somma\(2015\)Simulating hamiltonian dynamics with a truncated taylor series\.Physical Review Letters114\(9\),pp\. 090502\.External Links:[Document](https://dx.doi.org/10.1103/PhysRevLett.114.090502)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[5\]R\. Byers\(1987\)Solving the algebraic riccati equation with the matrix sign function\.Linear Algebra and Its Applications85,pp\. 267–279\.External Links:[Document](https://dx.doi.org/10.1016/0024-3795%2887%2990222-9)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[6\]A\. M\. Childs, R\. Kothari, and R\. D\. Somma\(2017\)Quantum algorithm for systems of linear equations with exponentially improved dependence on precision\.SIAM Journal on Computing46\(6\),pp\. 1920–1950\.External Links:[Document](https://dx.doi.org/10.1137/16M1087072)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[7\]L\. de Moura, S\. Kong, J\. Avigad, F\. van Doorn, and J\. von Raumer\(2015\)The Lean theorem prover \(system description\)\.InAutomated Deduction – CADE\-25,Lecture Notes in Computer Science, Vol\.9195,pp\. 378–388\.External Links:[Document](https://dx.doi.org/10.1007/978-3-319-21401-6%5F26)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[8\]A\. Fawzi, M\. Balog, A\. Huang, T\. Hubert, B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, F\. J\. R\. Ruiz, J\. Schrittwieser, G\. Swirszcz, D\. Silver, D\. Hassabis, and P\. Kohli\(2022\)Discovering faster matrix multiplication algorithms with reinforcement learning\.Nature610,pp\. 47–53\.External Links:[Document](https://dx.doi.org/10.1038/s41586-022-05172-4),[Link](https://doi.org/10.1038/s41586-022-05172-4)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[9\]T\. Feng, T\. H\. Trinh, G\. Bingham, D\. Hwang, Y\. Chervonyi, J\. Jung, J\. Lee, C\. Pagano, S\. Kim, F\. Pasqualotto, S\. Gukov, J\. N\. Lee, J\. Kim, K\. Hou, G\. Ghiasi, Y\. Tay, Y\. Li, C\. Kuang, Y\. Liu, H\. Lin, E\. Z\. Liu, N\. Nayakanti, X\. Yang, H\. Cheng, D\. Hassabis, K\. Kavukcuoglu, Q\. V\. Le, and T\. Luong\(2026\)Towards autonomous mathematics research\.arXiv preprint arXiv:2602\.10177\.External Links:2602\.10177,[Link](https://arxiv.org/abs/2602.10177)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1)\.
- \[10\]A\. E\. Ghareeb, B\. Chang, L\. Mitchener, A\. Yiu, C\. J\. Szostkiewicz, D\. Shved, G\. J\. Gyimesi, J\. M\. Laurent, S\. M\. Wright, M\. T\. Razzak, A\. D\. White, S\. C\. Finnemann, M\. M\. Hinks, and S\. G\. Rodriques\(2026\)A multi\-agent system for automating scientific discovery\.Nature\.Note:Published May 19, 2026External Links:[Document](https://dx.doi.org/10.1038/s41586-026-10652-y),[Link](https://doi.org/10.1038/s41586-026-10652-y)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px2.p1.1)\.
- \[11\]A\. Gilyén, Y\. Su, G\. H\. Low, and N\. Wiebe\(2019\)Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics\.InProceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing,pp\. 193–204\.External Links:[Document](https://dx.doi.org/10.1145/3313276.3316366)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[12\]J\. Gottweis, W\. Weng, A\. Daryin, T\. Tu, P\. Sirkovic, A\. Myaskovsky, G\. Glowaty, F\. Weissenberger, A\. Orlandi, D\. Popovici,et al\.\(2026\)Accelerating scientific discovery with co\-scientist\.Nature\.Note:Published May 19, 2026External Links:[Document](https://dx.doi.org/10.1038/s41586-026-10644-y),[Link](https://doi.org/10.1038/s41586-026-10644-y)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px2.p1.1)\.
- \[13\]A\. W\. Harrow, A\. Hassidim, and S\. Lloyd\(2009\)Quantum algorithm for linear systems of equations\.Physical Review Letters103\(15\),pp\. 150502\.External Links:[Document](https://dx.doi.org/10.1103/PhysRevLett.103.150502)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[14\]N\. J\. Higham\(2008\)Functions of matrices: theory and computation\.SIAM,Philadelphia, PA\.External Links:[Document](https://dx.doi.org/10.1137/1.9780898717778)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1),[§4\.2](https://arxiv.org/html/2606.24899#S4.SS2.p1.2)\.
- \[15\]X\. Huang and D\. An\(2025\)Fourier Transform\-Based Linear Combination of Hamiltonian Simulation\.arXiv preprint arXiv:2508\.19596\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2508.19596),2508\.19596,[Link](https://arxiv.org/abs/2508.19596)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[16\]T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom,et al\.\(2026\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature651,pp\. 607–613\.Note:Published online November 12, 2025External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y),[Link](https://doi.org/10.1038/s41586-025-09833-y)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[17\]C\. S\. Kenney and A\. J\. Laub\(1995\)The matrix sign function\.IEEE Transactions on Automatic Control40\(8\),pp\. 1330–1348\.External Links:[Document](https://dx.doi.org/10.1109/9.402226)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[18\]G\. Lample, T\. Lacroix, M\. Lachaux, A\. Rodriguez, A\. Hayat, T\. Lavril, G\. Ebner, and X\. Martinet\(2022\)HyperTree proof search for neural theorem proving\.InAdvances in Neural Information Processing Systems,Vol\.35,pp\. 26337–26349\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2022/hash/a8901c5e85fb8e1823bbf0f755053672-Abstract-Conference.html)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[19\]P\. Lancaster and L\. Rodman\(1995\)Algebraic riccati equations\.Oxford University Press,Oxford\.Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[20\]C\. Li, Z\. Lai, D\. An, J\. Hu, and Z\. Wen\(2025\)Advancing mathematical research via human\-AI interactive theorem proving\.arXiv preprint arXiv:2512\.09443\.External Links:2512\.09443,[Link](https://arxiv.org/abs/2512.09443)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px3.p1.1)\.
- \[21\]N\. Liu, Q\. Wang, M\. M\. Wilde, and Z\. Zhang\(2025\)Quantum algorithms for matrix geometric means\.npj Quantum Information11,pp\. 101\.External Links:[Document](https://dx.doi.org/10.1038/s41534-025-00973-7),2405\.00673Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[22\]Y\. Liu, Y\. Huang, Y\. Wang, P\. Li, and Y\. Liu\(2025\)AI mathematician: towards fully automated frontier mathematical research\.arXiv preprint arXiv:2505\.22451\.External Links:2505\.22451,[Link](https://arxiv.org/abs/2505.22451)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§1](https://arxiv.org/html/2606.24899#S1.p5.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px3.p1.1)\.
- \[23\]Y\. Liu, B\. Wang, P\. Li, and Y\. Liu\(2025\)AI mathematician as a partner in advancing mathematical discovery—a case study in homogenization theory\.arXiv preprint arXiv:2510\.26380\.External Links:2510\.26380,[Link](https://arxiv.org/abs/2510.26380)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px3.p1.1)\.
- \[24\]G\. H\. Low and I\. L\. Chuang\(2017\)Optimal hamiltonian simulation by quantum signal processing\.Physical Review Letters118\(1\),pp\. 010501\.External Links:[Document](https://dx.doi.org/10.1103/PhysRevLett.118.010501),1606\.02685Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[25\]G\. H\. Low and I\. L\. Chuang\(2019\)Hamiltonian simulation by qubitization\.Quantum3,pp\. 163\.External Links:[Document](https://dx.doi.org/10.22331/q-2019-07-12-163),1610\.06546Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[26\]G\. H\. Low and R\. D\. Somma\(2025\)Optimal Quantum Simulation of Linear Non\-Unitary Dynamics\.arXiv preprint arXiv:2508\.19238\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2508.19238),2508\.19238,[Link](https://arxiv.org/abs/2508.19238)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[27\]C\. Lu, C\. Lu, R\. T\. Lange, Y\. Yamada, S\. Hu, J\. Foerster, D\. Ha, and J\. Clune\(2026\)Towards end\-to\-end automation of AI research\.Nature651\(8107\),pp\. 914–919\.External Links:[Document](https://dx.doi.org/10.1038/s41586-026-10265-5),[Link](https://doi.org/10.1038/s41586-026-10265-5)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px2.p1.1)\.
- \[28\]I\. Novikau and I\. Joseph\(2025\)An Efficient Explicit Implementation of a Near\-Optimal Quantum Algorithm for Simulating Linear Dissipative Differential Equations\.arXiv preprint arXiv:2501\.11146\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2501.11146),2501\.11146,[Link](https://arxiv.org/abs/2501.11146)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[29\]OpenAI\(2026\-05\)An OpenAI model has disproved a central conjecture in discrete geometry\.Note:OpenAI Research MilestonePublished May 20, 2026External Links:[Link](https://openai.com/index/model-disproves-discrete-geometry-conjecture/)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[30\]S\. Polu and I\. Sutskever\(2020\)Generative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.External Links:2009\.03393,[Link](https://arxiv.org/abs/2009.03393)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[31\]J\. D\. Roberts\(1980\)Linear model reduction and solution of the algebraic riccati equation by use of the sign function\.International Journal of Control32\(4\),pp\. 677–687\.External Links:[Document](https://dx.doi.org/10.1080/00207178008922881)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[32\]B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, M\. Balog, M\. P\. Kumar, E\. Dupont, F\. J\. R\. Ruiz, J\. S\. Ellenberg, P\. Wang, O\. Fawzi, P\. Kohli, and A\. Fawzi\(2024\)Mathematical discoveries from program search with large language models\.Nature625\(7995\),pp\. 468–475\.External Links:[Document](https://dx.doi.org/10.1038/s41586-023-06924-6),[Link](https://doi.org/10.1038/s41586-023-06924-6)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[33\]P\. Schleich, T\. Kharazi, X\. Li, J\. Liu, A\. Aspuru\-Guzik, and N\. Wiebe\(2025\)Arbitrary Boundary Conditions and Constraints in Quantum Algorithms for Differential Equations via Penalty Projections\.arXiv preprint arXiv:2506\.21751\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2506.21751),2506\.21751,[Link](https://arxiv.org/abs/2506.21751)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[34\]R\. D\. Somma, G\. H\. Low, D\. W\. Berry, and R\. Babbush\(2025\)Quantum algorithm for linear matrix equations\.Note:arXiv:2508\.02822External Links:2508\.02822Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[35\]S\. Takahira, A\. Ohashi, T\. Sogabe, and T\. S\. Usuda\(2022\)Quantum algorithms based on the Block\-Encoding framework for matrix functions by contour integrals\.Quantum Information and Computation22\(11–12\),pp\. 965–979\.External Links:[Document](https://dx.doi.org/10.26421/QIC22.11-12-4),2106\.08076Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[36\]T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong\(2024\)Solving olympiad geometry without human demonstrations\.Nature625\(7995\),pp\. 476–482\.External Links:[Document](https://dx.doi.org/10.1038/s41586-023-06747-5),[Link](https://doi.org/10.1038/s41586-023-06747-5)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p1.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px1.p1.1)\.
- \[37\]Y\. Wang and J\. Liu\(2026\)Sign embedding quantum algorithms for matrix equations and matrix functions\.arXiv preprint arXiv:2604\.25333\.External Links:2604\.25333,[Link](https://arxiv.org/abs/2604.25333)Cited by:[§1](https://arxiv.org/html/2606.24899#S1.p3.1),[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1),[Figure 3](https://arxiv.org/html/2606.24899#S3.F3),[Figure 3](https://arxiv.org/html/2606.24899#S3.F3.3.2),[§3\.3](https://arxiv.org/html/2606.24899#S3.SS3.p1.1),[§4\.1](https://arxiv.org/html/2606.24899#S4.SS1.p1.4)\.
- \[38\]S\. Yang and J\. Liu\(2025\)Circuit\-Efficient Randomized Quantum Simulation of Non\-Unitary Dynamics with Observable\-Driven and Symmetry\-Aware Designs\.arXiv preprint arXiv:2509\.08030\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2509.08030),2509\.08030,[Link](https://arxiv.org/abs/2509.08030)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px4.p1.1)\.
- \[39\]D\. Zheng, I\. von Glehn, Y\. Zwols, I\. Beloshapka, L\. Buesing, D\. M\. Roy, M\. Wattenberg, B\. Georgiev, T\. Schmidt, A\. Cowie, F\. Viegas, D\. Kanevsky, V\. Kahlon, H\. Maennel, S\. Alj, G\. Holland, A\. Davies, and P\. Kohli\(2026\)AI co\-mathematician: accelerating mathematicians with agentic AI\.arXiv preprint arXiv:2605\.06651\.External Links:2605\.06651,[Link](https://arxiv.org/abs/2605.06651)Cited by:[§2](https://arxiv.org/html/2606.24899#S2.SS0.SSS0.Px3.p1.1)\.

## Appendix AExperimental Results

This section records representative interaction traces between the human researcher andAIMv2\. Given a human input,AIMv2 first judges whether the problem is sufficiently well specified\. If the input is vague, under\-specified, or still at the level of a broad research intuition,AIMv2 enters a divergent exploration mode: it expands the input into a set of more concrete and related candidate questions, directions, or problem formulations for the human researcher to inspect and select from\. If the input is already clearly defined,AIMv2 enters a problem\-solving mode: it incrementally explores the problem, proposes intermediate lemmas that may help solve it, generates proofs and checks for these lemmas, and records the validated or partially validated results in a theorem graph\. Thus, the traces below should be read not merely as raw dialogue, but as examples of a human\-gated interaction loop in whichAIMv2 alternates between problem clarification, route expansion, theorem formation, proof generation, verification, and theorem\-graph memory\.

Note on formatting\.The originalAIMoutputs were in JSON format\. For readability, AI was used here only to convert the records into LaTeX format, without changing their substantive content\.

User Entry \(Human’s Prompt\)I am exploring the following meta idea: use rational approximation as a design principle for quantum algorithms, especially for algorithms whose outputs are operators or block\-encodings rather than just quantum states\.Please brainstorm concrete research directions at the interface of numerical linear algebra, matrix functions, matrix equations, and block\-encoding/QSVT\-based quantum algorithms\. For each direction, identify:1\.the classical analytic representation that might be useful, such as rational approximations, resolvent formulas, contour integrals, matrix sign functions, or spectral projectors;2\.the target quantum output model;3\.the likely quantum primitives needed;4\.what would be genuinely new compared with standard HHL/QSVT/contour\-integral approaches;5\.the main technical obstacles\.Do not try to force a single answer\. Give several candidate projects and rank them by conceptual unity, feasibility, and potential novelty\.

Assistant Entry \(AIM’s Response\)Below are candidate projects organized around the principle:Instead of viewing QSVT only as a way to implement polynomial approximations to scalar functions of spectra, use rational/meromorphic representations from numerical linear algebra as the primary design object, and compile them into quantum primitives that output block\-encodings, projectors, superoperators, or compressed operator data\.I rank each direction by:•Conceptual unity: how cleanly the rational\-approximation idea drives the algorithm\.•Feasibility: whether current block\-encoding/QSVT/LCU primitives plausibly suffice\.•Novelty: how different it is from standard HHL/QSVT/contour\-integral algorithms\.Scores are rough, from 1 to 5\.#### High\-level ranking #### 1\. Rational block\-encodings of matrix functions via shifted resolvents ##### Core idea Given a matrix functionf​\(A\)f\(A\), use a rational approximationf​\(A\)≈r​\(A\)=c0​I\+∑j=1mcjA−zj​If\(A\)\\approx r\(A\)=c\_\{0\}I\+\\sum\_\{j=1\}^\{m\}\\frac\{c\_\{j\}\}\{A\-z\_\{j\}I\}or, for HermitianAA,f​\(A\)≈c0​I\+∑j=1mcj​\(A−zj​I\)−1\.f\(A\)\\approx c\_\{0\}I\+\\sum\_\{j=1\}^\{m\}c\_\{j\}\(A\-z\_\{j\}I\)^\{\-1\}\.Instead of implementingffby a high\-degree QSVT polynomial, implement a linear combination of shifted inverses\. ##### 1\.1\. Classical analytic representation Useful representations include:•partial fraction expansions;•Zolotarev rational approximations;•Pade and Chebyshev rational approximants;•Cauchy integral formula:f​\(A\)=12​π​i​∫Γf​\(z\)​\(z​I−A\)−1​𝑑z;f\(A\)=\\frac\{1\}\{2\\pi i\}\\int\_\{\\Gamma\}f\(z\)\(zI\-A\)^\{\-1\}\\,dz;•rational approximations tosign⁡\(A\)\\operatorname\{sign\}\(A\),A−1/2A^\{\-1/2\},log⁡A\\log A,e−t​Ae^\{\-tA\}, Fermi\-Dirac functions, etc\. ##### 1\.2\. Target quantum output model The natural output is a block\-encoding ofr​\(A\)r\(A\), hence off​\(A\)f\(A\):Ur=\(r​\(A\)/α∗∗∗\)\.U\_\{r\}=\\begin\{pmatrix\}r\(A\)/\\alpha&\*\\\\ \*&\*\\end\{pmatrix\}\.This is stronger than producingf​\(A\)​\|b⟩f\(A\)\\ket\{b\}\. It gives reusable operator access tof​\(A\)f\(A\)\.Possible output variants:•block\-encoding off​\(A\)f\(A\);•normalized density operator proportional tof​\(A\)f\(A\), whenf​\(A\)⪰0f\(A\)\\succeq 0;•block\-encoding of a preconditionerr​\(A\)r\(A\);•compressed representation using a small ancilla register indexing poles\. ##### 1\.3\. Likely quantum primitives •Block\-encoding ofAA\.•Block\-encoding or QLSA for shifted systemsA−zj​IA\-z\_\{j\}I\.•LCU over the poleszjz\_\{j\}\.•Oblivious amplitude amplification\.•Variable\-time amplitude amplification if the shifted systems have different condition numbers\.•QSVT for implementing inverses or regularized inverses\.•Possibly Hamiltonian simulation ifAAis Hermitian and resolvents are represented by Laplace transforms\. ##### 1\.4\. What is genuinely new? Standard QSVT is polynomial\-first\. This would be rational\-first\.The novelty would be a systematic theory comparing:polynomial degree needed for​fversusnumber and conditioning of shifted resolvent calls\.\\text\{polynomial degree needed for \}f\\quad\\text\{versus\}\\quad\\text\{number and conditioning of shifted resolvent calls\}\.For functions with singularities near the spectrum, rational approximations can be exponentially better than polynomial approximations\. The new contribution would be to translate classical rational approximation theory into end\-to\-end block\-encoding complexity bounds\.Especially interesting targets:•A−1/2A^\{\-1/2\};•log⁡A\\log A;•sign⁡\(A\)\\operatorname\{sign\}\(A\);•spectral projectors;•Fermi\-Dirac functions;•fractional powersAαA^\{\\alpha\};•resolvent\-based Green’s functions\. ##### 1\.5\. Main obstacles •Shifted inverses may be ill\-conditioned whenzjz\_\{j\}is close tospec⁡\(A\)\\operatorname\{spec\}\(A\)\.•LCU normalization may scale with∑j\|cj\|​‖\(A−zj​I\)−1‖\\sum\_\{j\}\|c\_\{j\}\|\\\|\(A\-z\_\{j\}I\)^\{\-1\}\\\|, which can erase the rational\-approximation advantage\.•Complex shifts require non\-Hermitian block\-encodings or Hermitian embeddings\.•Error must be controlled uniformly in operator norm, not just pointwise on eigenvalues\.•For nonnormal matrices, resolvent norms can be huge due to pseudospectral effects\. ##### Evaluation This is probably the cleanest starting point\. It is conceptually unified, feasible, and potentially impactful\. #### 2\. Quantum algorithms for Lyapunov and Sylvester equations using rational Krylov ideas ##### Core idea Solve matrix equations such asA​X\+X​B=C,AX\+XB=C,or the continuous Lyapunov equationA​X\+X​A†=−Q,AX\+XA^\{\\dagger\}=\-Q,not by vectorizing and applying HHL to the huge linear system, but by using integral or rational representations of the solution operator\.For example, ifAAis stable,X=∫0∞et​A​Q​et​A†​𝑑t\.X=\\int\_\{0\}^\{\\infty\}e^\{tA\}Qe^\{tA^\{\\dagger\}\}\\,dt\.There are also rational approximations of the formX≈∑j=1mωj​\(A−σj​I\)−1​Q​\(A†−σj¯​I\)−1\.X\\approx\\sum\_\{j=1\}^\{m\}\\omega\_\{j\}\(A\-\\sigma\_\{j\}I\)^\{\-1\}Q\(A^\{\\dagger\}\-\\overline\{\\sigma\_\{j\}\}I\)^\{\-1\}\.This mirrors rational Krylov and ADI methods in classical numerical linear algebra\. ##### 2\.1\. Classical analytic representation Useful representations:•Laplace integral for Lyapunov equations;•Cauchy integral formula for Sylvester equations;•alternating\-direction implicit, ADI, iteration:Xk\+1=Φk​\(A\)​Xk​Φk​\(A\)†\+correction;X\_\{k\+1\}=\\Phi\_\{k\}\(A\)X\_\{k\}\\Phi\_\{k\}\(A\)^\{\\dagger\}\+\\text\{correction\};•rational Krylov approximation;•separable expansions of the kernel1/\(λ\+μ\)1/\(\\lambda\+\\mu\);•contour integral representation:X=1\(2​π​i\)2​∫ΓA∫ΓB1z\+w​\(z​I−A\)−1​C​\(w​I−B\)−1​𝑑z​𝑑w\.X=\\frac\{1\}\{\(2\\pi i\)^\{2\}\}\\int\_\{\\Gamma\_\{A\}\}\\int\_\{\\Gamma\_\{B\}\}\\frac\{1\}\{z\+w\}\(zI\-A\)^\{\-1\}C\(wI\-B\)^\{\-1\}\\,dz\\,dw\. ##### 2\.2\. Target quantum output model Several interesting output models:1\.Block\-encoding ofXX\.2\.Purification ofX/Tr⁡XX/\\operatorname\{Tr\}XwhenX⪰0X\\succeq 0\.3\.Block\-encoding of the solution superoperatorℒ−1:C↦X,\\mathcal\{L\}^\{\-1\}:C\\mapsto X,whereℒ​\(X\)=A​X\+X​B\.\\mathcal\{L\}\(X\)=AX\+XB\.1\.Low\-rank factor block\-encodingX≈Z​Z†,X\\approx ZZ^\{\\dagger\},whereZZis constructed from shifted resolvent actions\.The fourth output model is especially natural because classical Lyapunov solvers often produce low\-rank factors\. ##### 2\.3\. Likely quantum primitives •Block\-encodings ofAA,BB, andQQ\.•Shifted linear\-system solvers forA−σj​IA\-\\sigma\_\{j\}IandB−τj​IB\-\\tau\_\{j\}I\.•LCU over pole pairs\(σj,τj\)\(\\sigma\_\{j\},\\tau\_\{j\}\)\.•Tensor\-product block\-encodings for vectorized operators:I⊗A\+BT⊗I\.I\\otimes A\+B^\{T\}\\otimes I\.•Density matrix preparation ifQ⪰0Q\\succeq 0\.•Quantum singular value transformation for regularized inverses\.•Trace estimation for normalization\. ##### 2\.4\. What is genuinely new? A naive quantum approach vectorizesXXand applies HHL to a linear system of dimensionn2n^\{2\}\. That misses the structure of matrix equations\.A genuinely new approach would exploit the separability of rational approximations:1λ\+μ≈∑j=1mωj\(λ−σj\)​\(μ−τj\)\.\\frac\{1\}\{\\lambda\+\\mu\}\\approx\\sum\_\{j=1\}^\{m\}\\frac\{\\omega\_\{j\}\}\{\(\\lambda\-\\sigma\_\{j\}\)\(\\mu\-\\tau\_\{j\}\)\}\.This could yield algorithms whose complexity depends on the rational separation rankmm, spectral separation, and block\-encoding costs forAAandBB, rather than on the condition number of the full Kronecker\-sum operator\.This would connect quantum algorithms to classical ADI and rational Krylov theory\. ##### 2\.5\. Main obstacles •Need a clean output model forXX; full classical description is impossible\.•The solutionXXcan be dense and high\-rank even whenQQis simple\.•Normalization may depend on‖X‖\\\|X\\\|,Tr⁡X\\operatorname\{Tr\}X, or an LCU coefficient sum that is hard to estimate\.•Stability regions and spectral separation matter strongly\.•Non\-normality ofAAcan make rational resolvent bounds much worse\.•For positive semidefiniteXX, preparing a purification may be easier than block\-encoding; the right model must be chosen carefully\. ##### Evaluation This is one of the most promising directions because it is structurally different from HHL and directly imports powerful numerical linear algebra ideas\.\[… The response then elaborated each candidate direction in the same format: analytic representation, target output model, quantum primitives, novelty, and obstacles\. These detailed elaborations are omitted because the main text uses only the route map and ranking structure\.\] #### Recommended project clusters #### Cluster A: Rational block\-encoding theory This is the foundational cluster\.Projects:1\.Rational block\-encodings off​\(A\)f\(A\)\.2\.Rational approximations for fractional powers\.3\.Matrix logarithm and inverse square root\.4\.Compiler for rational approximations\.Main deliverable:A theorem converting a rational approximationr​\(x\)=c0\+∑j=1mcjx−zjr\(x\)=c\_\{0\}\+\\sum\_\{j=1\}^\{m\}\\frac\{c\_\{j\}\}\{x\-z\_\{j\}\}into a block\-encoding ofr​\(A\)r\(A\), with complexity depending explicitly on pole locations, coefficientℓ1\\ell\_\{1\}\-norm, shifted condition numbers, and target error\.This would give a rigorous backbone for the broader program\. #### Cluster B: Rational filters and projectors Projects:1\.Spectral projectors via rational filters\.2\.Matrix sign and stable subspaces\.3\.Quantum FEAST\-style algorithms\.4\.Green’s function and spectral density operators\.Main deliverable:A quantum rational\-filter framework that outputs block\-encodings of spectral projectors or approximate projectors, with complexity competitive against polynomial QSVT in small\-gap regimes\.This cluster is conceptually clean and application\-rich\. #### Cluster C: Matrix equations as rational operator functions Projects:1\.Lyapunov/Sylvester equations\.2\.ADI\-inspired quantum algorithms\.3\.Bivariate separable rational approximations\.4\.Riccati equations\.Main deliverable:Quantum algorithms for structured matrix equations that avoid black\-box vectorization and instead exploit separable rational approximations of kernels such as1λ\+μ\.\\frac\{1\}\{\\lambda\+\\mu\}\.This is probably the most novel cluster, but also technically harder\. #### Cluster D: Rational preconditioners and reduced operators Projects:1\.Quantum rational preconditioners\.2\.Schur complements\.3\.Effective Hamiltonians\.4\.Domain decomposition\.Main deliverable:Reusable block\-encoded approximate inverses, Schur complements, or effective operators for downstream quantum algorithms\.This is potentially very impactful if one can define a convincing reuse model\. #### Most promising individual projects #### Project 1: Rational block\-encoding theorem for Stieltjes functions Focus on functions of the formf​\(A\)=∫0∞\(A\+t​I\)−1​𝑑μ​\(t\),f\(A\)=\\int\_\{0\}^\{\\infty\}\(A\+tI\)^\{\-1\}\\,d\\mu\(t\),includingA−α,log⁡A,A−1/2\.A^\{\-\\alpha\},\\quad\\log A,\\quad A^\{\-1/2\}\.These have positive\-weight resolvent representations forA≻0A\\succ 0\.Why this is good:•Strong classical approximation theory\.•Positive weights reduce LCU cancellation issues\.•Shifted systemsA\+t​IA\+tIare better conditioned thanAAfort\>0t\>0\.•Natural block\-encoding output\.•Clear comparison to QSVT\.Potential theorem shape:Given a block\-encoding ofA⪰λmin​IA\\succeq\\lambda\_\{\\min\}I, a quadrature rulef​\(A\)≈∑j=1mωj​\(A\+tj​I\)−1,f\(A\)\\approx\\sum\_\{j=1\}^\{m\}\\omega\_\{j\}\(A\+t\_\{j\}I\)^\{\-1\},and block\-encodings of\(A\+tj​I\)−1\(A\+t\_\{j\}I\)^\{\-1\}, one obtains a block\-encoding off​\(A\)f\(A\)with normalization approximatelyα∼∑jωj​‖\(A\+tj​I\)−1‖\.\\alpha\\sim\\sum\_\{j\}\\omega\_\{j\}\\\|\(A\+t\_\{j\}I\)^\{\-1\}\\\|\.The main technical goal is to choose quadrature nodes and weights minimizing this quantum cost, not merely the classical approximation error\. #### Project 2: Quantum ADI for Lyapunov equations Target:A​X\+X​A†\+Q=0\.AX\+XA^\{\\dagger\}\+Q=0\.Classical low\-rank ADI givesX≈Z​Z†,X\\approx ZZ^\{\\dagger\},where columns ofZZare generated by shifted solves\.Quantum version:•input: block\-encoding or purification ofQ=B​B†Q=BB^\{\\dagger\};•output: block\-encoding or purification ofX≈Z​Z†X\\approx ZZ^\{\\dagger\};•use shifted solves\(A\+pj​I\)−1\(A\+p\_\{j\}I\)^\{\-1\};•choose ADI shifts using rational approximation theory\.What is new:This would be a genuine quantum analogue of one of the central matrix\-equation solvers in numerical linear algebra, not just HHL on a Kronecker sum\.Main challenge:Define and implement the low\-rank factorZZquantumly without needing to classically enumerate its columns\. #### Project 3: Quantum FEAST/projector algorithm Target:P=12​π​i​∫Γ\(z​I−A\)−1​𝑑z\.P=\\frac\{1\}\{2\\pi i\}\\int\_\{\\Gamma\}\(zI\-A\)^\{\-1\}\\,dz\.Output:•block\-encoding ofPP;•reflection2​P−I2P\-I;•state sampler fromrange⁡\(P\)\\operatorname\{range\}\(P\);•block\-encoding ofP​A​PPAP\.What is new:Quantum phase estimation can project onto eigenvalue intervals, and QSVT can implement polynomial filters, but a rational FEAST\-style projector could have sharper windows and direct compatibility with contour methods\.Main challenge:Resolvent costs near the contour and LCU normalization\. #### Project 4: Rational preconditioner block\-encodings Target:ConstructM≈A−1M\\approx A^\{\-1\}as a reusable block\-encoding\.Novelty:Instead of treating preconditioning as a hidden improvement to HHL, make the preconditioner the output\.Possible use case:If many systemsA​xi=biAx\_\{i\}=b\_\{i\}or many downstream functions ofAAmust be computed, the cost of buildingMMcan be amortized\.Main challenge:Prove advantage over simply applying QSVT inverse each time\. #### Project 5: Non\-Hermitian rational functional calculus Target:For nonnormalAA,f​\(A\)=12​π​i​∫Γf​\(z\)​\(z​I−A\)−1​𝑑z\.f\(A\)=\\frac\{1\}\{2\\pi i\}\\int\_\{\\Gamma\}f\(z\)\(zI\-A\)^\{\-1\}\\,dz\.Output:•block\-encoding off​\(A\)f\(A\);•Riesz spectral projector;•pseudospectral diagnostic\.Novelty:This would broaden quantum matrix\-function algorithms beyond Hermitian or singular\-value transformations\.Main challenge:Complexity must depend on pseudospectral quantities, and these may be large\. #### Cross\-cutting technical questions #### 1\. What is the correct quantum cost model for rational approximants? Classically, one minimizes approximation error or number of poles\. Quantumly, the cost should include:Cost​\(r\)≈∑j\|cj\|⋅Cost​\(\(A−zj​I\)−1\)\\text\{Cost\}\(r\)\\approx\\sum\_\{j\}\|c\_\{j\}\|\\cdot\\text\{Cost\}\\big\(\(A\-z\_\{j\}I\)^\{\-1\}\\big\)or, more accurately, an LCU\-normalized version involvingαr=\|c0\|\+∑j\|cj\|​αj,\\alpha\_\{r\}=\|c\_\{0\}\|\+\\sum\_\{j\}\|c\_\{j\}\|\\alpha\_\{j\},whereαj\\alpha\_\{j\}is the block\-encoding normalization of\(A−zj​I\)−1\(A\-z\_\{j\}I\)^\{\-1\}\.Thus the best classical rational approximant may not be the best quantum rational approximant\.This is a major research theme\. #### 2\. Can pole locations be optimized for quantum implementation cost? Classical pole optimization focuses on uniform approximation\. Quantumly, poles near the spectrum are expensive because shifted systems become ill\-conditioned\.So one wants to solve a constrained rational approximation problem:mincj,zj⁡\[approximation error\+λ⋅quantum implementation cost\]\.\\min\_\{c\_\{j\},z\_\{j\}\}\\left\[\\text\{approximation error\}\+\\lambda\\cdot\\text\{quantum implementation cost\}\\right\]\.This could be a genuinely new bridge between rational approximation and quantum algorithm design\. #### 3\. When do rational methods beat polynomial QSVT? For HermitianAA, QSVT can implement many functions nearly optimally in polynomial degree\. Rational methods are compelling only if the savings in approximation order survive the cost of shifted inverses\.Promising regimes:•functions with poles or branch points near the spectral domain;•spectral projectors with tiny gaps;•Stieltjes functions;•fractional powers;•matrix equations with separable rational kernels;•non\-Hermitian problems where QSVT is less directly applicable\. #### 4\. How should one handle complex shifts? Forz=a\+i​bz=a\+ib, one needs to implement\(A−z​I\)−1\.\(A\-zI\)^\{\-1\}\.IfAAis Hermitian, this can be reduced to real block systems such as\(A−a​Ib​I−b​IA−a​I\)−1\.\\begin\{pmatrix\}A\-aI&bI\\\\ \-bI&A\-aI\\end\{pmatrix\}^\{\-1\}\.Alternatively, one can pair conjugate poles to maintain Hermiticity:c​\(A−z​I\)−1\+c¯​\(A−z¯​I\)−1\.c\(A\-zI\)^\{\-1\}\+\\overline\{c\}\(A\-\\overline\{z\}I\)^\{\-1\}\.A good project would formalize efficient block\-encodings for conjugate\-paired rational terms\. #### 5\. What output model is most useful? Possible output models differ substantially:1\.Block\-encodingoff​\(A\)f\(A\): reusable and composable\.2\.Stateproportional tof​\(A\)​\|b⟩f\(A\)\\ket\{b\}: standard HHL\-like model\.3\.Density operatorproportional tof​\(A\)f\(A\): useful whenf​\(A\)⪰0f\(A\)\\succeq 0\.4\.Projector/reflection: useful for subspace algorithms\.5\.Quantum channelrepresenting a solution mapC↦XC\\mapsto X\.6\.Low\-rank factor block\-encoding: natural for Lyapunov and covariance equations\.The most distinctive angle is to emphasize block\-encodings, projectors, and solution superoperators rather than merely states\. #### Suggested near\-term research plan #### Phase 1: Foundational theorem Develop a theorem of the form:Given a block\-encoding ofAAand rational approximationr​\(x\)=c0\+∑j=1mcj​\(x−zj\)−1,r\(x\)=c\_\{0\}\+\\sum\_\{j=1\}^\{m\}c\_\{j\}\(x\-z\_\{j\}\)^\{\-1\},construct a block\-encoding ofr​\(A\)r\(A\), with error and cost bounded in terms of:•pole locationszjz\_\{j\};•coefficientscjc\_\{j\};•shifted condition numbersκ​\(A−zj​I\)\\kappa\(A\-z\_\{j\}I\);•LCU normalization;•target errorε\\varepsilon;•block\-encoding normalization ofAA\.This becomes the "rational approximation to block\-encoding" compiler theorem\. #### Phase 2: Demonstration cases Choose two or three functions where rational approximation is known to be superior:•A−1/2A^\{\-1/2\};•A−αA^\{\-\\alpha\};•log⁡A\\log A;•spectral projector𝟏\[a,b\]​\(A\)\\mathbf\{1\}\_\{\[a,b\]\}\(A\);•Fermi\-Dirac function\.Compare to QSVT polynomial approximations\. #### Phase 3: Matrix equation application Apply the framework to the Lyapunov equation:A​X\+X​A†\+Q=0\.AX\+XA^\{\\dagger\}\+Q=0\.Try to output either:•a purification ofX/Tr⁡XX/\\operatorname\{Tr\}X, or•a block\-encoding ofXX, or•a low\-rank factor block\-encoding\.This would demonstrate that the rational viewpoint naturally handles operator\-valued outputs\. #### My top recommendation If you want a coherent and publishable program, I would start with: #### "Rational approximation as a block\-encoding compiler for Stieltjes matrix functions and spectral projectors\." This includes:A−α,A−1/2,log⁡A,sign⁡\(A\),𝟏Ω​\(A\)\.A^\{\-\\alpha\},\\quad A^\{\-1/2\},\\quad\\log A,\\quad\\operatorname\{sign\}\(A\),\\quad\\mathbf\{1\}\_\{\\Omega\}\(A\)\.Then extend to: #### "Quantum ADI and rational Krylov methods for Lyapunov/Sylvester equations\." The first project builds the machinery\. The second demonstrates that the machinery reaches beyond standard HHL/QSVT by producing structured operator\-valued solutions to matrix equations\.

User Entry \(Human’s Prompt\)I would like to explore a possible research program at the intersection of rational approximation, matrix functions, matrix equations, and quantum algorithms\.The starting idea is to use augmented\-matrix identities, in the spirit of Higham’s matrix sign function techniques, to reduce several structured linear\-algebraic problems—such as Sylvester equations, generalized Lyapunov equations, generalized Sylvester equations, inverse square roots, square roots, geometric means, or related matrix\-function problems—to the extraction of a specific block, or a projector block, of the matrix sign function of a larger block matrix\. More generally, I am also interested in whether closely related piecewise analytic matrix functions could play the same organizing role\.Please investigate this idea systematically\.First, identify the relevant classical sign\-function or augmented\-matrix identities\. For each target problem, derive the block matrix whose matrix sign, spectral projector, or related analytic function contains the desired solution or matrix function as a block\. State the required spectral separation, half\-plane separation, field\-of\-values, or strip\-resolvent assumptions clearly\.Second, examine how the matrix sign function can be represented or approximated by rational functions\. In particular, study whether Cauchy contour integrals, real\-line sign integral formulas, logarithmic\-sinc quadrature, or other rational approximation schemes can express the sign function as a finite linear combination of shifted resolvents of the form\(zI \- M\)^\{\-1\}\.Where possible, exploit the block structure of the augmented matrix to factor these resolvents into shifted inverses of the original input matrices\.Third, design a quantum algorithmic framework that turns these rational\-resolvent formulas into block\-encodings of the desired target operators\. The framework may use LCU, QSVT\-based matrix inversion, quantum linear system primitives, Hamiltonian simulation, or related block\-encoding techniques\. The goal is to formulate a reusable "rational–resolvent quantum compiler" that takes a sign\-embedding identity and a rational approximation scheme as input, and outputs a block\-encoding of the target block\.Please give theorem\-level statements whenever possible\. In particular, specify:1\.the input access model, such as block\-encodings of the coefficient matrices;2\.the augmented matrix and the sign or projector identity;3\.the rational or contour\-integral approximation and its deterministic error;4\.the quantum implementation of the shifted resolvents;5\.the LCU normalization or block\-encoding normalization;6\.the total query complexity;7\.how deterministic approximation error and quantum implementation error are combined\.Finally, compare this framework with existing quantum algorithms for Sylvester equations, Lyapunov equations, matrix functions, and contour\-integral\-based matrix\-function algorithms\. Identify regimes where the sign\-embedding/rational\-resolvent approach gives a genuine structural or complexity advantage, and also identify regimes where it may be worse, less practical, or dependent on hard\-to\-certify quantities such as non\-normal resolvent bounds, field\-of\-values gaps, nodewise inverse profiles, or projector invertibility gaps\.Be critical rather than promotional: I want a mathematically rigorous roadmap, including both advantages and limitations, not just a high\-level proposal\.

Theorem\-graph note\.WhenAIMv2 works on a problem, it incrementally constructs theorem\-like intermediate results that may support the solution, and organizes them into a theorem graph according to their dependency relations\. In the record below,Reviewsdenotes the number of timesAIMv2 checked the stated theorem and its proof;Dependenciesrecords which earlier theorem\-graph entries the result depends on; andCommentsrecords review comments produced whenAIMv2 checked the theorem or proof\.

Assistant Entry \(AIM’s Response\)### Theorem Graph Entry 0 •Type:context•Reviews:0•Derivations:1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15##### Statement Research context: investigate augmented\-matrix sign/projector identities and rational\-resolvent quantum compilers for structured matrix functions and matrix equations, including assumptions, rational approximation error, block\-encoding implementation, complexity, and limitations\. ##### Proof Source: user request in this conversation\. The user asked for a systematic investigation of a research program using augmented\-matrix identities, especially Higham\-style matrix sign techniques, to reduce Sylvester, Lyapunov, generalized matrix equations, inverse square roots, square roots, geometric means, and related matrix\-function problems to extracting blocks or projector blocks of the matrix sign or related piecewise analytic functions of larger matrices, and to compile rational/resolvent formulas into quantum block\-encodings\. ### Theorem Graph Entry 1 •Type:theorem•Reviews:3•Dependencies:0##### Statement Triangular sign/Sylvester identity: Ifs​p​e​c​\(A\)spec\(A\)lies in the open right half\-plane ands​p​e​c​\(B\)spec\(B\)lies in the open left half\-plane, then forM=\[\[A,C\],\[0,B\]\],s​i​g​n​\(M\)=\[\[I,2​X\],\[0,−I\]\]M=\[\[A,C\],\[0,B\]\],sign\(M\)=\[\[I,2X\],\[0,\-I\]\], where X is the unique solution of AX−X​B=CX\-XB=C\. Equivalently the right\-half\-plane Riesz projector P\_\+=\(I\+sign\(M\)\)/2I\+sign\(M\)\)/2has off\-diagonal block X\. ##### Proof Let f be analytic on neighborhoods of two disjoint spectral sets containings​p​e​c​\(A\)spec\(A\)ands​p​e​c​\(B\)spec\(B\)\. The standard holomorphic functional calculus for block triangular matrices givesf​\(\[\[A,C\],\[0,B\]\]\)=\[\[f​\(A\),Y\],\[0,f​\(B\)\]\]f\(\[\[A,C\],\[0,B\]\]\)=\[\[f\(A\),Y\],\[0,f\(B\)\]\], withY=\(1/\(2πY=\(1/\(2\\pi\{\}i\)\)∫\\int\_Γ​f​\(z\)\\Gamma\{\}f\(z\)\(zI\-A\)−1C\(zI−B\)−1A\)^\{\-1\}C\(zI\-B\)^\{\-1\}dz for a contour enclosings​p​e​c​\(A\)spec\(A\)ands​p​e​c​\(B\)spec\(B\)\. Equivalently, ifs​p​e​c​\(A\)spec\(A\)ands​p​e​c​\(B\)spec\(B\)are disjoint, Y is the unique solution of AY−Y​B=f​\(A\)​C−C​f​\(B\)Y\-YB=f\(A\)C\-Cf\(B\)\. For f=sign, assumings​p​e​c​\(A\)spec\(A\)is in the open right half\-plane ands​p​e​c​\(B\)spec\(B\)in the open left half\-plane,f​\(A\)=If\(A\)=Iandf​\(B\)=−If\(B\)=\-I, hence AY−Y​B=2​CY\-YB=2C\. If X is the unique solution of AX−X​B=CX\-XB=C, thenY=2​XY=2X\. The projector identity follows from P\_\+=\(II\+sign\)/2\. ### Theorem Graph Entry 2 •Type:theorem•Reviews:0•Dependencies:0##### Statement Rational\-resolvent block\-encoding compiler: If a target operator T is a contraction\-selected block ofg​\(M\),r​\(M\)=c0​I\+Σ​cjj=1m​\(zj​I−M\)−1g\(M\),r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}\(z\_\{j\}I\-M\)^\{\-1\}approximatesg​\(M\)g\(M\)withinδdet\\delta\{\}\_\{\\mathrm\{det\}\}, and each shifted resolvent has anαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encoding usingQjQ\_\{j\}queries, then T has a block\-encoding with normalizationα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and error at mostδ\+detΣ\|jcj\|η\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. In the basic LCU implementation the controlled\-query complexity is𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)per use of thisα\\alpha\{\}\-normalized block\-encoding, up to coefficient\-preparation overhead\. ##### Proof AssumeUjU\_\{j\}is anαj\\alpha\{\}\_\{j\}\-normalized block\-encoding ofRjR\_\{j\}with scaled error∥top\(Uj\)−Rj/α∥j≤ηj\\lVert top\(U\_\{j\}\)\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}\. Thenα​tj​o​p​\(Uj\)\\alpha\{\}\_\{j\}top\(U\_\{j\}\)approximatesRjR\_\{j\}with unnormalized error at mostαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. Standard LCU over the normalized termscj​α​tj​o​p​\(Uj\)c\_\{j\}\\alpha\{\}\_\{j\}top\(U\_\{j\}\), together withc0​Ic\_\{0\}I, gives normalizationα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and anα\\alpha\{\}\-normalized block\-encoding ofr​\(M\)=c0​I\+Σ​cjj​Rjr\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}up to unnormalized implementation error at mostΣ\|jcj\|αηj\+jδLCU\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. If∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}, the triangle inequality gives unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}forg​\(M\)g\(M\)\. If T is obtained fromg​\(M\)g\(M\)by left and right selection isometries or contractions, the same bound applies to the selected target block\. The query complexity of one use is that of one coherent PREPARE/SELECT LCU call; under efficient coefficient preparation and multiplexed access to theUjU\_\{j\}, this is𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)oracle queries plus polylogarithmic/prescribed multiplexing overhead, or the corresponding variable\-time bound if a variable\-time implementation is substituted\. No normalization reduction beyond the LCU normalizationα\\alpha\{\}is claimed\. ### Theorem Graph Entry 3 •Type:theorem•Reviews:3•Dependencies:0##### Statement Square\-root sign identity: If A has no eigenvalues on the closed negative real axis, then forM=\[\[0,A\],\[I,0\]\],s​i​g​n​\(M\)=\[\[0,A1/2\],\[A−1/2,0\]\]M=\[\[0,A\],\[I,0\]\],sign\(M\)=\[\[0,A^\{1/2\}\],\[A^\{\-1/2\},0\]\], whereA1/2A^\{1/2\}is the principal square root\. ##### Proof Let A have no eigenvalues on the closed negative real axis so that its principal square root is defined and has spectrum in the open right half\-plane\. ForM=\[\[0,A\],\[I,0\]\],M2=d​i​a​g​\(A,A\)M=\[\[0,A\],\[I,0\]\],M^\{2\}=diag\(A,A\)\. The primary square root ofM2M^\{2\}isd​i​a​g​\(A1/2,A1/2\)diag\(A^\{1/2\},A^\{1/2\}\), with inversed​i​a​g​\(A−1/2,A−1/2\)diag\(A^\{\-1/2\},A^\{\-1/2\}\)\. The matrix sign iss​i​g​n​\(M\)=M​\(M2\)−1/2sign\(M\)=M\(M^\{2\}\)^\{\-1/2\}, since M has no imaginary\-axis eigenvalues\. Multiplying gives \[\[0,A1/2\],\[A−1/2,0\]\]A^\{1/2\}\],\[A^\{\-1/2\},0\]\]\. ### Theorem Graph Entry 4 •Type:theorem•Reviews:0•Dependencies:0##### Statement Off\-diagonal sign identity for product square roots: ForM=\[\[0,A\],\[B,0\]\]M=\[\[0,A\],\[B,0\]\]with AB and BA avoiding the closed negative real axis,s​i​g​n​\(M\)=\[\[0,A​\(B​A\)−1/2\],\[B​\(A​B\)−1/2,0\]\]sign\(M\)=\[\[0,A\(BA\)^\{\-1/2\}\],\[B\(AB\)^\{\-1/2\},0\]\]\. For positive definiteA,BA,Bthis block encodes standard geometric\-mean factors, e\.g\.A​\(B​A\)−1/2​B=AA\(BA\)^\{\-1/2\}B=A\#B\. ##### Proof ForM=\[\[0,A\],\[B,0\]\],M2=d​i​a​g​\(A​B,B​A\)M=\[\[0,A\],\[B,0\]\],M^\{2\}=diag\(AB,BA\)\. If AB and BA have no eigenvalues on the closed negative real axis and A is invertible \(or under the usual assumptions ensuring the principal roots and equivalence of spectra\),s​i​g​n​\(M\)=M​\(M2\)−1/2sign\(M\)=M\(M^\{2\}\)^\{\-1/2\}\. Hences​i​g​n​\(M\)sign\(M\)has upper\-right blockA​\(B​A\)−1/2A\(BA\)^\{\-1/2\}and lower\-left blockB​\(A​B\)−1/2B\(AB\)^\{\-1/2\}\. When A and B are positive definite, the upper\-right block equals the matrix geometric mean A\#B−1B^\{\-1\}? More precisely, for positive definiteA,B,A​\(B​A\)−1/2=A1/2​\(A1/2​B​A1/2\)−1/2​A1/2=AA,B,A\(BA\)^\{\-1/2\}=A^\{1/2\}\(A^\{1/2\}BA^\{1/2\}\)^\{\-1/2\}A^\{1/2\}=A\#B−1B^\{\-1\}, whileA​\(B​A\)−1/2​BA\(BA\)^\{\-1/2\}Bgives A\#B\. Thus the sign block gives inverse\-geometric\-mean\-like factors from which A\#B can be obtained by multiplication with B or A depending on convention\. ##### Comments The geometric\-mean equalityA​\(B​A\)−1/2​B=AA\(BA\)^\{\-1/2\}B=A\#B is not generally correct for noncommuting positive definiteA,BA,B; it agrees in the scalar/commuting case but the block is generally a related Riccati/polar factor rather than the symmetric Pusz\-Woronowicz geometric mean\. ### Theorem Graph Entry 5 •Type:theorem•Reviews:1•Dependencies:0##### Statement Corrected geometric\-mean sign identity: For positive definiteA,BA,BandM=\[\[0,A\],\[B,0\]\],sign\(M\)=M=\[\[0,A\],\[B,0\]\],sign\(M\)= \[\[0,B−1\[\[0,B^\{\-1\}\#A\],\[A−1A\],\[A^\{\-1\}\#B,0\]\]B,0\]\], where \# denotes the Pusz\-Woronowicz geometric mean\. Equivalently, the upper\-right block is the unique positive definite Z satisfying ZBZ=AA, and the lower\-left block isZ−1Z^\{\-1\}\. ##### Proof For positive definiteA,BA,B, the block matrixM=\[\[0,A\],\[B,0\]\]M=\[\[0,A\],\[B,0\]\]is diagonalizable with no imaginary\-axis eigenvalues because it is similar to the Hermitian matrix \[\[0,A1/2BA1/2\],\[IA^\{1/2\}BA^\{1/2\}\],\[I?\]\]? A cleaner route uses the principal square root formula for the sign of matrices whose square has no negative\-real\-axis spectrum:sign\(M\)=M\(M2\)\(−1/2\)sign\(M\)=M\(M^\{2\}\)^\{\(\}\-1/2\)\. SinceM2=d​i​a​g​\(A​B,B​A\)M^\{2\}=diag\(AB,BA\)and AB,BA have positive real spectrum and principal square roots,sign\(M\)=\[\[0,A\(BA\)\(−1/2\)\],\[B\(AB\)\(−1/2\),0\]\]sign\(M\)=\[\[0,A\(BA\)^\{\(\}\-1/2\)\],\[B\(AB\)^\{\(\}\-1/2\),0\]\]\. It remains to identifyZ:=A\(BA\)\(−1/2\)Z:=A\(BA\)^\{\(\}\-1/2\)\. This Z is positive definite in the operator\-geometric\-mean sense: by standard geometric\-mean identity, the unique positive definite solution of Z BZ=AZ=AisZ=B−1Z=B^\{\-1\}\#A\. Verify ZBZ=A via the known formulaB−1B^\{\-1\}\#A=B−1/2​\(B1/2​A​B1/2\)1/2​B−1/2A=B^\{\-1/2\}\(B^\{1/2\}AB^\{1/2\}\)^\{1/2\}B^\{\-1/2\}, which is the unique positive definite solution of XBX=A\. The equalityA\(BA\)\(−1/2\)=B−1A\(BA\)^\{\(\}\-1/2\)=B^\{\-1\}\#A is a standard identity following from uniqueness of the principal square root/Riccati solution; indeedA\(BA\)\(−1/2\)A\(BA\)^\{\(\}\-1/2\)satisfies XBX=A and has positive spectrum/similar to a positive definite matrix\. SimilarlyB\(AB\)\(−1/2\)=A−1B\(AB\)^\{\(\}\-1/2\)=A^\{\-1\}\#B and the two blocks are inverses becauses​i​g​n​\(M\)2=Isign\(M\)^\{2\}=I\. This supplies the missing justification of off\-diagonal form and positivity using the explicit sign formula and standard uniqueness characterization of the geometric mean\. ##### Comments The proof contains an invalid/malformed similarity claim: it says M is similar to the Hermitian matrix \[\[0,A1/2BA1/2\],\[IA^\{1/2\}BA^\{1/2\}\],\[I?\]\], which is not a well\-defined matrix and is not justified\. Although the proof later attempts a cleaner route, this line is an erroneous formula deduction in the proof as written\. ### Theorem Graph Entry 6 •Type:theorem•Reviews:3•Dependencies:0##### Statement Resolvent factorizations for common sign embeddings: \(i\) ForM=\[\[A,C\],\[0,B\]\]M=\[\[A,C\],\[0,B\]\], \(zI\-M\)\(−1\)M\)^\{\(\}\-1\)has off\-diagonal block \(zI\-A\)\(−1\)C\(zI−B\)\(−1\)A\)^\{\(\}\-1\)C\(zI\-B\)^\{\(\}\-1\)\. \(ii\) ForM=\[\[0,A\],\[I,0\]\]M=\[\[0,A\],\[I,0\]\], \(zI\-M\)\(−1\)M\)^\{\(\}\-1\)=\[\[zR,AR\],\[RR,zR\]\] withR=\(z2I−A\)\(−1\)R=\(z^\{2\}I\-A\)^\{\(\}\-1\)\. \(iii\) ForM=\[\[0,A\],\[B,0\]\]M=\[\[0,A\],\[B,0\]\], \(zI\-M\)\(−1\)=\[\[z\(z2I−AB\)\(−1\),A\(z2I−BA\)\(−1\)\],\[B\(z2I−AB\)\(−1\),z\(z2I−BA\)\(−1\)\]\]M\)^\{\(\}\-1\)=\[\[z\(z^\{2\}I\-AB\)^\{\(\}\-1\),A\(z^\{2\}I\-BA\)^\{\(\}\-1\)\],\[B\(z^\{2\}I\-AB\)^\{\(\}\-1\),z\(z^\{2\}I\-BA\)^\{\(\}\-1\)\]\]\. ##### Proof ForM=\[\[A,C\],\[0,B\]\]M=\[\[A,C\],\[0,B\]\], compute zI\-MM=\[\[zI\-A,−C\],\[0A,\-C\],\[0,zI\-B\]\]B\]\]\. If z is outsides​p​e​c​\(A\)∪s​p​e​c​\(B\)spec\(A\)\\cup spec\(B\), the inverse of this upper triangular block matrix is \[\[\(zI\-A\)\(−1\)A\)^\{\(\}\-1\),\(zI\-A\)\(−1\)C\(zI−B\)\(−1\)\],\[0A\)^\{\(\}\-1\)C\(zI\-B\)^\{\(\}\-1\)\],\[0,\(zI\-B\)\(−1\)\]\]B\)^\{\(\}\-1\)\]\], as direct multiplication verifies\. ForMs=\[\[0,A\],\[I,0\]\]M\_\{s\}=\[\[0,A\],\[I,0\]\], solving or applying the block inverse formula gives \(zI\-Ms\)\(−1\)M\_\{s\}\)^\{\(\}\-1\)=\[\[zR,AR\],\[RR,zR\]\] withR=\(z2I−A\)\(−1\)R=\(z^\{2\}I\-A\)^\{\(\}\-1\), wheneverz2∉s​p​e​c​\(A\)z^\{2\}\\notin spec\(A\)\. ForMp=\[\[0,A\],\[B,0\]\]M\_\{p\}=\[\[0,A\],\[B,0\]\], the same computation gives top\-leftz\(z2I−AB\)\(−1\)z\(z^\{2\}I\-AB\)^\{\(\}\-1\), top\-rightA\(z2I−BA\)\(−1\)A\(z^\{2\}I\-BA\)^\{\(\}\-1\), bottom\-leftB\(z2I−AB\)\(−1\)B\(z^\{2\}I\-AB\)^\{\(\}\-1\), bottom\-rightz\(z2I−BA\)\(−1\)z\(z^\{2\}I\-BA\)^\{\(\}\-1\), whenever the displayed inverses exist\. ### Theorem Graph Entry 7 •Type:theorem•Reviews:4•Dependencies:0##### Statement Corrected rational\-resolvent block\-encoding compiler: If T is a contraction\-selected block ofg​\(M\),r​\(M\)=c0​I\+Σ​cjj=1m​\(zj​I−M\)−1g\(M\),r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}\(z\_\{j\}I\-M\)^\{\-1\}approximatesg​\(M\)g\(M\)withinδdet\\delta\{\}\_\{\\mathrm\{det\}\}, and each shifted resolventRj=\(zj​I−M\)−1R\_\{j\}=\(z\_\{j\}I\-M\)^\{\-1\}has anαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encoding usingQjQ\_\{j\}queries, then T has anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. One use costs one coherent LCU PREPARE/SELECT call, typically𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)oracle queries plus coefficient\-preparation and multiplexing overhead, or the corresponding variable\-time cost if such a implementation is used\. ##### Proof AssumeUjU\_\{j\}is anαj\\alpha\{\}\_\{j\}\-normalized block\-encoding ofRjR\_\{j\}with scaled error∥top\(Uj\)−Rj/α∥j≤ηj\\lVert top\(U\_\{j\}\)\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}\. Thenα​tj​o​p​\(Uj\)\\alpha\{\}\_\{j\}top\(U\_\{j\}\)approximatesRjR\_\{j\}with unnormalized error at mostαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. Standard LCU applied to the termscj​α​tj​o​p​\(Uj\)c\_\{j\}\\alpha\{\}\_\{j\}top\(U\_\{j\}\), and toc0​Ic\_\{0\}Iwith normalization \|c0c\_\{0\}\|, produces anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized implementation error at mostΣ\|jcj\|αηj\+jδLCU\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Adding deterministic error∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}by the triangle inequality gives the claimed bound\. Contractive block selection cannot increase operator\-norm error\. The query statement is the usual coherent PREPARE/SELECT LCU cost bound under efficient coefficient state preparation and multiplexed access to the shifted\-resolvent block\-encodings\. ##### Comments Potential flaw: the query\-complexity claim does not follow from merely having separateQjQ\_\{j\}\-query block\-encodings of each shifted resolvent\. The proof implicitly assumes efficient coherent PREPARE of coefficients and a multiplexed SELECT implementing controlledUjU\_\{j\}at cost𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\); without this additional uniform/coherent access model, SELECT may cost more \(e\.g\.sumjQj\)sum\_\{j\}Q\_\{j\}\)or may not be available\. The query\-complexity step implicitly assumes efficient coherent coefficient PREPARE and multiplexed controlled access to all shifted\-resolvent block\-encodings at cost𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)\. Separate existence ofQjQ\_\{j\}\-query block\-encodings does not by itself imply such a SELECT oracle; cost could be larger or incoherent access unavailable\. The proof’s query\-complexity conclusion implicitly assumes efficient coherent coefficient PREPARE and a multiplexed controlled SELECT implementing allUjU\_\{j\}at cost𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\); separate existence ofQjQ\_\{j\}\-query block\-encodings of each resolvent does not by itself guarantee such coherent access, and the cost may be larger or unavailable\. ### Theorem Graph Entry 8 •Type:theorem•Reviews:4•Dependencies:0##### Statement Rational\-resolvent compiler with explicit coherent access model: Supposer\(M\)=c0I\+Σcjj=1mRj,Rj=\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}R\_\{j\},R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), approximatesg​\(M\)g\(M\)withinδdet\\delta\{\}\_\{\\mathrm\{det\}\}; T is obtained fromg​\(M\)g\(M\)by contractive block selection; eachRjR\_\{j\}has anαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encodingUjU\_\{j\}; and there are coherent PREPARE/SELECT oracles implementing the LCU coefficients and controlledUjU\_\{j\}with costsQprepQ\_\{\\mathrm\{prep\}\}andQselQ\_\{\\mathrm\{sel\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding,α=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}, with unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, using𝒪​\(Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)queries/gates per block\-encoding use\. If a multiplexed SELECT has cost𝒪​\(maxj⁡Qj\)\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\), this gives that special\-case query bound; otherwise no such bound is implied\. ##### Proof Under the stated oracle model, the LCU construction has an explicit PREPARE unitary mapping \|0\> to the normalized coefficient\-amplitude state and a SELECT unitary applyingUjU\_\{j\}controlled on j\. Standard block\-encoding LCU then yields normalizationα=\|c0\|\+Σ\|cj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\. The error bound is identical to the corrected compiler proof: the scaled errorηj\\eta\{\}\_\{j\}inUjU\_\{j\}contributes unnormalized \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}, and deterministic approximation and LCU synthesis errors add by the triangle inequality\. Contractive block selection preserves the bound\. Since SELECT cost is assumed to beQselQ\_\{\\mathrm\{sel\}\}, one use costs𝒪​\(Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)plus elementary reflection/uncompute overhead; if the model additionally supplies a multiplexed construction withQsel=𝒪​\(maxj⁡Qj\)Q\_\{\\mathrm\{sel\}\}=\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\), this specializes to the familiar maximum\-branch bound, but that is not asserted without the multiplexing assumption\. ##### Comments The proof turns a mathematical contractive block selectionT=L​g​\(M\)​RT=Lg\(M\)Rinto a block\-encoding without assuming or accounting for coherent implementability of the selection isometries/contractionsL,RL,R\. Contractivity only preserves the norm error; it does not by itself provide the circuits or cost needed to select the desired block\. The proof treats contractive block selectionT=L​g​\(M\)​RT=Lg\(M\)Ras freely producing a block\-encoding, but the theorem does not assume coherent implementability/cost of the selection isometries or contractionsL,RL,R; contractivity only preserves norm error, not circuit access to the selected block\. The proof assumes that the contractive block\-selection maps extracting T fromg​\(M\)g\(M\)are coherently implementable at no cost; contractivity preserves the error norm but does not by itself yield a block\-encoding circuit or account for the selection isometries/contractions\. ### Theorem Graph Entry 9 •Type:theorem•Reviews:1•Dependencies:0##### Statement Rational\-resolvent compiler with implementable selection: Letg​\(M\)g\(M\)be a matrix function,T=L​g​\(M\)​RT=Lg\(M\)RwhereL,RL,Rare explicitly implementable isometries or contractions with costsQL,QRQ\_\{L\},Q\_\{R\}, andr\(M\)=c0I\+Σcjj=1mRj,Rj=\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}R\_\{j\},R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), satisfy∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. Suppose eachRjR\_\{j\}has anαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encodingUjU\_\{j\}, and coherent PREPARE/SELECT oracles implement the LCU over\{I,Uj\}\\\{I,U\_\{j\}\\\}with costsQprep,QselQ\_\{\\mathrm\{prep\}\},Q\_\{\\mathrm\{sel\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, using𝒪​\(QL\+QR\+Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{L\}\+Q\_\{R\}\+Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)cost per use\. A boundQsel=𝒪​\(maxj⁡Qj\)Q\_\{\\mathrm\{sel\}\}=\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)holds only under an additional efficient multiplexed\-SELECT construction\. ##### Proof The LCU part follows from the standard PREPARE/SELECT block\-encoding construction: with PREPARE amplitudes proportional to the absolute coefficients \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}and phases storingcj/\|cjc\_\{j\}/\|c\_\{j\}\|, the selected block isr​\(M\)/αr\(M\)/\\alpha\{\}up to LCU synthesis error\. The scaled block\-encoding errorηj\\eta\{\}\_\{j\}contributes unnormalized \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}, so summing givesΣ\|cj\|αηjj\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. Add deterministic rational approximation errorδdet\\delta\{\}\_\{\\mathrm\{det\}\}by the triangle inequality\. If the desired T is extracted by explicit implementable isometries L andRR, compose the block\-encoding ofg​\(M\)g\(M\)with these isometries; the selected block isL​g​\(M\)​RLg\(M\)Rand the error is at most∥L∥​∥E∥​∥R∥≤∥E∥\\lVert L\\rVert\\lVert E\\rVert\\lVert R\\rVert\\leq\\lVert E\\rVertbecauseL,RL,Rare isometries/contractions\. The circuit cost includesQLQ\_\{L\}andQRQ\_\{R\}, plusQprepQ\_\{\\mathrm\{prep\}\}andQselQ\_\{\\mathrm\{sel\}\}\. The max\-branch query bound requires a separate multiplexed SELECT assumption; otherwise the theorem states only the cost of the supplied SELECT oracle\. ##### Comments The proof treats general contractionsL,RL,Ras if they can simply be composed with the block\-encoding ofg​\(M\)g\(M\)\. This is valid for explicitly implemented isometries/unitaries, but for contractions one needs specified exact/approximate block\-encodings or unitary dilations ofL,RL,R, with their normalizations and errors accounted for; the theorem only says "explicitly implementable contractions with costs," which is not a sufficient or precise hypothesis for the claimed block\-encoding and error bound\. ### Theorem Graph Entry 10 •Type:theorem•Reviews:2•Dependencies:0##### Statement Rational\-resolvent compiler for selected blocks: LetT=L​g​\(M\)​RT=Lg\(M\)R, where L and R are exactly implementable selection isometries with costsQL,QRQ\_\{L\},Q\_\{R\}\. Supposer\(M\)=c0I\+Σcjj=1m\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}\(z\_\{j\}I\-M\)^\{\(\}\-1\)satisfies∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. Suppose eachRj=\(zjI−M\)\(−1\)R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\)has anαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encodingUjU\_\{j\}and coherent PREPARE/SELECT oracles implement the LCU over\{I,Uj\}\\\{I,U\_\{j\}\\\}with costsQprep,QselQ\_\{\\mathrm\{prep\}\},Q\_\{\\mathrm\{sel\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding,α=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}, with unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}and cost𝒪​\(QL\+QR\+Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{L\}\+Q\_\{R\}\+Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)per use\. The boundQsel=𝒪​\(maxj⁡Qj\)Q\_\{\\mathrm\{sel\}\}=\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)requires an additional efficient multiplexed\-SELECT assumption\. ##### Proof Apply standard LCU with PREPARE amplitudes proportional to \|c0c\_\{0\}\| and \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}and SELECT applying either identity orUjU\_\{j\}with the coefficient phase\. This gives anα\\alpha\{\}\-normalized block\-encoding ofr​\(M\)r\(M\)with unnormalized implementation error bounded byΣ\|cj\|αηj\+jδLCU\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Since∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}, the block\-encoding approximatesg​\(M\)g\(M\)with unnormalized error bounded byδ\+detΣ\|cj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. If L and R are selection isometries implemented exactly as unitaries between the relevant registers, composing them before/after the block\-encoding produces anα\\alpha\{\}\-normalized block\-encoding ofL​g​\(M\)​RLg\(M\)R\. Isometries have norm one, so the same unnormalized error bound applies\. Costs add\. More general contractions require separate block\-encodings and would multiply normalizations and add their errors, so they are deliberately excluded from the statement\. ##### Comments The selection step is not precise enough: to extract a block one generally needs an implementable coisometry/isometry pair with the correct orientations \(e\.g\. L maps the augmented space to the target output while R maps the target input into the augmented space\), or explicit unitary/block\-encoding dilations\. The statement merely says "selection isometries" and the proof treats composition with possibly non\-square maps as automatically yielding a standard block\-encoding ofL​g​\(M\)​RLg\(M\)R, which hides dimension/orientation and implementability assumptions not stated\. The selection\-composition step is underspecified: extractingT=L​g​\(M\)​RT=Lg\(M\)Rrequires compatible orientations and implementable unitary/isometric dilations \(e\.g\. L as a coisometry from augmented output and R as an isometry into augmented input\)\. The statement only says "selection isometries," so the proof hides dimension/orientation and block\-encoding implementation assumptions needed for the claimed block\-encoding\. ### Theorem Graph Entry 11 •Type:theorem•Reviews:4•Dependencies:0##### Statement Rational\-resolvent compiler for oriented block extraction: Letg​\(M\)g\(M\)act on an augmented Hilbert spaceHaugH\_\{\\mathrm\{aug\}\}, and let the desired target beT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}for exactly implementable isometriesEin:Hin→HaugE\_\{\\mathrm\{in\}\}:H\_\{\\mathrm\{in\}\}\\to H\_\{\\mathrm\{aug\}\}andEout:Hout→HaugE\_\{\\mathrm\{out\}\}:H\_\{\\mathrm\{out\}\}\\to H\_\{\\mathrm\{aug\}\}with implementation costsQin,QoutQ\_\{\\mathrm\{in\}\},Q\_\{\\mathrm\{out\}\}\. Supposer\(M\)=c0I\+Σcjj=1mRj,Rj=\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}R\_\{j\},R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), satisfies∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. SupposeUjU\_\{j\}areαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encodings ofRjR\_\{j\}, and coherent PREPARE/SELECT oracles for the LCU over\{I,Uj\}\\\{I,U\_\{j\}\\\}have costsQprep,QselQ\_\{\\mathrm\{prep\}\},Q\_\{\\mathrm\{sel\}\}and LCU synthesis errorδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, using𝒪​\(Qin\+Qout\+Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{\\mathrm\{in\}\}\+Q\_\{\\mathrm\{out\}\}\+Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)cost per use\. A specializationQsel=𝒪​\(maxj⁡Qj\)Q\_\{\\mathrm\{sel\}\}=\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)is valid only if an efficient multiplexed SELECT for theUjU\_\{j\}is part of the access model\. ##### Proof Use standard LCU to build a block\-encoding ofr​\(M\)r\(M\)\. Namely PREPARE prepares a coefficient state whose probabilities are proportional to the positive weights \|c0c\_\{0\}\| and \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}, equivalently amplitudes proportional to their square roots, while SELECT applies identity orUjU\_\{j\}with the coefficient phase\. This yields anα\\alpha\{\}\-normalized block\-encoding ofr\(M\),α=\|c0\|\+Σ\|cj\|αjr\(M\),\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}, with unnormalized error bounded byΣ\|cj\|αηj\+jδLCU\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, whereδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}is by definition the unnormalized error caused by imperfect coefficient preparation, phases, and SELECT synthesis\. The termΣ\|cj\|αηjj\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}appears because anαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encoding contributes unnormalized errorαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. Add the deterministic approximation errorδdet\\delta\{\}\_\{\\mathrm\{det\}\}by the triangle inequality\. Now suppose the selected block has the formT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}with isometriesEin:Hin→HaugE\_\{\\mathrm\{in\}\}:H\_\{\\mathrm\{in\}\}\\to H\_\{\\mathrm\{aug\}\}andEout:Hout→HaugE\_\{\\mathrm\{out\}\}:H\_\{\\mathrm\{out\}\}\\to H\_\{\\mathrm\{aug\}\}\. Exact circuitsVin,VoutV\_\{\\mathrm\{in\}\},V\_\{\\mathrm\{out\}\}implementing these embeddings allow one to composeVinV\_\{\\mathrm\{in\}\}before andVout∗V\_\{\\mathrm\{out\}\}^\{\\ast\}after the block\-encoding ofg​\(M\)g\(M\); the resulting top block isEout∗​g​\(M\)​EinE\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}up to the same unnormalized error because multiplication by isometries has norm one\. Costs add\. The statement deliberately gives cost in terms of the supplied coherent PREPARE/SELECT oracle; a max\-branch bound is only a corollary under a separate multiplexed SELECT implementation\. ##### Comments The LCU step implicitly requires allUjU\_\{j\}\(and the identity term\) to be compatible block\-encodings with a common system space and common/alignable ancilla projector \(or explicit padding/dilations\)\. The statement only says eachUjU\_\{j\}is a block\-encoding and that PREPARE/SELECT exists, but the proof applies standard block\-encoding LCU without stating or accounting for this compatibility assumption\. The LCU proof omits a necessary compatibility assumption: theUjU\_\{j\}must be block\-encodings on a common/alignable system and ancilla subspace \(with padding/dilations accounted for\) for PREPARE/SELECT LCU to block\-encode the stated linear combination; separate block\-encodings plus PREPARE/SELECT costs do not by themselves ensure this\. The LCU step omits a necessary compatibility assumption: theUjU\_\{j\}must be block\-encodings on a common/alignable system and ancilla subspace \(or include explicit padding/dilations and their costs/errors\); separate block\-encodings plus PREPARE/SELECT access do not by themselves justify standard LCU of the stated resolvents\. The LCU step omits a necessary compatibility assumption: the shifted\-resolvent block\-encodingsUjU\_\{j\}must share a common/alignable system space and ancilla projector \(or include explicit padding/dilations with costs/errors\) for standard PREPARE/SELECT LCU to block\-encode the stated linear combination; separate block\-encodings plus SELECT access do not by themselves justify the proof\. ### Theorem Graph Entry 12 •Type:theorem•Reviews:4•Dependencies:0##### Statement Fully specified rational\-resolvent block\-extraction compiler: Letg​\(M\)g\(M\)act onHaugH\_\{\\mathrm\{aug\}\}andT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}for exactly implementable isometriesEin:Hin→HaugE\_\{\\mathrm\{in\}\}:H\_\{\\mathrm\{in\}\}\\to H\_\{\\mathrm\{aug\}\}andEout:Hout→HaugE\_\{\\mathrm\{out\}\}:H\_\{\\mathrm\{out\}\}\\to H\_\{\\mathrm\{aug\}\}, with costsQin,QoutQ\_\{\\mathrm\{in\}\},Q\_\{\\mathrm\{out\}\}\. Letr\(M\)=c0I\+Σcjj=1mRj,Rj=\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j=1\}^\{m\}c\_\{j\}R\_\{j\},R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), satisfy∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. Suppose allUjU\_\{j\}are compatible, common\-registerαj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encodings ofRjR\_\{j\}, with any padding/dilation already included, and suppose coherent PREPARE/SELECT oracles for the LCU over\{I,Uj\}\\\{I,U\_\{j\}\\\}have costsQprep,QselQ\_\{\\mathrm\{prep\}\},Q\_\{\\mathrm\{sel\}\}and unnormalized synthesis errorδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, using𝒪​\(Qin\+Qout\+Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{\\mathrm\{in\}\}\+Q\_\{\\mathrm\{out\}\}\+Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)cost per use\. The simplificationQsel=𝒪​\(maxj⁡Qj\)Q\_\{\\mathrm\{sel\}\}=\\mathcal\{O\}\(\\max\_\{j\}Q\_\{j\}\)is valid only under an additional efficient multiplexed\-SELECT assumption\. ##### Proof Use standard block\-encoding LCU in its compatible\-oracle form\. PREPARE prepares a coefficient state whose probabilities are proportional to \|c0c\_\{0\}\| and \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}, while SELECT applies the corresponding common\-register block\-encodingUjU\_\{j\}with the coefficient phase\. Compatibility guarantees that the same ancilla projection selects the encoded matrices, so the top block of thePREPARE†​SELECT​PREPARE\\mathrm\{PREPARE\}^\{\\dagger\}\\,\\mathrm\{SELECT\}\\,\\mathrm\{PREPARE\}construction is the weighted sum divided byα\\alpha\{\}\. The unnormalized error from each shifted\-resolvent block\-encoding is \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}; imperfect LCU synthesis contributesδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}by definition as an unnormalized error\. The deterministic approximation errorδdet\\delta\{\}\_\{\\mathrm\{det\}\}is added by triangle inequality\. Exact embedding isometriesEin,EoutE\_\{\\mathrm\{in\}\},E\_\{\\mathrm\{out\}\}are implemented by circuits before and after the block\-encoding; because they are isometries, they do not enlarge the operator\-norm error\. Costs add as stated\. The theorem intentionally phrasesQselQ\_\{\\mathrm\{sel\}\}as part of the coherent access model; max\-branch costs require a further multiplexing construction\. ##### Comments The proof’s error bound implicitly assumes that "αj\\alpha\{\}\_\{j\}\-normalizedηj\\eta\{\}\_\{j\}\-accurate block\-encoding" means scaled top\-block error∥top\(Uj\)−Rj/α∥j≤ηj\\lVert top\(U\_\{j\}\)\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}, so the unnormalized contribution is \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. The theorem statement does not define this convention; under the common convention∥Rj−αtjop\(Uj\)∥≤ηj\\lVert R\_\{j\}\-\\alpha\{\}\_\{j\}top\(U\_\{j\}\)\\rVert\\leq\\eta\{\}\_\{j\}, the contribution would be \|cj\|ηjc\_\{j\}\|\\eta\{\}\_\{j\}instead\. Thus the proof relies on an unstated accuracy convention and the stated bound is ambiguous/possibly wrong\. The proof relies on an unstated convention for block\-encoding accuracy: it treatsηj\\eta\{\}\_\{j\}as scaled top\-block error, giving unnormalized contribution \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}; under the common unnormalized\-error convention the term would be \|cj\|ηjc\_\{j\}\|\\eta\{\}\_\{j\}, so the stated bound is ambiguous without definingηj\\eta\{\}\_\{j\}\. ### Theorem Graph Entry 13 •Type:theorem•Reviews:6•Dependencies:0##### Statement Rational\-resolvent block\-extraction compiler with scaled\-error convention: Letg​\(M\)g\(M\)act onHaugH\_\{\\mathrm\{aug\}\}andT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}for exactly implementable isometriesEin:Hin→HaugE\_\{\\mathrm\{in\}\}:H\_\{\\mathrm\{in\}\}\\to H\_\{\\mathrm\{aug\}\}andEout:Hout→HaugE\_\{\\mathrm\{out\}\}:H\_\{\\mathrm\{out\}\}\\to H\_\{\\mathrm\{aug\}\}, with costsQin,QoutQ\_\{\\mathrm\{in\}\},Q\_\{\\mathrm\{out\}\}\. Letr\(M\)=c0I\+ΣcjjRj,Rj=\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\},R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), satisfy∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. Suppose allUjU\_\{j\}are compatible common\-register block\-encodings satisfying∥ΠUjΠ−∗Rj/α∥j≤ηj\\lVert\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}, with padding/dilation included, and suppose coherent PREPARE/SELECT oracles for the LCU over\{I,Uj\}\\\{I,U\_\{j\}\\\}have costsQprep,QselQ\_\{\\mathrm\{prep\}\},Q\_\{\\mathrm\{sel\}\}and unnormalized synthesis errorδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, using𝒪​\(Qin\+Qout\+Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{\\mathrm\{in\}\}\+Q\_\{\\mathrm\{out\}\}\+Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)cost per use\. Ifηj\\eta\{\}\_\{j\}is instead defined as unnormalized block\-encoding error, replaceαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}byηj\\eta\{\}\_\{j\}\. ##### Proof The proof is the standard compatible block\-encoding LCU argument\. PREPARE prepares coefficient probabilities proportional to \|c0c\_\{0\}\| and \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}, SELECT applies the corresponding common\-registerUjU\_\{j\}with phases\. Since the top block ofUjU\_\{j\}differs fromRj/αjR\_\{j\}/\\alpha\{\}\_\{j\}by at mostηj\\eta\{\}\_\{j\}in operator norm, multiplying by the LCU weight \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}gives unnormalized contribution \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. The identity term is exact unless included inδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}\. The LCU synthesis imperfections contributeδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}by definition as unnormalized error\. Thus the constructed block\-encoding approximatesr​\(M\)r\(M\)with unnormalized errorΣ\|cj\|αηj\+jδLCU\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}and normalizationα=\|c0\|\+Σ\|cj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\. Add∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. Composing with exact embedding isometriesEin,EoutE\_\{\\mathrm\{in\}\},E\_\{\\mathrm\{out\}\}gives the selected block and preserves the norm error\. Costs are exactly those of the embeddings and supplied PREPARE/SELECT oracles\. ##### Comments The final sentence is not generally valid as stated: replacingαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}byηj\\eta\{\}\_\{j\}only changes the resolvent\-implementation error convention, but the rest of the theorem/proof still uses the scaled\-error definition in the hypothesis∥ΠUjΠ−∗Rj/α∥j≤ηj\\lVert\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}; an unnormalized\-error convention would require restating that hypothesis as∥Rj−αΠjUjΠ∥∗≤ηj\\lVert R\_\{j\}\-\\alpha\{\}\_\{j\}\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\\rVert\\leq\\eta\{\}\_\{j\}\. As written it mixes two accuracy conventions ambiguously\. The final convention\-switch sentence is ambiguous/incorrect: replacingαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}byηj\\eta\{\}\_\{j\}is valid only if the hypothesis is also restated as an unnormalized\-error bound∥Rj−αΠjUjΠ∥∗≤ηj\\lVert R\_\{j\}\-\\alpha\{\}\_\{j\}\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\\rVert\\leq\\eta\{\}\_\{j\}; as written the theorem keeps the scaled\-error hypothesis and mixes conventions\. The final convention\-switch sentence is ambiguous/incorrect: replacingαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}byηj\\eta\{\}\_\{j\}is valid only if the block\-encoding hypothesis is also restated as an unnormalized\-error bound∥Rj−αΠjUjΠ∥∗≤ηj\\lVert R\_\{j\}\-\\alpha\{\}\_\{j\}\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\\rVert\\leq\\eta\{\}\_\{j\}; as written the theorem keeps the scaled\-error hypothesis and mixes accuracy conventions\. The final convention\-switch sentence is ambiguous/incorrect: replacingαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}byηj\\eta\{\}\_\{j\}is valid only if the hypothesis is also restated as an unnormalized\-error bound∥Rj−αΠjUjΠ∥∗≤ηj\\lVert R\_\{j\}\-\\alpha\{\}\_\{j\}\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\\rVert\\leq\\eta\{\}\_\{j\}; as written the theorem keeps the scaled\-error hypothesis and mixes accuracy conventions\. The final convention\-switch sentence is ambiguous/incorrect: replacingαηjj\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}byηj\\eta\{\}\_\{j\}is valid only if the block\-encoding hypothesis is also restated as∥Rj−αΠjUjΠ∥∗≤ηj\\lVert R\_\{j\}\-\\alpha\{\}\_\{j\}\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\\rVert\\leq\\eta\{\}\_\{j\}; as written the theorem keeps the scaled\-error hypothesis and mixes conventions\. ### Theorem Graph Entry 14 •Type:theorem•Reviews:15•Dependencies:0##### Statement Scaled\-error rational\-resolvent block\-extraction compiler: Letg​\(M\)g\(M\)act onHaugH\_\{\\mathrm\{aug\}\}andT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}for exactly implementable isometriesEin:Hin→HaugE\_\{\\mathrm\{in\}\}:H\_\{\\mathrm\{in\}\}\\to H\_\{\\mathrm\{aug\}\}andEout:Hout→HaugE\_\{\\mathrm\{out\}\}:H\_\{\\mathrm\{out\}\}\\to H\_\{\\mathrm\{aug\}\}, with costsQin,QoutQ\_\{\\mathrm\{in\}\},Q\_\{\\mathrm\{out\}\}\. Letr\(M\)=c0I\+ΣcjjRj,Rj=\(zjI−M\)\(−1\)r\(M\)=c\_\{0\}I\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\},R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), satisfy∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}\. Suppose allUjU\_\{j\}are compatible common\-register block\-encodings satisfying the scaled\-error bound∥ΠUjΠ−∗Rj/α∥j≤ηj\\lVert\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}, with padding/dilation included, and suppose coherent PREPARE/SELECT oracles for the LCU over\{I,Uj\}\\\{I,U\_\{j\}\\\}have costsQprep,QselQ\_\{\\mathrm\{prep\}\},Q\_\{\\mathrm\{sel\}\}and unnormalized synthesis errorδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Then T has anα\\alpha\{\}\-normalized block\-encoding withα=\|c0\|\+Σ\|jcj\|αj\\alpha\{\}=\|c\_\{0\}\|\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}and unnormalized error at mostδ\+detΣ\|jcj\|αηj\+jδLCU\\delta\{\}\_\{\\mathrm\{det\}\}\+\\Sigma\{\}\_\{j\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}, using𝒪​\(Qin\+Qout\+Qprep\+Qsel\)\\mathcal\{O\}\(Q\_\{\\mathrm\{in\}\}\+Q\_\{\\mathrm\{out\}\}\+Q\_\{\\mathrm\{prep\}\}\+Q\_\{\\mathrm\{sel\}\}\)cost per use\. ##### Proof This is the same standard LCU proof, but with only one accuracy convention\. PREPARE prepares probabilities proportional to the LCU weights \|c0c\_\{0\}\| and \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}, SELECT applies the common\-registerUjU\_\{j\}with coefficient phases\. Compatibility of the block\-encodings ensures the top block is the corresponding weighted sum\. Since∥ΠUjΠ−∗Rj/α∥j≤ηj\\lVert\\Pi\{\}U\_\{j\}\\Pi\{\}^\{\\ast\}\-R\_\{j\}/\\alpha\{\}\_\{j\}\\rVert\\leq\\eta\{\}\_\{j\}, the unnormalized contribution of the jth error is \|cj\|αηjjc\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\. The LCU synthesis errorδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}is stipulated to be unnormalized\. Therefore the block\-encoding approximatesr​\(M\)r\(M\)with normalizationα\\alpha\{\}and unnormalized errorΣ\|cj\|αηj\+jδLCU\\Sigma\{\}\|c\_\{j\}\|\\alpha\{\}\_\{j\}\\eta\{\}\_\{j\}\+\\delta\{\}\_\{\\mathrm\{LCU\}\}\. Add the deterministic rational approximation error by triangle inequality\. Exact embedding isometriesEin,EoutE\_\{\\mathrm\{in\}\},E\_\{\\mathrm\{out\}\}extractT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}and do not increase the operator norm error\. The cost is the sum of embedding and PREPARE/SELECT costs\. ##### Comments Potential flaw: the proof invokes a "standard LCU proof" but does not specify the two PREPARE states/phasing convention needed for complex coefficients\. Preparing one probability distribution proportional to \|cj\|αjc\_\{j\}\|\\alpha\{\}\_\{j\}and putting phases only in SELECT is sufficient only if the SELECT oracle is defined to applyp​h​a​s​e​\(cj\)​Ujphase\(c\_\{j\}\)U\_\{j\}coherently on each branch with a compatible inverse/uncompute; otherwise the top block need not equalΣ​cjj​Rj/α\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}/\\alpha\{\}\. The theorem’s phrase "PREPARE/SELECT oracles … with unnormalized synthesis errorδLCU\\delta\{\}\_\{\\mathrm\{LCU\}\}" may intend this, but the proof leaves the complex\-coefficient LCU implementation under\-specified\. The LCU step is under\-specified for complex coefficients: the proof assumes a PREPARE/SELECT convention in which coefficient phases \(including the c0 branch\) are coherently incorporated so that the top block is exactlyΣ​cjj​Rj/α\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}/\\alpha\{\}, but the theorem only states generic PREPARE/SELECT access and does not spell out the required phasing/two\-state LCU convention; without this, the weighted\-sum conclusion need not follow\. LCU step is under\-specified for complex coefficients: the proof assumes a phasing/two\-PREPARE convention making the top block equalΣ​cjj​Rj/α\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}/\\alpha\{\}, but the theorem only states generic PREPARE/SELECT access; without explicit coherent coefficient phases \(including c0\) the weighted\-sum conclusion need not follow\. LCU step is under\-specified for complex coefficients: the proof assumes a coherent phasing/two\-PREPARE convention, including the c0 branch, so that the LCU top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}\. The theorem only states generic PREPARE/SELECT access, so the weighted\-sum conclusion does not follow without this additional specification\. LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases/two\-PREPARE convention \(including the c0 branch\) so that the top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}, but the theorem only states generic PREPARE/SELECT access; without this extra specification the weighted\-sum conclusion need not follow\. LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases/two\-PREPARE convention, including the c0 branch, so the top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}; the theorem only states generic PREPARE/SELECT access, so the weighted\-sum conclusion need not follow without this extra specification\. LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases/two\-PREPARE convention, including the c0 branch, so the top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}; generic PREPARE/SELECT access as stated does not by itself imply this weighted\-sum conclusion\. LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases/two\-PREPARE convention, including the c0 branch, so that the top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}; generic PREPARE/SELECT access as stated does not by itself imply this weighted\-sum conclusion\. The LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases/two\-PREPARE convention, including the c0 branch, so that the top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}; generic PREPARE/SELECT access as stated does not by itself imply this weighted\-sum conclusion\. The LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases/two\-PREPARE convention, including the c0 branch, so the top block equals \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}; generic PREPARE/SELECT access as stated does not by itself imply this weighted\-sum conclusion\. LCU step is under\-specified for complex coefficients: the proof assumes coherent coefficient phases, including the c0 identity branch, are built into SELECT/PREPARE so that the selected top block is \(c0I\+ΣcjjRj\)/αI\+\\Sigma\{\}\_\{j\}c\_\{j\}R\_\{j\}\)/\\alpha\{\}; generic PREPARE/SELECT access as stated does not by itself guarantee this weighted\-sum identity\. ### Theorem Graph Entry 15 •Type:theorem•Reviews:6•Dependencies:0##### Statement Block extraction from a rational\-resolvent block\-encoding: LetT=Eout∗​g​\(M\)​EinT=E\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}with exactly implementable isometriesEin,EoutE\_\{\\mathrm\{in\}\},E\_\{\\mathrm\{out\}\}\. Ifr​\(M\)r\(M\)is a rational\-resolvent approximation with∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}and W is anα\\alpha\{\}\-normalized block\-encoding ofr​\(M\)r\(M\)with unnormalized errorϵr\\epsilon\{\}\_\{r\}, then composing W withEinE\_\{\\mathrm\{in\}\}andEoutE\_\{\\mathrm\{out\}\}gives anα\\alpha\{\}\-normalized block\-encoding of T with unnormalized error at mostδ\+detϵr\\delta\{\}\_\{\\mathrm\{det\}\}\+\\epsilon\{\}\_\{r\}\. If W was obtained by a valid LCU of compatible shifted\-resolvent block\-encodingsRj=\(zjI−M\)\(−1\)R\_\{j\}=\(z\_\{j\}I\-M\)^\{\(\}\-1\), then one may takeα\\alpha\{\}equal to the LCU weight andϵr\\epsilon\{\}\_\{r\}equal to the unnormalized LCU implementation error, including all shifted\-resolvent and coefficient\-synthesis errors\. ##### Proof By hypothesis, W is already anα\\alpha\{\}\-normalizedϵr\\epsilon\{\}\_\{r\}\-accurate block\-encoding ofr​\(M\)r\(M\), meaning its encoded block differs fromr​\(M\)/αr\(M\)/\\alpha\{\}by at mostϵ/rα\\epsilon\{\}\_\{r\}/\\alpha\{\}, equivalently the unnormalized encoded operator differs fromr​\(M\)r\(M\)by at mostϵr\\epsilon\{\}\_\{r\}\. Since∥g\(M\)−r\(M\)∥≤δdet\\lVert g\(M\)\-r\(M\)\\rVert\\leq\\delta\{\}\_\{\\mathrm\{det\}\}, the same block\-encoding approximatesg​\(M\)g\(M\)with unnormalized error at mostδ\+detϵr\\delta\{\}\_\{\\mathrm\{det\}\}\+\\epsilon\{\}\_\{r\}\. Exact embedding isometriesEinE\_\{\\mathrm\{in\}\}andEoutE\_\{\\mathrm\{out\}\}compose with W to encodeEout∗​g​\(M\)​Ein/αE\_\{\\mathrm\{out\}\}^\{\\ast\}g\(M\)E\_\{\\mathrm\{in\}\}/\\alpha\{\}\. Multiplication by isometries does not increase operator norm, so the error bound is preserved\. Costs add by circuit composition\.

Similar Articles

Characterizing initial human-AI proof formalization workflows

arXiv cs.AI

Researchers from Oxford, Cambridge, MIT, CMU and other institutions conduct a mixed-methods study examining how people integrate AI tools into mathematical proof formalization workflows, finding that participants generally achieve higher formalization accuracy with AI assistance while preferring to maintain high-level human control over the proof discovery process.

AI Co-Mathematician: Accelerating Mathematicians with Agentic AI

Hugging Face Daily Papers

This paper introduces the AI Co-Mathematician, a workbench that uses agentic AI to support mathematicians in open-ended research tasks like ideation and theorem proving. Early tests show the system achieving state-of-the-art results on hard problem-solving benchmarks, including a 48% score on FrontierMath Tier 4.

Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries

arXiv cs.CL

This paper presents EinsteinArena, an agent-native platform enabling decentralized scientific discovery through open interaction among autonomous AI agents. The platform has already produced 12 new state-of-the-art results, including an improved lower bound for the kissing number problem in dimension 11, demonstrating that collective AI-driven research can emerge from agents sharing insights and building on each other's work.

Accelerating discovery with the AI for Math Initiative

Google DeepMind Blog

Google DeepMind and Google launched the AI for Math Initiative, partnering with five prestigious research institutions to use AI tools like Gemini Deep Think and AlphaProof to accelerate mathematical discoveries.

@rohanpaul_ai: Google DeepMind's new paper. Shows that AI can now search formal mathematics proofs, but only inside carefully constrai…

X AI KOLs Following

Google DeepMind's new paper introduces AlphaProof Nexus, an AI system that combines an LLM with the Lean proof checker to search for formal proofs in constrained mathematical domains. The system solves several unsolved problems from the Erdős and OEIS sets, demonstrating a new division of labor where the AI proposes proof candidates and the verifier enforces correctness.