THE OMEGA INSTITUTE / RESEARCH

Research highlights

The questions we resolve. The ideas they make possible.

1,076 proofs · 620 refutations. Each result links a question from the literature to its precise formal statement and released Lean evidence.

1,696resolved results

Questions from the literature.
Answers checked by Lean.

Explore the release history ↗

Selected results

Browse the full result order ↗

Rocky Mountain J. Math. 15 (1985)Editorial selection

Source excerpt

“I would not be surprised if 23 is the only counterexample.”
P. Erdős

Our answer47

Erdős suggested 23 might be the only counterexample. 47 is another.

Only the proposed uniqueness of 23 is refuted; conjecture (22) and the classification of all counterexamples remain outside this result.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

p. 361

The questionPut (21) ∏{i=1}^{k} (x + i) = uk(x) vk(x), (uk(x), vk(x)) = 1 where vk(x) is squarefree and all prime factors of uk(x) occur with an exponent greater than 1.

Why it mattersThe paper identifies 23 as a counterexample and proposes that it could be the only one.

The ideaFor 1 ≤ k ≤ 78, split the interval into 1..30, 31..60, and 61..78.

Our contributionThe starting value 47 refutes the proposed uniqueness of 23 among starting values whose consecutive products always have dominant repeated factors.

Scope & next questionIt makes no claim about conjecture (22), an estimate of k0(x), the assertion that 23 and 47 are the only counterexamples, or the statement that 23 itself is a counterexample.

Explore the result ↗

Annals of Probability 51 (2023)Editorial selection

Source excerpt

“May Var(ζ₁ + … + ζ_t) be sublinear? We do not have an answer.”
I. Benjamini, H. Helman Tov, M. Zhukovskii

Our answerNo

The noisy voter model: the repetition variance is never sublinear

Synchronous noisy voter dynamics on connected locally finite simple graphs with a neighbor at every vertex, fair independent opinions, noise 0 < ε < 1 and positive lag.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

§2.2 · arXiv:2207.01224v2, p. 6

The questionZhukovskii, Global information from local observations of the noisy voter model on a graph, Annals of Probability 51(5), 1963–1992 (2023), Section 2.2, asks:

Why it mattersThe question distinguishes the linear and logarithmic branches of Lemma 2.3 for a local statistic observed through time.

The ideaPairing its future fair coin with its flip gives a contribution of half this mass.

Our contributionNoisy voter repetition counts have a positive linear variance lower bound.

Explore the result ↗

Phys. Rev. A 111 (2025)Editorial selection

Source excerpt

“Open problem. Does there exist a distribution p(A,B,C) that is local in the triangle network and fully symmetric such that p(A=B=C) > 1/4?”
E. Bäumer, V. Gitton, T. Kriváchy, N. Gisin, R. Renner

Our answerYes: 41/144

A fully symmetric local triangle model beats 1/4

Four outcomes per party, independent local triangle sources, and symmetry under party permutations and joint outcome relabelings. The witness refutes the universal 1/4 bound.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conclusion · arXiv:2405.08939v1

The questionA 111, 052453 (2025)) study classical (local) models in the triangle network with four outcomes per party.

Why it mattersFully symmetric distributions with four outcomes include the distribution of the Elegant Joint Measurement, the main candidate for noise-robust quantum nonlocality in the triangle network, and the local value of p(A = B = C) calibrates the Bell-type inequalities used to certify such nonlocality.

The ideaEach source sends one of the 12 ordered pairs x = (x₁, x₂) of distinct outcomes, uniformly; every party applies f(x, y) = x₂ if x₂ ∈ {y₁, y₂} and x₁ otherwise, with a = f(β, γ), b = f(γ, α), c = f(α, β).

Our contributionThere is a distribution that is local in the triangle network and fully symmetric, with four outcomes per party, such that p(A = B = C) = 41/144 > 1/4.

Explore the result ↗

More research highlights

J. Math. Phys. 50 (2009)Editorial selection

Source excerpt

“The main open question of the present work is to show that this is indeed the case.”
F. Hiai, M. Mosonyi, M. Hayashi

Our answerNo: a corner at s = ½

Hiai, Mosonyi and Hayashi’s main open question: ψ need not be differentiable

A finite-group counterexample with faithful states and the stated asymptotic convergence premise; the question is differentiability of ψ on (0, 1).

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

§7 · arXiv:0904.0704v2

The questionHayashi, Quantum hypothesis testing with group symmetry, J.

Why it mattersDifferentiability would provide a route to matching asymptotic hypothesis testing bounds.

The ideaBoth diagonal matrices are positive definite and have trace one.

Our contributionA faithful four-level example with a corner in its asymptotic overlap.

Explore the result ↗

PRX Quantum 3 (2022)Editorial selection

Source excerpt

“Conjecture: θ^C_{d≥5} = 1.”
P.-E. Emeriau, M. Howard, S. Mansfield

Our answerProved for every d ≥ 5

The Torpedo Game has a perfect classical strategy in every dimension d ≥ 5

Perfect classical winning probability for the dimension-d Torpedo Game, for every integer d ≥ 5; the source had checked 5 ≤ d ≤ 23.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conjecture · arXiv:2007.15643v2

The questionMansfield (arXiv:2007.15643, quant-ph; PRX Quantum 3, 020307 (2022)) introduce the dimension-d Torpedo Game: Alice receives x, z ∈ Zd and sends one dit; Bob is asked q ∈ {∞, 0, …, d − 1} and must answer a ≠ x for q = ∞ and a ≠ qx − z otherwise.

Why it mattersThe quantum Torpedo Game is won perfectly for d ≥ 3 by a qudit strategy built from stabilizer states, while d = 2, 3 show a classical–quantum gap.

The ideaA deterministic strategy is a colouring E of the d × d grid with d colours and a decoding D; it is perfect iff D(E(x, z), q) differs from the forbidden label for every (x, z, q).

Our contributionFor every d >= 5, the dimension-d Torpedo Game has a perfect classical strategy: the classical value, the greatest winning probability of a one-dit prepare-and-measure strategy with shared randomness, equals 1.

Explore the result ↗

IEEE Trans. Inf. Theory 51 (2005)Editorial selection

The question · paraphrased

Can a 2×4×4 experiment using joint measurements on pairs of Bell singlets be more than twice as strong as CHSH?
W. van Dam, R. D. Gill, P. D. Grünwald

Our answerYes

Two singlets are more than twice as strong as CHSH

Statistical strength means KL divergence in bits, under the uniform, product and correlated setting distributions defined in the source.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conjecture 5 · §VI.D, p. 11

The questionGrünwald, “The Statistical Strength of Nonlocality Proofs”, IEEE Transactions on Information Theory 51(8), 2812–2835 (2005), arXiv:quant-ph/0307125v2, Section VI.D, p. 11, Conjecture 5 states:

The ideaThe commuting rows and columns of the Mermin–Peres square provide the first three PVM settings.

Our contributionFour joint settings on two literal singlets beat twice CHSH under all three statistical-strength conventions.

Explore the result ↗

arXiv:2502.12240 (2025)Editorial selection

Source excerpt

“Conjecture 1 For any T_AB on a finite-dimensional H_A ⊗ H_B and p > 1: 1 + ||T_AB||_p ≥ ||Tr_A T_AB||_p + ||Tr_B T_AB||_p.”
A. Milekhin, Z. Adamska, J. Preskill

Our answerNo: a witness at p = 2

Spacetime density matrices violate Schatten subadditivity

A three-qubit witness at Schatten exponent p = 2 refutes Conjecture 1 for spacetime density matrices.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conjecture 1 · arXiv:2502.12240v2

The questionPreskill, Observable and computable entanglement in time, arXiv:2502.12240v2, define the spacetime density matrix TAB of a subsystem A at time 0 and a subsystem B at time t. - The definition. Tr(TAB (OA ⊗ 1B)(1A ⊗ OB)) = ⟨OA(0) OB(t)⟩ = Tr(ρ OA U† OB U) (Eqs. (4), (9)); A and B "do not have to be related to each other in any particular way".

Why it mattersThe spacetime density matrix extends reduced density matrices to subsystems at different times, and its Rényi-type quantities continue timelike entanglement in field theory.

The idea1. The witness. Three qubits Q, R and S, with A = B = Q, the same qubit at times 0 and t.

Our contributionA rational pure state of three qubits violates Schatten subadditivity for a qubit observed at two times.

Scope & next questionThe numerical evidence of the paper is consistent with the whole-system case, which remains open.

Explore the result ↗

arXiv:2605.21457 (2026)Editorial selection

Source excerpt

“This channel is optimal for m ≤ n (see Ref. [S2]), and we conjecture that it is also optimal for m > n.”
Z. Li, E. Theil, A. W. Harrow, I. Chuang

Our answerNo, already at d = 2

Purify-and-clone is not optimal beyond m = n

The counterexample has n = 1, m = 2 and d = r = 2, under the one-site worst-case squared-infidelity reading.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

§S3 A · arXiv:2605.21457v2, p. 9

The questionChuang, An Exponential Sample-Complexity Advantage for Coherent Quantum Inference, arXiv:2605.21457v2, Section S3 A, p. 9, states:

Why it mattersCloning the entire system-environment register and cloning the system before adjoining a symmetric environment have different one-site risks.

The ideaThe proof uses convexity.

Our contributionA symmetric quantum channel has one-site worst-case infidelity at most one sixth, while purify-and-clone has risk at least one fifth in system and environment dimension two.

Explore the result ↗

J. Math. Phys. · arXiv:1508.03551Editorial selection

Source excerpt

“Conjecture 6.3. Equality holds in (45c) through (45e) above.”
F. Hiai, M. B. Ruskai

Our answerAll three equalities hold

Hiai and Ruskai's exact contraction coefficients hold

All three equalities (45c–45e) for the specified non-unital qubit CQ channel, on the full parameter domain stated in Conjecture 6.3.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conjecture 6.3 · arXiv:1508.03551v1, p. 19

The questionA quantum channel makes states harder to distinguish. What is its exact contraction under different information-geometric metrics?

Why it mattersHiai and Ruskai proposed three optimal bounds in their 2015 preprint. The question asks whether each bound is attained when all admissible states and tangent directions are considered.

The ideaA common input estimate and positive kernel representations control all three metrics. The maximally mixed state and a Pauli direction attain the bounds.

Our contributionWe establish all three exact contraction coefficients for the stated family of qubit channels: dual Wigner–Yanase, geometric and Bogoliubov–Kubo–Mori.

Scope & next questionThis resolves the three metrics in Conjecture 6.3. A formula for every kernel in the broader metric class remains outside this result.

Explore the result ↗

J. Symbolic Comput. · arXiv:2401.08481Editorial selection

Source excerpt

“Moreover, the following identities are conjectured to hold for all n ≥ 3:”
C. Koutschan, C. Krattenthaler, M. Schlosser

Our answer(10.10) holds for all n ≥ 3

Koutschan, Krattenthaler and Schlosser's equation (10.10) is proved

This result proves the complete chain of equalities in equation (10.10), for all n ≥ 3. The other equations of Conjecture 23 are separate results.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conjecture 23 · equation (10.10)

The questionKoutschan, Krattenthaler and Schlosser, arXiv:2401.08481v1, Conjecture 23, states: “Moreover, the following identities are conjectured to hold for all n ≥ 3:”.

Why it mattersThe determinant families share a rational column transformation.

The ideaThe multiplier has constant coefficient one, so its lower triangular coefficient matrix preserves determinants.

Our contributionThe binomial determinant identities follow from a common column multiplier and triangular determinant reductions.

Explore the result ↗

Erdős on Mahler (1989)Editorial selection

Source excerpt

“In fact, the only nontrivial solution he found was 7^3 + 7^2 + 7 + 1 = 20^2, and perhaps there are no others”
P. Erdős, recalling K. Mahler

Our answer521² = 111101₁₂

Mahler's 0/1-digit square was not unique

A counterexample to the suggested uniqueness of a nontrivial coprime 0/1-digit square, as recorded by Erdős; not Mahler’s fixed-base finiteness conjecture.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

p. 2

The questionErdős's 1989 reminiscence, page 2 (verbatim):

Why it mattersThe source presents the base-7 identity as Mahler's only known nontrivial example and immediately suggests that no others may exist.

The ideaThe finite certificate first proves Nat.Coprime 12 521 and 12^5 + 12^4 + 12^3 + 12^2 + 1 = 271441 = 521^2.

Our contributionA coprime base-12 square contradicts the reported uniqueness of Mahler's nontrivial binary-digit example.

Scope & next questionThis refutation makes no claim about Mahler's finiteness conjecture for any fixed k > 4 and no claim about infinitude for k = 2, 3, 4.

Explore the result ↗

arXiv:2010.14682 (2020)Editorial selection

The question · paraphrased

Must a locally strictly contracting channel uniformly contract trace-norm conditional mutual information?
C.-F. Chen, K. Kato, F. G. S. L. Brandão

Our answerNo such η

No uniform contraction for trace-norm conditional mutual information

A qubit channel with local trace-norm contraction ratio at most 1/√2 refutes the claimed uniform contraction of trace-norm conditional mutual information.

✓ Lean 4 kernel-checked Original question ↗

Mathematical idea & verification details

Conjecture III.2 · arXiv:2010.14682v3, p. 17

The questionBrandão, Matrix Product Density Operators: when do they have a local parent Hamiltonian?, arXiv:2010.14682v3, Section III.C (PDF p. 17), Conjecture III.2:

Why it mattersThe source studies whether matrix product density operators are Gibbs states of quasi-local parent Hamiltonians through the decay of conditional mutual information.

Our contributionA flagged measurement in two qubit bases strictly contracts local trace distance while preserving the trace-norm conditional mutual information of a tripartite state.

Explore the result ↗

A universal matrix bound reveals a hidden geometry

When does a bound on every positive block matrix force its off-diagonal block to have a special structure?

Every complex matrix satisfying the proposed bound for all positive block completions is essentially Hermitian: it is an affine complex transform of a Hermitian matrix.

Why it mattersBourin and Lee posed this question in 2021. It connects a norm inequality to the geometry of a matrix, and includes an earlier normality question of Hayashi.

The ideaFinite rank-one perturbations expose the extreme eigenvalues. Their symmetry forces normality; a second identity reconstructs the affine Hermitian structure in every dimension.

Scope & next questionThe result gives a structural implication for the operator norm. An algorithm producing violating completions and extensions to other norms remain open.

Explore the result ↗Original question ↗

Publications

arXiv:2611.04568Preprint

2026-11-03 / Preprint

Time-invariant negativity and persistent bound entanglement in a cyclic two-qutrit family

Wenlin Zhang, Mazhar Ali, Haobo Ma

arXiv:2611.04568

For a cyclic two-qutrit family under collective dephasing, the paper gives exact PPT and separability regions along the whole trajectory with explicit certificates, and a closed-form negativity. The entanglement is time-invariant exactly when the weight of the maximally entangled state exceeds r/(1+r+r^2); below that threshold it either dies suddenly or, for r different from 1 in an intermediate range, loses distillability and stays bound entangled at all later times.

Read article

Source & evidence

https://arxiv.org/abs/2611.04568v1

arXiv:2610.05623v2Preprint

2026-11-03 / Preprint

Approximation of a continuous-variable Gaussian state by discrete-variable quantum states

Nicolae Cotfas, Haobo Ma, Wenlin Zhang

arXiv:2610.05623v2

For every centered one-mode Gaussian state, the signed Wigner periodization is a discrete-variable density operator in every odd dimension d at least 3, and positivity is equivalent to the one-mode uncertainty condition. A covariance-independent isometric embedding gives exponential convergence in trace norm with an explicit error bound uniform in Planck's constant.

Read article

Source & evidence

https://arxiv.org/abs/2610.05623v2

2026-10-31 / Preprint

Maximal input entropy for binary two-deletion and two-insertion channels

Haobo Ma, Wenlin Zhang

arXiv:2611.01064v1

Independent public preprint by Haobo Ma, Wenlin Zhang.

Read article

Source & evidence

https://arxiv.org/abs/2611.01064

2026-10-29 / Preprint / cs.FL, math.CO

Block-exchange descent for insertion: commuting projections and minimum masks

Haobo Ma, Wenlin Zhang, Charles E. Hughes

arXiv:2610.39941

A block exchange from a minimum insertion mask of degree r has minimum degree exactly r − 1 among masks with commuting source projections. The paper proves exact descent for unary sources, repairs an infinite periodic degree-three family, and establishes a separate no-gap theorem for minimum iteration depths of arbitrary languages.

Exact commuting-mask descent; iteration-depth no-gap theorem formalized in Lean

General block-exchange descent and the Singleton No-Gap problem remain open.

Read article Code & verification

Source & evidence

Title, authors, submission date and scope checked against arXiv:2610.39941v1, submitted 29 October 2026, and its PDF. Computer-assisted first-mask descent covers combined length seventeen over every alphabet; degree-three first-mask descent and repair cover length thirty. The paper cites HughesIterationDepthNoGap.lean at revision 16f6e1a0d882 for the iteration-depth theorem over arbitrary languages and alphabets. The computational supplement is public as release v1.0. Pages does not replay the computations or Lean build.

2026-10-21 / Preprint / math.NT

Residue Sums Modulo Products of Two Distinct Odd Primes

Haobo Ma, Mircea Merca, Wenlin Zhang

arXiv:2610.29608

When does the sum of residues in a multiplicative period modulo pq equal pqk/2? For distinct odd primes p and q and even period length k, character-sum criteria give index-four classifications and an infinite index-six family. A reproducible census of 75,090 eligible cyclic subgroups distinguishes balance of a subgroup from balance of all its cosets.

Index-four balance criteria and an infinite index-six cancellation family

Read article Code & verification

Source & evidence

Title, authors, submission date and scope checked against arXiv:2610.29608v1, submitted 21 October 2026, and its PDF. The census covers pq ≤ 10000 and finds 101 mixed index-four subgroups centered themselves but not on every coset. The paper cites Lean formalizations only for the counterexample (a, m) = (2, 15) to Merca’s Conjecture 1 and the distinct prime-modulus lifted identity in Conjecture 2; these do not constitute a formalization of all structural results. The public residue-sums-pq-data repository contains the data package and provenance. Pages does not replay those checks.

2026-10-16 / Preprint / math.CO

Sharp zero forcing numbers for the generalized Petersen graphs P(n,3) and P(n,4)

Arnav Krishnan, Haobo Ma, Wenlin Zhang

arXiv:2610.24059

The zero forcing numbers are Z(P(n,3)) = 8 for every n ≥ 13 and Z(P(n,4)) = 10 for every n ≥ 18. Both thresholds are sharp, and the paper gives exact values for all smaller admissible n. The first equality proves Krishnan’s Conjecture 5.

Sharp thresholds 13 and 18; k = 3 formalized in Lean, k = 4 checked with DRAT certificates

Read article Code & verification

Source & evidence

Title, authors, first submission date and scope checked against arXiv:2610.24059v1, submitted 16 October 2026, and its PDF. The k = 3 stabilization theorem is formalized in Lean 4 at upstream revision 7ee4c64c. The k = 4 proof combines a mathematical reduction with 89 boundary formulas, 11 fort formulas, independently checked DRAT certificates and explicit forcing sequences. Its Lean formalization remains incomplete. The public v2-full release includes the complete certificate archive. Pages does not replay either verification pipeline.

2026-10-14 / Preprint

Generation by lazy and invertible cellular automata over the Klein four-group

Edgar Alcalá-Arroyo, Alonso Castillo-Ramirez, Haobo Ma, Wenlin Zhang

arXiv:2610.20329

For G = C2 × C2 and A = {0, 1}, the submonoid of CA(G; A) generated by lazy and invertible cellular automata is characterized: a cellular automaton belongs to it exactly when, whenever it maps the two free G-orbits onto the same free orbit, it also maps both constant configurations and some two-point orbit to the same constant. The proof factors every member through elementary orbit collapses and three two-cell lazy maps.

59,712 generated maps; the criterion and both cardinalities are verified in Lean

Read article Code & verification

Source & evidence

https://arxiv.org/abs/2610.20329

2026-10-13 / Preprint

On the coincidence of discrete and continuous definitions of Entanglement of Formation

Haobo Ma, Maksim E. Shirokov, Wenlin Zhang

arXiv:2610.18816

Every Borel ensemble of pure states on a separable bipartite Hilbert space with finite average entanglement admits a countable ensemble with the same barycenter and arbitrarily small additional average entanglement. Consequently the discrete and continuous definitions of the Entanglement of Formation coincide on the whole state space of an infinite-dimensional bipartite quantum system, with infinite values allowed.

Discrete and continuous Entanglement of Formation coincide in infinite dimensions

The arXiv record describes the current version as preliminary and invites comments; the authors state that the main proof idea was realized with AI assistance.

Read article

Source & evidence

https://arxiv.org/abs/2610.18816

2026-09-27 / Preprint

A Padovan-automatic description of a nested recurrence

Benoit Cloitre, Haobo Ma, Wenlin Zhang

arXiv:2609.33421

A finite-state description of the nested recurrence OEIS A076502 in the greedy Padovan numeration system. The paper proves the exact floor-offset set {−1, 0, 1, 2}, bounded discrepancy, and an explicit 26-letter morphic presentation of the first-difference word with least balance constant four.

Recurrence identification, exact offsets and balance four formalized in Lean

Read article Code & verification

Source & evidence

https://arxiv.org/abs/2609.33421

2026-09-20 / Preprint

Sub-quorum colorings of graphs

Haobo Ma, Rafik Sahbi, Wenlin Zhang

arXiv:2609.25128 / v4 updated 10 October 2026

Structural bounds, algorithms and exact values for partial vertex colorings in which each colored vertex has a weak majority of its colored closed neighborhood in its own color. Results include a linear-time algorithm on trees, NP-completeness on bipartite graphs, exact rectangular-grid values for every fixed width from two through eleven, and the hypercube identity ψsq(Qn) = β2(Qn) = 2^(n−1) for every n ≥ 2.

Exact hypercube values in every dimension n ≥ 2; grid strips of widths 2–11

The arbitrary-width rectangular-grid sub-quorum formula remains a conjecture; the reported strip certificates cover widths 2–11.

Read article Code & verification

Source & evidence

https://arxiv.org/abs/2609.25128

2026-09-09 / Preprint / quant-ph

Generalized Fidelity, the Data Processing Inequality, and Convexity

Haobo Ma, Reza Rajaei, Wenlin Zhang

arXiv:2609.09753 / v3 updated 20 October 2026

The generalized Bures–Wasserstein distance induced by generalized fidelity fails the data processing inequality in every dimension n ≥ 2; neither the distance nor its square is convex in one state with the other state and reference fixed. The paper gives three sufficient conditions for data processing in dimension two and an exact criterion for generalized fidelity to reduce to Uhlmann fidelity.

Failure of data processing and convexity in every dimension n ≥ 2

Read article

Source & evidence

Title, authors, first submission date (9 September 2026) and scope checked against the arXiv record and arXiv:2609.09753v3, updated 20 October 2026. The PDF states the dimension-independent failures, three sufficient conditions in dimension two, and a necessary and sufficient condition for equality with Uhlmann fidelity. The revision date is distinct from the first publication date.

2026-09-01 / Preprint / official results pending

A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver

Haobo Ma, Wenlin Zhang, Manuel Israel Cázares

arXiv:2609.00706

A proof-producing cascade for equational implication. Positive answers produce Lean proofs; negative answers produce countermodels checked by the competition judge.

All evaluation question banks correct

Team-reported result, 7 September 2026. Official results have not been announced; this is not an official ranking or independent confirmation of hidden-set performance.

Read article

Source & evidence

The preprint records accepted certificates for all 1,889 rows across six public sets, agreement on 800 published Stage 1 evaluation-distribution problems, 100 accepted canonical Marathon rows, and 200 accepted hosted playground rows. These are separate measurements and are not added together.

2026-09 / Accepted poster / workshop

Cross-Engine Admission Contracts for Autonomous Formalization

Haobo Ma, Wenlin Zhang

6th Workshop on Mathematical Reasoning and AI (MATH-AI), NeurIPS 2026

Accepted for poster presentation at the 6th Workshop on Mathematical Reasoning and AI at NeurIPS 2026. We look forward to presenting in Atlanta on 12 December 2026.

Poster presentation / Atlanta / 12 December 2026

Paper on OpenReview Official acceptance list Workshop details Institute announcement

Source & evidence

The official MATH-AI accepted-papers list links this title to OpenReview xOAZvprLXO. The workshop website confirms Atlanta Hall C3 on 12 December 2026. Authors, poster format and the September announcement are recorded in The Omega Institute organization profile at revision f98733b9eb0f4423d668128a651ac0389bf3d485; the announcement gives no exact day.

2026-08-13 / Published

Canonical Zeckendorf Normalization and sharp iteration depth of the Berstel Adder

Haobo Ma, Wenlin Zhang

RAIRO - Theoretical Informatics and Applications 60, 29

Exact limits on least-significant-digit-first Zeckendorf normalization, maximal prefix erasure, and sharp iteration depth for Berstel recoding. The published article distinguishes the classical ten-state presentation from its six-state output-delay quotient.

From Fibonacci structure to exact computational bounds

Read article

Source & evidence

https://www.rairo-ita.org/articles/ita/abs/2026/01/ita20260032/ita20260032.html

2026-07-05 / Preprint / empirical study

Mechanism-level routing failure in LLMs over Lean-verified algebraic structures

Manuel Israel Cázares, Wenlin Zhang, Haobo Ma

arXiv:2607.04534

An empirical study of how language models select proof mechanisms over Lean-verified algebraic objects. Mechanism-bearing evidence improves routing, while truth prediction and proof-mechanism classification show different failure patterns.

Correct verdicts can still select the wrong proof mechanism

Read article

Source & evidence

The main study uses 22 FiberRing items; a six-item cross-corpus extension provides a small cross-module check. Reported effects describe this experimental corpus.