Open registry federation

Mathematical findings

639 source-grounded records. Verification labels remain separate from source authentication and publication status.

Imported from VibeMathed under CC BY 4.0. Each record links to its registry entry and named primary source. Registry verification is preserved verbatim.

combinatoricsAug 19, 2026Significance 8/100Registry: unreviewed

The 4-color Rado number of x+y+c=z: general case

Prior state unknownproved

The claim is R(c)=40c+41R(c) = 40c+41 for every c2c \ge 2, reduced to three finite facts: the base value R(2)=121R(2) = 121, and the unsatisfiability of a 321-position and a 521-position spoke template. The reduction is Lean-checked and holds for every D1D \ge 1; the two unsatisfiability results carry DRAT proofs. This completes the partial entry for the same conjecture, which proved it for roughly two thirds of integers via a sc…

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
probability-statisticsAug 18, 2026Significance 8/100Registry: unreviewed

Fourth-moment conjectures for Rademacher sums

Prior state unknownproved

Four results, and the first is partly a refutation. Jakimiuk conjectured cp=μp1c_p = \mu_p - 1 is optimal for every p3p \ge 3; the paper proves that for p4p \ge 4 and gives a counterexample for every 2<p<42 < p < 4, so the conjecture is false as posed and the corrected range is p4p \ge 4. The witness is the two-coordinate vector S2=(ε1+ε2)/2S_2 = (\varepsilon_1+\varepsilon_2)/\sqrt2. The Baranski-Murawski-Nayar-Oleszkiewicz flat-po…

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
algebraAug 14, 2026Significance 8/100Registry: unreviewed

Tarizadeh's Conjecture on the Maximality of Purely-Prime Ideals

Prior state unknowndisproved

Every purely-maximal ideal of a commutative ring is purely-prime, and the converse holds for several important classes of rings; Tarizadeh conjectured (Conjecture 5.8 of his earlier published paper) that in a commutative ring every purely-prime ideal is purely-maximal. False: there is a commutative ring with a purely-prime ideal that is not purely-maximal.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJan 27, 2026Significance 8/100Registry: lean checked

A Generalization of Boppana's Entropy Inequality

Prior state unknownproved

A generalization of Boppana's entropy inequality, of the kind used in union-closed-sets arguments, proved and formalized: the sharp form with the extremal constant characterized via the unique positive solution of an explicit equation.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
probability-statisticsAug 11, 2026Significance 8/100Registry: unreviewed

Predicting Diagonalizability of a Mean Matrix

Prior state unknownproved

The general principle is the interesting part: every semialgebraic property of a bounded fixed-dimensional mean parameter is eventually almost surely predictable. Against merely integrable matrix laws it fails from dimension two.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
differential-equationsOct 26, 2025Significance 8/100Registry: unreviewed

Curto et al.'s Minimality Conjecture for Threshold-Linear Networks

Prior state unknowndisproved

Curto et al. (Advances in Applied Mathematics, 2024) conjectured that every stable fixed point of a threshold-linear network is minimal. Disproved: an explicit competitive 3-neuron TLN has a stable fixed point whose support strictly contains another's, and 3 neurons is proven smallest possible.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
number-theoryApr 20, 2026Significance 8/100Registry: lean checked

Nathanson's Problems on Product Intersection Sets

Prior state unknownproved

Nathanson asked which subsets of N\mathbb{N} can occur as product intersection sets of a family of semigroup subsets, for arbitrary and for decreasing families (his Problems 10 and 11). Both are solved by complete classifications.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
theoretical-computer-scienceJul 9, 2026Significance 7/100Registry: unreviewed

Minimum Edge-Outerplanar Embedding

Prior state unknownproved

Can the minimum edge-outerplanarity of a finite loopless planar graph, minimized over all planar embeddings, be computed in polynomial time? Asked by Bentz in 2009.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
theoretical-computer-scienceJul 28, 2026Significance 7/100Registry: unreviewed

Probabilistic Automatic Complexity Is At Most Three

Prior state unknownproved

Gill introduced the probabilistic automatic complexity AP(w)A_P(w) of a string: the least number of states of a probabilistic finite automaton for which ww is the unique most probably accepted string of its length. He asked whether APA_P is unbounded, no string with AP>3A_P>3 being known. The paper proves AP(w)3A_P(w)\le 3 for every string over every finite alphabet, with an explicit three-state witness.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
algorithms-optimizationJun 18, 2026Significance 7/100Registry: lean checked

The Ramachandra-Natarajan Pairwise Independent Correlation Gap Conjecture

Prior state unknowndisproved

Ramachandra and Natarajan conjectured a bound on the pairwise independent correlation gap in their 2025 Operations Research Letters paper. An explicit counterexample refutes it.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
number-theoryJul 14, 2026Significance 7/100Registry: unreviewed

A Universal Leading-Residue Formula for Witten Zeta Functions

Prior state unknownproved

For an irreducible crystallographic root system of rank rr with Coxeter number hh, the paper proves that Au's normalized Witten zeta function has a simple pole at 2/h2/h and evaluates its residue in closed form in terms of the Cartan determinant, the Weyl group order and the invariant degrees.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
geometry-topologyJul 29, 2026Significance 7/100Registry: unreviewed

Twelve Common Flex Lines in a General Pencil of Cubics

Prior state unknownproved

Does a general pencil of plane cubics over C\mathbb{C} have exactly 1212 common flex lines? Ciliberto, Miranda and Roé asked this in Remark 5.3 of their paper; the answer is yes.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
number-theoryJul 13, 2026Significance 7/100Registry: unreviewed

Ross's Two Conjectures on Nondeficient Numbers

Prior state unknowndisproved

Ross introduced S\mathcal{S}-perfect numbers, integers expressible as 1+λjdj1 + \sum \lambda_j d_j over their proper divisors with coefficients in S\mathcal{S}, and conjectured that they have the same density as the nondeficient numbers, plus a second conjecture relating odd nondeficient numbers to S\mathcal{S}-perfection. Both are false.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 12, 2026Significance 7/100Registry: unreviewed

The Coxeter Code Minimum Distance Conjecture

Prior state unknownproved

Coble and Barg introduced binary Coxeter codes, the span of indicators of standard cosets of fixed rank in a finite Coxeter system, generalizing Reed-Muller codes, and proposed a conjectural value for the minimum distance of a general Coxeter code. The conjecture is true, and it yields a decoding consequence.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
mathematical-physicsJun 8, 2026Significance 7/100Registry: unreviewed

Free Fermions in Disguise without Exponential Degeneracies

Prior state unknownproved

An existence question settled by exhibiting an object, not a general theorem: one model in the family has no exponential degeneracies for generic couplings, and nothing here says which others do. The route is worth recording because it is not the one anyone was looking down. The author had tried and failed to find such a model directly. It surfaced instead from an unrelated classification of medium-range spin chain…

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
logic-foundationsAug 4, 2026Significance 7/100Registry: unreviewed

Signed Depth Relevance of subDL

Prior state unknownproved

subDL satisfies the signed depth relevance property, answering an open question posed by Øgaard (2026). More precisely, every valid inference in subDL contains a propositional variable that occurs in both the premises and conclusion with matching sign and at matching implicational depth.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
number-theorySep 30, 2025Significance 6/100Registry: unreviewed

Cohen's 22 Conjectures on Cyclic Numbers

Prior state unknownproved

22 conjectures of Cohen about cyclic numbers (integers with gcd(n,φ(n))=1\gcd(n, \varphi(n)) = 1) settled at once - 16 proved, 6 disproved - together with a complete resolution of a related OEIS problem on sequences whose running averages are Fibonacci numbers (Fried's Conjecture 2).

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review! Disputed
combinatoricsJul 30, 2026Significance 6/100Registry: unreviewed

Sombor-Energy Conjecture

Prior state unknowndisproved

Does every nontrivial finite simple graph have noninteger Sombor energy? If ρ1,,ρn\rho_1,\ldots,\rho_n are the eigenvalues of the Sombor matrix of a graph GG, its Sombor energy is ESO(G)=i=1nρi.E_{\mathrm{SO}}(G)=\sum_{i=1}^{n}|\rho_i|. The conjecture asserted that ESO(G)ZE_{\mathrm{SO}}(G)\notin\mathbb Z for every nontrivial graph. A connected graph on nine vertices is exhibited with ESO(G)=64E_{\mathrm{SO}}(G)=64, disproving the conject…

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsAug 3, 2026Significance 5/100Registry: unreviewed

Graffiti's Residue Problem for Common-Divisor Graphs

Prior state unknownproved

A problem from Fajtlowicz's Graffiti program, studied by Erdős and Staton, on the Havel-Hakimi residue of common-divisor graphs. The paper resolves the problem and extends it, determining the residue's first-order scale and its nontrivial constant from the degree sequence.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 30, 2026Significance 5/100Registry: unreviewed

Graffiti Conjecture 6

Prior state unknowndisproved

Infinite family of counterexamples; mathematical argument internally checked, with external verification and novelty review pending.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
geometry-topologyJul 29, 2026Significance 5/100Registry: unreviewed

Positivity on Deligne–Mumford Stacks Without the Torsion-Free Hypothesis

Prior state unknownproved

Casalaina-Martin and Zhjeqi proved that the first Chern class of every torsion-free coherent quotient of a tensor power of the logarithmic cotangent sheaf is pseudo-effective, noting in Remark 4.5 that torsion-freeness was imposed only for technical reasons. Can it be dropped? Yes.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
algebraFeb 24, 2026Significance 5/100Registry: unreviewed

Ran-Teng Conjecture 20 on 4-Cycle Stochastic Matrices

Prior state unknownproved

Is the exact nonreal spectral region of the four-cycle family of row-stochastic nonnegative matrices determined by the Karpelevich constraint, as Ran and Teng conjectured in 2024?

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
number-theoryJun 1, 2026Significance 5/100Registry: unreviewed

Divisibility Set of the Generalized Euler Totient

Prior state unknownproved

Define φk(n)=1an,(a,n)=1ak\varphi_k(n) = \sum_{1 \le a \le n, (a,n)=1} a^k and Ds={ks:φs(n)φk(n) for every n}\mathcal{D}_s = \{k \ge s : \varphi_s(n) \mid \varphi_k(n) \text{ for every } n\}. Is D1={1,3,15}\mathcal{D}_1 = \{1, 3, 15\}, as conjectured by Büyükaşik and collaborators?

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
geometry-topologyJun 11, 2026Significance 5/100Registry: unreviewed

IRIS Conjecture 6.1 on Simple 3-Polytopes

Prior state unknowndisproved

For a simple 33-polytope with at least three faces of size at least 77, must p63920+p32p54k7pkp_6 \ge \frac{39}{20} + \frac{p_3}{2} - \frac{p_5}{4} - \sum_{k \ge 7} p_k? Five minimal ten-face counterexamples refute the printed inequality.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJun 12, 2026Significance 5/100Registry: unreviewed

Graffiti Conjecture 143

Prior state unknowndisproved

For every connected graph, is the variance of its positive adjacency eigenvalues at most its order divided by its average distance? Exact dumbbell-graph certificates refute the bound under both conventions for average distance.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsAug 13, 2026Significance 5/100Registry: site confirmed

Nineteen exact reflective and dihedral Ramsey numbers from Damnjanovic-Dordevic's tables

Prior state unknownproved

Nineteen individual exact values, each decided by SAT certificate: unsatisfiable at the claimed nn, witnessed satisfiable at n1n-1. They close cells in DD26's Tables 3-13 but settle no infinite family - the sibling entries do that for the KK column. The three overlap cells are Rdih(P4alt,K6)=16R_{dih}(P_4^{alt},K_6)=16, Rdih(P3alt,K9)=17R_{dih}(P_3^{alt},K_9)=17 and Rdih(P9alt,K3)=17R_{dih}(P_9^{alt},K_3)=17, each an instance of a sibling theorem; the remain…

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 12, 2026Significance 5/100Registry: lean verified

Elizalde-Luo Pattern-Avoidance Conjecture

Prior state unknownproved

Is the number of nonnesting permutations of {1,1,,n,n}\{1,1,\dots,n,n\} avoiding both 11321132 and 33123312 equal to 3n32n1+13^n - 3 \cdot 2^{n-1} + 1 for every n1n \ge 1?

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 23, 2026Significance 5/100Registry: site confirmed

WOWII Conjecture 72: Two induced trees pin down tree(G G )

Prior state unknownproved

The evenly-divided reading of WOWII Conjecture 72 holds: (A+L)/3t, \lceil(A + L)/3\rceil \le t, where t= t = tree(G G ) (order of a largest induced tree), A= A = average eccentricity and L= L = maximum neighbourhood independence number. A stronger reading that divides only L L by three is false. The argument rests on two elementary observations (a diametral path is chordless and therefore induces a tre…

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 31, 2026Significance 5/100Registry: lean checked

The Han-Xiong Integer Trace Conjecture

Prior state unknownproved

Settles the conjecture for a large family and reduces the rest to unit fractions; the general unit-fraction case remains open.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsAug 3, 2026Significance 5/100Registry: lean verified

Written on the Wall II, Graph Conjecture 144

Prior state unknownproved

The Formal Conjectures pull request flipping this from open to solved is still open rather than merged, so the canonical repository has not yet accepted it.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 28, 2026Significance 5/100Registry: lean verified

Written on the Wall II, Graph Conjecture 109

Prior state unknowndisproved

Must every connected graph satisfy the proposed upper bound on its independence number in terms of residue and largest induced-bipartite-subgraph order? The family K2r+1(KrKr)\overline{K}_{2r+1} \vee (K_r \sqcup K_r) violates it for every r3r \ge 3.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsApr 29, 2026Significance 5/100Registry: unreviewed

Hamilton Decompositions of the Directed 5-Torus, Odd Modulus

Prior state unknownproved

The directed five-dimensional torus D5(m)D_5(m) has a Hamilton decomposition for every odd m3m \geq 3, extending the decomposition program for directed tori beyond the three-dimensional case.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
algebraMay 17, 2026Significance 5/100Registry: expert verified

Integral Local Invariant Cycles in Degree One

Prior state unknownproved

For a semistable one-parameter family of complex projective varieties with smooth nearby fiber XtX_t and monodromy TT, is the map H1(X,Z)H1(Xt,Z)TH^1(X, \mathbb{Z}) \to H^1(X_t, \mathbb{Z})^T surjective? True in degree one, although the integral statement fails in higher degree.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 22, 2026Significance 5/100Registry: unreviewed

Graffiti Conjecture 284

Prior state unknowndisproved

If a finite graph has girth at least five, must its minimum dual degree satisfy δ(G)n(G)\delta^*(G) \le -\partial_n(G), where n(G)\partial_n(G) is the smallest eigenvalue of its distance matrix? The Hoffman-Singleton graph violates it: dual degree 77 against eigenvalue bound 44.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsMay 21, 2026Significance 5/100Registry: lean verified

Written on the Wall II, Graph Conjecture 2

Prior state unknownproved

For a finite connected graph GG, let Ls(G)L_s(G) be the maximum number of leaves in a spanning tree and (G)\ell(G) the average local independence number. Must Ls(G)2((G)1)L_s(G) \ge 2(\ell(G) - 1)?

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review
combinatoricsJul 30, 2026Significance 5/100Registry: lean verified

Written on the Wall II, Graph Conjecture 217

Prior state unknownproved

VibeMathed records this result as “Written on the Wall II, Graph Conjecture 217.” The registry entry and named primary source contain the available statement and scope.

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review