Tencent-Hunyuan/Hyra-results

TL;DR: Tencent released the outputs of Hyra, its Hunyuan Research Agent: a folder-per-result repo of claimed improvements on real open problems in mathematics (sharper constants for the Beurling–Ahlfors transform, the 3D Blaschke–Lebesgue problem, Tao's commutator construction, a claimed full resolution of the sum-vs-difference exponent), plus wins on AI-research-automation benchmarks and 100 packing records. What makes this worth your time is that some results are claimed to be machine-checked in Lean 4 and others sit on independently maintained leaderboards — this is one of the few agent-discovery releases that is actually falsifiable. The agent itself is not released.

What this repo actually is

This is an artifacts repository, not a system. Each folder holds a final solution (a construction, a certified bound, a paper) and "where relevant" self-contained reproduction scripts. There is no agent code, no weights, no methodology description, and no paper about how Hyra works — for that you get a pointer to a launch post. So you can audit the claims, but not the process: how much human problem selection, scaffolding, or curation happened between the agent and this repo is invisible.

Three verification paths exist, of different strength:

The headline results

The mathematics is the interesting part. Four items stand out:

• Sum-vs-difference exponent settled (claimed): for finite A ⊆ ℤ, the supremum of log(|A+A|/|A|)/log(|A−A|/|A|) is exactly 2, approached but never attained, with a "complete, machine-checked resolution." If the Lean proof genuinely covers the full statement (not just a construction), this closes a known open question.
• 3D Blaschke–Lebesgue: certified lower bound on Vol(K)/w³ raised from 0.380799 (Nishioka, 2026) to >0.411040 — closing 77.4% of the gap to Meissner's conjectured 0.419860.
• Beurling–Ahlfors: uniform coefficient toward Iwaniec's 1982 conjecture drops from 1.575 (Bañuelos–Janakiraman, 2008 — a bound that stood 18 years) to 1.523958.
• Commutators near the identity: Tao's O(log⁵(1/ε)) construction, refined to log⁴, is now claimed at log³ (Popa's lower bound is log).

There are also 100 shape-packing records now listed on Erich Friedman's independently maintained Packing Center — genuinely external validation, though notably credited there as "Found by Haowei Lin," a human name, which tells you there's a human submission loop and leaves the division of labor unclear.

The weaker rows

The AI4AI results are marginal: nanogpt speedrun 77.5s → 76.4s, nanochat BPB 0.9109 → 0.9015, SOL-ExecBench 0.754 → 0.771. These show the agent can compete on ML-engineering leaderboards but are not the story. The sunspot forecasting R² of 0.78 looks impressive until you read the footnote: the 0.47 baseline is persistence (copy the last frame), which is a strawman for a quasi-periodic signal. Several "prev best" entries are other 2026 agent systems (TTT-Discover, SimpleTES), so those rows are agent-vs-agent leaderboard deltas, not advances over the human literature.

What to scrutinize

The Lean 4 claim is carefully scoped: the three newest results have formalizations of their "finite and numerical core." That likely means the certificate/computation is kernel-checked while the surrounding analytic argument (the Bellman-function machinery, the asymptotic counting) is an informal paper. That's still valuable — numerical cores are where errors usually hide in these bound-improvement papers — but "machine-checked result" would be an overstatement for three of the four math items. Verify the Lean statements match the claimed theorems, not weakened versions. Also note the repo's own warning that public leaderboards may already exceed these numbers by warm-starting from Hyra's solutions.

Trying it

No install; it's a browsable artifact archive under Apache 2.0. The math papers and Lean projects are the things to open:

git clone https://github.com/Tencent-Hunyuan/Hyra-results
cd Hyra-results
ls AI4Science/3d_blaschke_lebesgue/      # certified bound + paper
ls AI4Science/beurling_ahlfors_bellman/  # Lean core, per README
# Lean projects should build with `lake build` if standard, but the
# README gives no build instructions — expect to poke around.

Launch post with (presumably) methodology: https://hy.tencent.com/research/hyra. If the sum-vs-difference Lean proof checks out end-to-end, that alone would make this the strongest verified claim yet for an autonomous agent resolving an open math problem — worth the hour to audit.