Letong “Carina” Hong · eight papers · Lean 4

Seven fractions, one moonshine identity, and a seventeen-letter alphabet.

Carina Hong published eight papers between 2020 and 2022, on K3 surfaces, partitions, square-free words, inversion sequences, edge-colorings, Tamari lattices and Euler–Kronecker constants. This is that mathematics written out in Lean 4, where every step is checked by a compiler that does not take anyone's word for anything.

Read the eight results Walk the papers

published papers

pairs with 1/a = 1/b + 1/24

letters before extremal square-free words vanish

Hong–Zhang 2021 · J. Number Theory

Exactly seven fractions do this.

Ask which positive integers a and b satisfy 1/a = 1/b + 1/24. Rewrite it as 24b = a(b + 24) and the question turns finite. Seven pairs answer it: (6, 8), (8, 12), (12, 24), (15, 40), (16, 48), (20, 120) and (21, 168). They are the pairs behind the Ballantine–Merca conjecture on theta functions modulo 2, and the pair (12, 24) is the one survivor of an infinite family that oddness kills everywhere else. The Lean proof is one word, decide, because seven cases is what the problem reduces to once you have done the hard part.

Hong–Zhang 2021 · arXiv:2107.13123

At seventeen letters, extremal square-free words stop existing.

A square-free word never repeats a block back to back: no aa, no abab, nothing that stutters. Over three letters they are famously infinite in number. A word is extremal when it is square-free and every single-letter insertion ruins that. The paper proves extremal square-free words do not exist over any alphabet of 17 letters or more. The counting core is in the source as a closed theorem, (k − 2)(n + 1) · 10 > 147n, and the headline follows from it given a named counting bound of 14.7n. Seventeen is not a rounding. It is where the two sides of that inequality cross.

Hong 2022 · arXiv:2201.10030

Sorting a lattice with a stack that dumps everything at once.

Pop-stack sorting empties the whole stack in one motion instead of popping one element at a time. Run it on the Tamari lattice, count how many elements need exactly t passes, and the generating function is rational. Its denominator is 1 − 2z − Σ C(j−1) z^j, with Catalan numbers in the coefficients. For t = 1 the denominator collapses to 1 − 2z, which the source proves outright: the coefficients are 1 and −2 and nothing else.

Hong–Mertens–Ono–Zhang 2021 · arXiv:2108.01027

An identity that should not be true.

Moonshine is the recurring surprise that modular forms know about objects they have no business knowing about. The Caldararu–He–Huang identity is one of these, an elliptic expansion relating flat coordinates to hypergeometric data. The formalization states it as CHH_Conjecture and derives it from two explicit hypotheses, CHHUpperHalfPlaneBridge and JInversionBridge. Those two are the classical analytic input, held as named assumptions rather than smuggled in. Supplying them is the remaining mathematics.

Hong–Li 2021 · arXiv:2112.15081

Break a counting problem into fibers and it gets easier.

An inversion sequence records, for each position of a permutation, how many earlier entries beat it. Ask how many avoid a given length-four pattern and the count resists direct attack. The reduction proved here splits the avoidance class into fibers indexed by subsets S of the integers 1 through n−1, and the total is the sum over all such S. It is the structural move the paper is built on, and it is the cluster where the open Conjecture 3.18 still lives.

Hong–Miklós 2021 · arXiv:2103.11990

A random walk on the colorings of a bipartite graph.

To sample proper edge-colorings you build a Markov chain that recolors a little and accepts by the Metropolis–Hastings rule. The acceptance ratio looks intimidating until you notice the color-selection probabilities appear on both sides. The factorization theorem here shows they cancel, leaving a clean triple ratio. What is still open is the repair lemma for almost-colorings, the combinatorial heart of Lemma 2.1, and the source says so at the site.

Amir–Hong 2020 · arXiv:2007.09803

Parity survives the symmetric square.

Certain K3 surfaces come in a one-parameter family with seven singular values where complex multiplication appears. Their L-functions are governed by weight-3 newforms. The result proved here is a parity transfer: if the newform coefficients b(p) are even at every prime not dividing 2N, then the symmetric-square coefficients are even at those primes too. The classical inputs from Wiles and Mazur stay visible as named hypotheses.

Hong–Ono–Zhang

One term of a delicate constant, pinned to the right side of zero.

Euler–Kronecker constants generalize the Euler–Mascheroni constant to number fields, and for cyclotomic fields their size is tied to hard questions about primes. The decomposition here splits the constant into named summands. The γ₃ term is proved nonnegative, which is the sign you need before any of the estimates above it mean anything. A single analytic input remains open in the same file.

Formal statements

theorem

Hong.BallantineMerca.bmPairs_harmonic

∀ ab ∈ bmPairs, 24 * ab.2 = ab.1 * (ab.2 + 24). The seven pairs, verified exhaustively.

Hong/BallantineMerca/Conjecture.lean:20

conditional

Hong.SquareFree.no_extremal_squarefree_large_alphabet

For 17 ≤ k, no square-free word over a k-letter alphabet is extremal. Theorem 1.3, given the counting bound Corollary23CountingBridge.

Hong/SquareFree/Main.lean:331

theorem

Hong.PopStack.denom_t1

denominatorCoeff 1 0 = 1 ∧ denominatorCoeff 1 1 = -2. The t = 1 denominator is 1 − 2z.

Hong/PopStack/GeneratingFunction.lean:33

conditional

Hong.Moonshine.caldararu_he_huang_conjecture

CHH_Conjecture, given CHHUpperHalfPlaneBridge and JInversionBridge.

Hong/Moonshine/Main.lean:306

theorem

Hong.PatternAvoidance.reduction_to_S_inv_seq

For π starting at 0 with positive tail, avoidanceClassCard n π is the sum of sAvoidanceClassCard S (patternTail π) over all S ⊆ [1, n−1].

Hong/PatternAvoidance/Reduction.lean:1147

theorem

Hong.MarkovChains.mh_ratio_factorization

The Metropolis–Hastings ratio of the edge-coloring chain factors as a triple ratio. The color-selection probabilities cancel.

Hong/MarkovChains/MetropolisHastings.lean:26

theorem

Hong.LFunctions.k3_parity

If the weight-3 newform coefficients b p are even at every prime p ∤ 2N, the symmetric-square coefficient k3Coefficient b γ p is even there too.

Hong/LFunctions/K3Surfaces.lean:36

theorem

Hong.EulerKronecker.termGamma3_nonneg

0 ≤ termGamma3 q. The γ₃ summand in the Euler–Kronecker decomposition is nonnegative.

Hong/EulerKronecker/Decomposition.lean:61

Amir–Hong 2020 · L-functions of modular elliptic curves and certain K3 surfaces · arXiv:2007.09803 Hong–Zhang 2021 · the Ballantine–Merca conjecture and theta functions mod 2 · J. Number Theory Hong–Miklós 2021 · a Markov chain on edge-colorings of bipartite graphs · arXiv:2103.11990 Hong–Zhang 2021 · no extremal square-free words over large alphabets · arXiv:2107.13123 Hong–Mertens–Ono–Zhang 2021 · an elliptic expansion moonshine conjecture · arXiv:2108.01027 Hong–Li 2021 · length-four pattern avoidance in inversion sequences · arXiv:2112.15081 Hong 2022 · pop-stack-sorting on Tamari lattices · arXiv:2201.10030Hong–Ono–Zhang · Euler–Kronecker constants of cyclotomic fields

Eight papers, one shared foundation.

Lucas sequences, hypergeometric transformations, Tamari bracket vectors, edge colorings and formal power series mod 2 are written once and imported by name. The next page walks each paper into the modules it needs.

Walk the eight papers