We work on frontier problems in mathematics and build systems where AI and mathematicians explore, reason, challenge, and verify together. Our results now span arithmetic dynamics, algebraic geometry, rough integration, kinetic theory, and quantum information.
VDL / Discovery system
AI×Mathematicians
Advanced interaction systems and working modes for sustained collaboration between mathematical judgment and machine intelligence.
Research results
First known resolutions
To our knowledge at the time of publication, each result below was the first resolution of its question within the stated scope.
Each entry shows when the question was posed and when our result was published.
Posed
Quantum information · Representation theory
Entropy minima for fermionic states
Do coherent states minimize Wehrl and every positive-order Rényi–Wehrl entropy in the basic fermionic representations?
Full Husimi convex order and sharp entropy minima, with equality cases, hold for all basic exterior powers and fundamental half-spin and odd-spin representations. The exterior-power comparison and minimizers are formalized end to end; spin extensions and explicit constants have paper proofs. Higher highest-weight multiples are outside the scope.
Every p-normal set is realized exactly, including finite modifications, by a finite-order linear recurrence over Fₚ(t). The recurrence varies with the set; the coefficient field stays fixed.
For every fixed 0 < d < 1/2, every measurable, finite-a.e. invariant is a linear combination of a constant and the energy. Regularity is a consequence, not an assumption; we also establish a spectral gap and closed collision operator.
A larger projective embedding gives an extension over the original field, preserving both the original map and its degree. There is no need to replace the map by an iterate.
An explicit polynomial system in every prime characteristic admits no such universal seed. Retained-coordinate inseparable degree detects an obstruction that pointwise iteration cannot see.
For a fixed cubic plane birational map over F₂, that proportion has liminf 0 and limsup 1. This refutes the asymptotic-density claim in part (b), not the separate Zariski-density statement in part (a).
A degree-eighteen polynomial rules out every three-term decomposition, including cross-copy couplings. Gaussian rank is multiplicative for two nonzero four-mode even states. This is a paper theorem; the rank bounds and coordinate certificates are formalized, but the end-to-end rank-four proof remains in progress.
In the critical variation class, one boundary occupation density determines the area record on every subarc, and every allowed density is realized by one sequence of smooth embedded curves. The full space is compact and convex, with extreme points given by zero-or-one occupations.
With the Asano–Ike criterion, the construction yields prescribed rectangles when the coordinates have finite strong p- and q-variation, with p, q > 1 and 1/p + 1/q = 1, including finite strong quadratic variation. This advances the known range of a classical problem; the unrestricted problem remains open. The external rectangle criterion is not part of the Lean proof.
For wave kinetics with a fixed cube cutoff, we prove a fluid limit throughout a prescribed smooth, positive Euler interval, even as corner modes retain transport memory. We also determine the Onsager tensor’s seven-dimensional kernel and rank eight.
Full statements and proofs are in the linked preprints. Formal verification covers the components documented in each repository; some end-to-end formalizations remain in progress. Verification scope: arithmetic dynamics · kinetic theory · fermionic states · boundary occupation.
Current research
From exploration to checked knowledge.
01
Frontier mathematics
We take on difficult problems at the frontier of mathematics, where new structures and proof strategies have to be found.
02
Verification methods
Proof auditing, exact computation, and formal checking that connect every result to the claim it actually establishes.
03
Mathematics in use
Transferring new structures and verified results into difficult problems across science, engineering, and industry.
Human × AI
A new mode of mathematical collaboration.
We develop advanced systems and research protocols for AI and mathematicians to work as one discovery loop—from search and conjecture to proof and independent checking.
New answers, reusable methods, and a growing body of verifiable mathematics.
