QuantumBFS / QuantumBFS/quantum.harness
[challenge]: Sign-problem free hunter
Nobody has claimed this yet.
- Dominant language
- Python
- Stars
- 66
- Forks
- 93
- PR merge metrics
- No merged PRs in 30d
Description
Released by
Lei Wang, Institute of Physics, Chinese Academy of Sciences
Contact email
wangleiphy@gmail.com
Method
Quantum Monte Carlo
Challenge issue
Background
In May 2015 a numerical observation was posted on MathOverflow (How to prove this determinant is positive?): for real matrices $A_i = \begin{pmatrix} 0 & B_i \ B_i^T & 0 \end{pmatrix}$, the determinant $\det\left(I + e^{A_1} e^{A_2} \cdots e^{A_N}\right)$ appears to be always nonnegative. Within a day Terence Tao commented that each factor, and hence the product, lies in the split orthogonal group $O(n,n)$, the group of real matrices preserving the indefinite metric $\eta = \mathrm{diag}(1_n, -1_n)$. Gergely Harcos (user GH from MO) reduced the question to a block classification of $SO^0(n,n)$ and, with Tao supplying the final step, proved it; Tao then gave a streamlined proof on his blog using the standard branch of the matrix logarithm. The theorem is stronger than the conjecture: $\det(I+T)$ is nonnegative on the component $O^{++}(n,n)$ of the identity, nonpositive on $O^{--}(n,n)$, and identically zero on the two mixed components. This sign structure became a guiding principle for designing fermionic quantum Monte Carlo (QMC) simulations free of the sign problem, unifying previously unrelated solutions and producing new sign problem free models (PRL 115, 250601 (2015)).
A sequel question (How to prove this determinant is positive II?) went further: the diagonal blocks of $A_i$ acquire symmetric positive semidefinite parts, so the exponentials no longer preserve the quadratic form $x^\dagger \eta, x$ but monotonically expand it, forming a semigroup rather than a group, and the determinant stays nonnegative. The first rigorous proof of this stronger statement came from physics, via Majorana reflection positivity (PRL 116, 250601 (2016)); the question asked for an alternate matrix proof, and MathOverflow user jjcale supplied one in the accepted answer, showing that along an analytic path in the semigroup the real eigenvalues can cross $-1$ only in pairs, so the sign of the determinant cannot flip. The comment thread then identified the general Lie algebra level condition $A_i^T \eta + \eta A_i \succeq 0$, which strictly contains the split orthogonal condition $A_i^T \eta + \eta A_i = 0$; this semigroup viewpoint was later developed into a systematic framework (PRB 110, 075146 (2024)). The addendum of the second MathOverflow question is still open: the complex matrix results of arXiv:1601.01994v2 have never been stated in simple matrix language.
The general rule of the game, following the 2015 PRL: in determinantal QMC the partition function of an interacting fermion model takes the form $Z = \sum_{\mathcal{C}} f_{\mathcal{C}} \det\left(I + e^{A_1} e^{A_2} \cdots e^{A_N}\right)$, where the matrices $A_i$ are effective single particle Hamiltonians (hopping, pairing, auxiliary field vertices) depending on the Monte Carlo configuration $\mathcal{C}$, and $f_{\mathcal{C}}$ is a scalar prefactor that can typically be arranged to be nonnegative. A structured set $\mathfrak{g}$ of matrices solves the sign problem for a whole family of models if $\det\left(I + e^{A_1} \cdots e^{A_N}\right) \ge 0$ for every $N$ and all $A_i \in \mathfrak{g}$. Two such sets are known: the split orthogonal Lie algebra $A^T \eta + \eta A = 0$ and its semigroup cone $A^T \eta + \eta A \succeq 0$. The challenge is to find more.
Two features make this territory ideal for AI assisted research today. First, every conjecture has an instant numerical oracle: sample random generators in a candidate class, multiply the exponentials, and check the sign of the determinant. Second, the historical record proves the loop from numerical observation to theorem can close within days when enough sharp eyes are on the problem; AI agents now put many sharp eyes at every student's disposal. As the 2015 paper concluded, its conditions "are by no means the necessary conditions for a sign-problem-free QMC simulation. There should be more guiding principles of this kind."
Research objective
-
Learn the story and rebuild the oracle. Read the two MathOverflow threads (including the comments, where much of the action happened), Tao's blog post, and the two PRLs. Build a verification harness for the rule of the game: sample matrices $A_i$ from a candidate set, form $\det\left(I + e^{A_1} \cdots e^{A_N}\right)$, and test the sign across dimensions, depths $N$, and many random samples. Validate the harness in both directions against the known theorems: the determinant must come out nonnegative on the split orthogonal Lie algebra and on its semigroup cone, and the harness must also detect the sign violations that the same theorems predict on the other components of $O(n,n)$. A harness that passes these checks is the entry ticket to the hunt.
-
Understand the state of the art. Map what is already covered: the split orthogonal theorem, the Kramers time reversal principle (PRB 71, 155115 (2005)), Majorana positivity, and the semigroup conditions of PRB 110, 075146 (2024). Distill this into a written reduction checklist: given a candidate class, how would one recognize that it reduces to a known one (by a similarity transformation, a Kramers pairing argument, or the semigroup conditions)? This checklist is the novelty filter for everything that follows.
-
Push the frontier with AI. Candidate directions, roughly ordered by difficulty; each either survives massive randomized testing, falls to a certified counterexample, or reduces to a known class, and every one of these outcomes is a reportable result:
- the real symplectic group $Sp(2n,\mathbb{R})$ and other classical groups where the answer is likely a quick counterexample;
- the split unitary group $U(n,n)$, where the determinant is complex and the question becomes whether its phase is constrained (a connection to sign easing);
- a systematic sweep over the classical groups attached to the Altland Zirnbauer tenfold symmetry classes, filling in a periodic table of determinant sign structures in which the known results occupy only a few entries;
- the semigroup cone generalization of each surviving group entry;
- a clean matrix formulation of the complex results of arXiv:1601.01994v2, resolving the open addendum of the second MathOverflow question;
- a fully open hunt: let AI agents propose their own structured generator sets (linear subspaces plus cones of real or complex matrices) against the oracle, subject to the novelty filter.
House rules, learned from the story itself: a counterexample claim requires an exact arithmetic certificate in rational or symbolic form; a survival claim requires large randomized tests over dimensions and depths plus a documented proof attempt. Above all, keep the determinantal QMC constraint in view throughout: the goal is matrix classes that can actually appear as Monte Carlo weights $\det\left(I + \prod_i e^{A_i}\right)$ of fermionic lattice models, with the $A_i$ coming from physical bilinears such as hopping, pairing, and auxiliary field vertices. A discovery is complete only when it is mapped to an interacting model following the recipe of PRL 115, 250601 (2015), with special credit for any model that escapes half filling on a bipartite lattice. A positivity statement with no route to a physical weight is a curiosity, not a solution of anything.
-
Public endgame. Any verified discovery is drafted for the outside world, continuing the open science tradition in which this problem was born: a MathOverflow question titled "How to prove this determinant is positive III", an answer to an existing question, or a short arXiv note.
Verification plan
- Theorem grade anchors: the $O(n,n)$ sign structure (Tao and Harcos, 2015) and the semigroup theorem (Wei, Wu, Li, Zhang, Xiang, 2016; alternate proof by jjcale on MathOverflow, 2016; general framework in Wei, 2024) as exact ground truth for the harness; the components of $O(n,n)$ with nonpositive or vanishing determinant serve as negative controls against a harness that silently accepts everything.
- A ladder of verification channels: empirical numerics first (randomized sampling against the oracle, over a range of dimensions and product depths); exact rational or symbolic arithmetic for any counterexample claim, never floating point alone, since determinants near zero are the known numerical trap of this problem family; a human readable proof for any survival claim; and, at the top of the ladder, formalization in Lean for proved statements, with the split orthogonal theorem itself as a natural first target.
- Novelty filter: each claimed new class passes the written reduction checklist against all known classes before being called new.
- Physical relevance: every claimed class must be accompanied by an argument that it is realizable inside a determinantal QMC algorithm, so that the inequality certifies nonnegative Monte Carlo weights for a physical problem rather than standing as an isolated random matrix inequality.
- Full reporting: every claim ships with the generator definition, sampling protocol, matrix dimensions, sample counts, and the harness code, so any reader can rerun the oracle.
Why this may lead to research output
The traffic between physics and mathematics has run in both directions here: the 2015 MathOverflow question grew into a PRL, while the 2016 MathOverflow question was asked in the opposite direction, inspired by an existing physics preprint, and attracted an independent mathematical proof. Both directions remain open to students today. The periodic table over the tenfold symmetry classes is unexplored territory with immediate physical meaning, the complex case of Majorana positivity is an explicitly posed open formulation problem, and any new class is simultaneously a theorem candidate for mathematicians and a new family of sign problem free QMC algorithms for physicists. Even the negative outcomes, certified counterexample tables for natural candidate classes, are citable groundwork.
References
- MathOverflow, How to prove this determinant is positive? (2015); How to prove this determinant is positive II? (2016)
- T. Tao, The standard branch of the matrix logarithm, blog post (2015)
- L. Wang, Y.-H. Liu, M. Iazzi, M. Troyer, G. Harcos, PRL 115, 250601 (2015)
- Z. C. Wei, C. Wu, Y. Li, S. Zhang, T. Xiang, PRL 116, 250601 (2016)
- Z.-C. Wei, PRB 110, 075146 (2024)
- C. Wu, S.-C. Zhang, PRB 71, 155115 (2005)
- Z.-X. Li, H. Yao, Annu. Rev. Condens. Matter Phys. 10, 337 (2019)
- A contemporary account of the story: E. Brown, Sign problems, Terry Tau, and open science, This Condensed Life (2015)
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the verification plan and the two MathOverflow threads, Tao's post, and the cited PRLs. Build the determinant-sign oracle described in the research objective, then validate it against the split orthogonal and semigroup cases plus the negative controls. Done means a documented, rerunnable harness and a reduction checklist; broader discoveries are separate research work.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- python
- Domain
- testing-qa, tooling
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Quiet
- Clarity
- Needs clarification
- Newbie friendliness
- 15/100