THE OMEGA INSTITUTE

Research

Mathematical discoveries, formal proofs, and the questions that come next.

FROM QUESTION TO RESULT

Resolved questions

Where this leads next

2026-09-06Refuted in Lean

Real-rooted polynomials

Pochhammer Conjecture 6.5: a quadratic counterexample range

An exact degree-two classification yields a counterexample range to the conjectured strict upper bound.

Read result Lean theorem Original question Question record

Exact scope & proof record

For a > 0, c2(a) = (sqrt(a^2+a) - a)/2 satisfies c2(a) < 2a exactly when a > 1/24. Thus 0 < a <= 1/24 refutes the k = 1 strict upper bound. This does not settle the higher-degree classification.

Upstream Frozen / not in current Truth release

D5/S3/Zeros/PochhammerDeformation/QuadraticInterval.quadratic_conjecture_refutation

Development PR #5859 Read in mdBook

Frozen module record sha256:adf16034b6b75357f9feaee180f1e570626f00f86a3eb3125487a55155a65486

Evidence snapshot: b9afa2151caf868e9018c02df14489bc7e409da8. The linked mdBook follows upstream development.

2026-09-06Proved in Lean

Integer sequences

Chamberland-Dilcher Conjecture 2.1: consecutive zero blocks

An explicit construction locates consecutive zero blocks in an alternating sum of floor square roots.

Read result Lean theorem Original question Question record

Exact scope & proof record

The formal result proves the stated zero blocks and their disjointness for eligible labels and odd positive n, with an explicit bridge to the natural square-root floor. Source: section 2, equation 2.3 and Conjecture 2.1.

Upstream Frozen / not in current Truth release

D5/S1/Digit/AlternatingFloorSqrtZeroBlocks.conjecture21

Development PR #5914 Read in mdBook

Frozen module record sha256:cace4bac173c51d8c4fc5d46b5931c06670548e15fceacfc58c0db99e98f9016

Evidence snapshot: b9afa2151caf868e9018c02df14489bc7e409da8. The linked mdBook follows upstream development.

2026-09-06Proved in Lean

Combinatorics / integer sequences

Bosma et al. Conjecture 17: the greedy three-sumfree sequence

A universal periodic formula characterizes the literal greedy sequence starting from 1, g and g+d.

Read result Lean theorem Original question Question record

Exact scope & proof record

Proved for all natural parameters 2 <= d and d+1 <= g, including all four exceptions and inclusive residue bounds in the published statement. This is Conjecture 17, not the different g+1 third-seed problem in Conjecture 16.

Upstream Frozen / not in current Truth release

D5/S1/Words/Sumfree/GreedyThreeSumfreeTwoParameter.conjecture17

Development PR #5862 Read in mdBook

Frozen module record sha256:b747816e9a11f6361787befcf7759518443240b42e431c5b3b9dbc58252007bb

Evidence snapshot: b9afa2151caf868e9018c02df14489bc7e409da8. The linked mdBook follows upstream development.

2026-09-06Proved in Lean

Combinatorics on words

Thue-Morse reduced abelian complexity: the odd-length recurrence

The number of reduced abelian classes at length 2n+1 equals the count at length n+1, for every nonnegative n.

Read result Lean theorem Original question Question record

Exact scope & proof record

Proves R(2n+1) = R(n+1) for all natural n, the proposed odd recurrence in Campbell-Currie-Rampersad, arXiv:2509.16034v1, section 3. Factors range over every natural starting position. Maximal constant runs are compressed and the resulting character counts define equivalence classes, matching the paper's reduced abelian complexity. This does not settle the full recursion, the even-index recurrence, equation (11), the sign of the even-index difference, or non-k-automaticity. R(2^k+1) = 3 is a supporting corollary, not another resolved open problem.

Upstream Frozen / not in current Truth release

D5/S1/Words/Complexity/ThueMorseReducedAbelianOdd.reducedAbelianComplexity_odd

Development PR #5816 Read in mdBook

Frozen module record sha256:31fb069a0187ae500aa0a39e052a8deaceee7eb0f963bcc75879f9f575b26ff1

Evidence snapshot: b9afa2151caf868e9018c02df14489bc7e409da8. The linked mdBook follows upstream development.

PAPERS & PREPRINTS

Publications

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.

RAIROTheoretical Informatics
and Applications60 / 2026 / 2910.1051/ita/2026032

2026-08-13 / Published / journal article

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

Publication title, authors, date and scope verified against the publisher's Crossref record for DOI 10.1051/ita/2026032.

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.

The next questions

Explore the conjectures and proof targets growing from these results.

Conjectures Further reading in mdBook