Evidence history · claims become narrower as evidence becomes stronger
Evölther search baseline
The first governed campaign established the geometry search and replay path.
High-quality floating reconstruction
A contact-rich layout reached the final score neighborhood, but not strict feasibility.
Mathematical artifact v1.2.0
Three named contracts and the rational interval proof established the result.
Current release v1.2.1
The editorial and citation release preserves the certified mathematics unchanged.
Abstract
We study the placement of 26 independently sized circles in the unit square while maximizing their total radius. The headline is not one naked score: Evölther 2.0 publishes three independently replayable certificates for three non-interchangeable feasibility contracts—τ=10-6, 10-10, and 0. Each ranks first among the complete public witnesses in the manifested corpus that are valid under the same exact-rational contract.
For the strict problem, the finite-decimal witness has total radius
An exact rational interval certificate additionally proves that the nearby real 78-contact configuration is a strict local maximizer. This is a tolerance-aware reproducibility result and a local theorem—not a proof of global optimality or a new Packomania record.
1. One geometry, three numerical problems
For centers (xi,yi) and radii ri>0, maximize
subject to four wall constraints per circle and one non-overlap constraint per pair. The model therefore contains 78 continuous variables and 429 geometric inequalities: 104 wall decisions and 325 pair decisions. Including radius positivity, every certificate makes 455 exact decisions.
A tolerance τ changes the feasible set. Wall gaps may be as low as -τ, while a pair must satisfy
whenever ri+rj-τ>0. Consequently, a larger score at 10-6 cannot be presented as an improvement over a strict τ=0 witness. It solves a different numerical contract.
| Contract | Evölther 2.0 score | Zero-tolerance recheck | Manifested-corpus rank |
|---|---|---|---|
| τ = 10⁻⁶ | 2.63599872089287514 | fails | #1 among valid complete witnesses |
| τ = 10⁻¹⁰ | 2.63598308647338795 | fails | #1 among valid complete witnesses |
| τ = 0 | 2.635983084917607783… | passes | #1 among strict complete witnesses |
The relaxed certificates consume their declared tolerance and fail when rechecked at zero. The strict CSV was formed by rounding a high-precision contact root to 90 decimal places and reducing every radius by approximately 10-75. That tiny inward movement turns the serialized decimal geometry into an exact feasible rational lower bound.
The three drawings appear almost identical because their differences are smaller than the plotted line width. The contract and verifier—not the image—determine which result is valid.
2. Where each result stands
We authenticated nine upstream artifacts and evaluated ten complete public witnesses in a corpus frozen on 8 August 2026. Every numeric token was retained as a decimal string and reevaluated as a rational number under all three contracts. Downloaded programs and notebooks were parsed as data rather than executed; mutable sources were hash-pinned and fail closed if their contents drift.
τ = 0
| Pos. | Witness | Score |
|---|---|---|
| 1 | Göther Labs | 2.63598308491760778… |
| 2 | Jason Liang | 2.635983084893 |
| 3 | Theta 8B-RL Formal | 2.63598307738811934 |
| 4 | ShinkaEvolve | 2.63598282664580639 |
| 5 | Theta AlphaEvolve | 2.63586275641369812 |
τ = 10⁻¹⁰
| Pos. | Witness | Score |
|---|---|---|
| 1 | Göther Labs | 2.63598308647338795 |
| 2 | Packomania | 2.635983084919 |
| 3 | AlphaEvolve v2 | 2.6359830849176068 |
| 4 | Station | 2.63598308491754725 |
| 5 | Jason Liang | 2.635983084893 |
τ = 10⁻⁶
| Pos. | Witness | Score |
|---|---|---|
| 1 | Göther Labs | 2.63599872089287514 |
| 2 | Theta 8B-RL | 2.63598566124089912 |
| 3 | Hyra | 2.63598309510684482 |
| 4 | Packomania | 2.635983084919 |
| 5 | AlphaEvolve v2 | 2.6359830849176068 |
Evölther 2.0 is the highest-scoring valid witness in the explicit manifested corpus for each matching contract. At τ=10-6, 2.63599872089287514 ranks above the other complete witnesses admitted by that relaxed contract. At τ=10-10, 2.63598308647338795 ranks first in the stricter relaxed panel. At τ=0, 2.635983084917607783… ranks first among the strict exact-rational witnesses acquired in the audit.
This is the reproducible meaning of “best” on this page: best exact-rationally reevaluated witness in the manifested public corpus under the same tolerance. It is not an exhaustive world ranking. Reported values without a complete downloadable witness—such as Numaro and HELIX at the snapshot date—remain outside the computed ranking.
3. How the exact score is computed
Each CSV row contains xi, yi, and ri as finite decimal strings. Python's Decimal parser and Fraction convert them into exact rationals. The score is then the rational sum of the 26 radii; no binary floating-point value participates in acceptance.
For each circle the verifier computes xi-ri, 1-xi-ri, yi-ri, and 1-yi-ri. For every pair it computes the squared distance and compares it with the squared tolerance-adjusted radius sum. This is the core of the published verifier:
1def rational(value: str) -> Fraction:2 return Fraction(Decimal(value))3 4def verify_circles(circles, tolerance=Fraction(0)):5 wall_gaps = []6 for x, y, radius in circles:7 wall_gaps += [x-radius, 1-x-radius, y-radius, 1-y-radius]8 9 pair_pass = True10 for i, (xi, yi, ri) in enumerate(circles):11 for xj, yj, rj in circles[i + 1:]:12 dist2 = (xi-xj)**2 + (yi-yj)**213 required = ri + rj - tolerance14 if required > 0 and dist2 < required**2:15 pair_pass = False16 17 valid = min(wall_gaps) >= -tolerance and pair_pass18 score = sum((radius for _, _, radius in circles), Fraction())19 return {"valid": valid, "score": decimal_string(score)}
The strict certificate passes 455/455 decisions. Its smallest zero-tolerance wall gap is approximately 1.0×10-75, and its smallest squared pair gap is approximately 6.46×10-76. Square roots are used only for readable diagnostics, never for pass/fail.
| Quantity | Certified value |
|---|---|
| Exact total radius | 2.635983084917607783186569485443481730396676798274… |
| Wall / pair / positivity decisions | 104 / 325 / 26 — all pass |
| Minimum wall gap | +1.0000000000000015957 × 10⁻⁷⁵ |
| Minimum squared pair gap | +6.4628891171277475 × 10⁻⁷⁶ |
| Decision arithmetic | exact rationals |
4. From a feasible CSV to a local theorem
Exact feasibility proves that one serialized witness is valid. The stronger mathematical result concerns the nearby real contact root. The strict witness identifies 78 active constraints—58 circle-circle contacts and 20 wall contacts—which match the 78 variables.
Let g:ℝ78→ℝ78 collect those active polynomial gaps. The certificate proceeds in four auditable steps:
Step 1 — isolate the root. A rational Krawczyk operator proves that a box of radius 10-90 contains exactly one root x* of g(x)=0. Its maximum inclusion ratio and contraction bound are both below 8.552×10-15.
Step 2 — preserve feasibility. Every one of the 351 inactive geometric constraints remains strictly feasible throughout that box; the smallest certified inactive polynomial gap is greater than 0.0071877548.
Step 3 — certify stationarity. A second rational Krawczyk calculation encloses the KKT multipliers. All 78 multipliers are positive, with the smallest greater than 0.0208256021.
Step 4 — conclude locally. Because the active gradients form a basis, the active gaps are local coordinates. With positive multipliers, every nonzero feasible nearby gap direction strictly decreases the total radius. Therefore x* is a strict local maximum.
| Certificate stage | Verified bound | Consequence |
|---|---|---|
| Primal Krawczyk | inclusion ratio < 8.552 × 10⁻¹⁵ | one unique regular root |
| Inactive constraints | minimum gap > 0.0071877548 | all 351 remain strict |
| Dual Krawczyk | minimum multiplier > 0.0208256021 | all 78 multipliers positive |
| Local coordinate argument | full-rank active gradients | strict local maximum |
The real root is enclosed between 2.6359830849176077831865694854434817303966767982744 and 2.6359830849176077831865694854434817303966767982745 in total radius. It lies slightly above the deliberately shrunken CSV witness; the two objects should not be conflated.
5. What changed from the earlier result
The historical Evölther reconstruction printed 2.6359830849768984 under binary64 arithmetic, but its minimum numerical slack was negative. It remains valuable as a search checkpoint, not as a strict certificate. Evölther 2.0 separates search from publication: first propose a high-quality contact geometry, then publish independent witnesses for named contracts and prove what can actually be established.
The advance is therefore not merely a few more decimals. It is the transition from an attractive numerical output to a claim with explicit scope: three contract-specific corpus leaders, an exact strict witness, and a computer-assisted proof of strict local optimality for the nearby contact root.
6. Reproducibility and limits
The public artifact includes the three CSV certificates, exact-rational verifier, hash-authenticated source manifest, generated audit tables, contact system, interval certificate, and deterministic publication build. Version 1.2.1 passes 39/39 tests and the four-document publication gate. The verification path uses only the Python standard library.
cd results/circle-packing-26-unit-square/artifacts
python3 verifier.py
python3 -S prove_local_optimum.py
The audit is frozen to its manifested corpus and snapshot. It does not certify that no stronger unpublished or unacquired witness exists. The interval argument proves a strict local maximum for one 78-contact root, not global optimality over every 26-circle topology.
Read the technical repository, the v1.2.1 release, or the archived artifact at Zenodo.