Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean
Every choice of five positive masses gives finitely many planar central configurations, up to similarity.
Papers
Selected papers
The rank of 3×3 matrix multiplication over F2 is 23
No bilinear algorithm for 3×3 matrix multiplication, whether over F2 or with integer coefficients, uses fewer multiplications than Laderman’s.
Operon Finder: A Deep Learning-based Web Server for Accurate Prediction of Prokaryotic Operons
A web server that uses a deep-learning model to predict operons in prokaryotic genomes.
Sorting networks on 13 inputs need 45 comparators
Every sorting network on 13 inputs has at least 45 comparators, so Juillé’s 45-comparator network is optimal and S(13) = 45. The known lower bounds for 14 ≤ N ≤ 32 each rise by one.
A matching threshold of 2×10−3 for the rotated surface code under circuit-level noise
For the rotated surface code under depolarizing noise with p ≤ 2×10⁻³, the logical error rate of matching with log-likelihood weights decays exponentially in the distance. In this noise model, every gate, idle step, preparation and measurement in the standard circuit fails independently with probability p.
Area law for three-dimensional U(1) lattice gauge theory with the Wilson action at every coupling
Three-dimensional U(1) lattice gauge theory with the Wilson action confines static charges at every coupling.
Uniqueness of four-body convex central configurations for all masses
For any four positive masses and any cyclic ordering of the bodies, there is exactly one strictly convex central configuration with that ordering, up to similarity.
More papers
Smale's sixth problem for six bodies in the plane: finiteness of central configurations for generic masses, with a proof formalized in Lean
For generic masses (those outside a proper algebraic subset of the mass space), six bodies in the plane have finitely many central configurations.
The number of planar central configurations of four bodies
For all masses outside a closed null set, the number of four-body central configurations is even and lies between 32 and 50.
The Steiner ratio is at least 0.8564
The Steiner ratio of the Euclidean plane is at least 2141/2500 = 0.8564, up from the bound 0.8559 of Ke, Huang, Shu, He, Gai and Wang. The proof follows their computer-assisted method. The paper gives complete proofs of the geometric lemmas it needs, adds two new lemmas and uses a certificate of 555,102,905 boxes. For any bound of at least 0.856, a complete certificate of this form needs lemmas beyond those of Ke et al. In particular, this applies to the conditional value 0.860 listed in Tao’s repository of optimization constants.
The automorphism group of an extremal [72,36,16] code has order at most 2
A doubly-even self-dual [72,36,16] code has no automorphism of order 3 or 5 and no subgroup of automorphisms isomorphic to C₂ × C₂, so its automorphism group is trivial or has order 2. The case of order 3 uses a classification of the Hermitian self-dual [24,12,8] codes over F₄, of which there are 26,924,931 up to monomial equivalence.
Undistillability of Werner states from three, four and five copies
For every local dimension d ≥ 3, the Werner state ρ(d, α) is three-copy distillable exactly when α < −1/2, the same threshold as for one copy. It is four-copy undistillable for every α ≥ −79/160 in every dimension, and for every α ≥ −0.4979 when d = 3. The qutrit Werner state is five-copy undistillable for every α ≥ −0.47.
A lower bound of 0.6508 for the Beardwood–Halton–Hammersley constant
The Beardwood–Halton–Hammersley constant β is at least 0.6508, improving the lower bound 0.6421 proved by Dong and Cao.
Tied group sizes make GroupKFold folds depend on the scikit-learn version and the CPU
Up to scikit-learn 1.8, GroupKFold ordered groups of equal size with numpy's default argsort, so its folds could depend on the numpy version and the CPU; version 1.9 sorts stably, which changes the folds when group sizes tie. In a sample of public code, 92.8% of the uses of GroupKFold apply it, without shuffling, to groups whose sizes can tie.
A lower bound of 0.8366 for Lebesgue's universal covering problem
Every universal cover in Lebesgue’s problem has area at least 0.8366, which beats the earlier bounds of Hatchett (0.83474) and Mishra (0.8344). The best known cover, by Gibbs, has area at most 0.8440935944.
A thrackle on n vertices has fewer than 4n/3 edges
Every thrackleable graph with n ≥ 4 vertices has at most 4(n − 1)/3 edges. This improves the bound of 18(n − 1)/13 proved independently by Tóth and by Scoppetto, and comes closer to Conway’s conjectured bound of n. The key steps are computer searches showing that the dumbbells DB(6, 8, −1) and DB(6, 10, −3) are not thrackleable. These searches perform about 2.1·10¹¹ and 8.3·10¹⁰ planarity tests, respectively.
Essential enhancements of site percolation in every dimension and on periodic lattices
Every essential enhancement strictly lowers the critical probability of site percolation on the hypercubic lattice in every dimension d ≥ 2 and on ten further periodic lattices, among them the honeycomb, Kagomé and face-centred cubic lattices. The same holds for bond percolation on the honeycomb lattice. After finding that a combinatorial lemma in Aizenman and Grimmett’s 1991 argument was false, Balister, Bollobás and Riordan proved the cases d = 2 and 3 and outlined a proof for the triangular lattice.
Certified upper bounds for the Chvátal–Sankoff constant
The Chvátal–Sankoff constant for two random binary strings is at most 0.821963, improving the bound 0.824120 posted by L. Jack in October 2026.
The L¹ Poincaré constant of the Hamming cube
For real-valued functions, the L¹ Poincaré constant of the Hamming cube equals √(π/2), the lower bound given by the Gaussian case.
The PPT2 conjecture holds for spin-factor maps
The PPT² conjecture holds for compositions of spin-factor maps on M₄, whatever the intermediate dimension.
Which Fine-Grained Lower Bounds Survive the Refutation of 3SUM and APSP?
After the refutation of the 3SUM and APSP hypotheses in October 2026, the paper classifies the main conditional lower bounds derived from them, recording which hypotheses imply each surviving bound and which bounds are false or have lost their support. It proves that, when queries are known in advance, the algorithms behind the refutation solve the natural lopsided instances in truly subquadratic time for every middle-part exponent below 0.17843, whereas Majdoddin's analysis stops at 0.17227. It also gives a data structure for 3SUM-Indexing with truly subquadratic preprocessing time and truly sublinear expected query time.
Subplanes of order 3 and maximal arcs in projective planes of order 12
If a projective plane of order 12 had a subplane of order 3, the 27 points lying on no line of the subplane would form a maximal arc of degree 3, and the plane would yield partial geometries pg(8, 9, 6) and pg(9, 8, 6), whose existence is open. No plane of order 12 has a maximal arc of degree 3 whose design is AG(3, 3).
The 24-cell conjecture in the all-contact case and near D4
In a packing of unit balls in R⁴, if a ball touches all other balls whose centres lie at distance less than 2√2 from its own, its Voronoi cell has volume at least 8, that of the regular 24-cell. If instead 24 other centres have directions within root-sum-square distance 2/5 of a rotated D₄ root system and lie at distances 2 + δᵢ from the ball's centre with Σδᵢ ≤ 3/100, the volume is at least 8 + 0.2437 · ½Σδᵢ, regardless of the remaining centres. In both cases equality holds only for the D₄ root configuration.
Sorting networks on 13 inputs need at least 44 comparators
The bound S(13) ≥ 44 holds, as do the other nineteen lower bounds in Dobbelaere’s table for 14 ≤ N ≤ 32. The argument computes how many comparators the two largest values must meet, replacing a 1972 inequality whose proof was invalid.
Formal Verification of a Computer-Assisted Proof in Celestial Mechanics
The Lean 4 and Mathlib formalization of the convex four-body uniqueness theorem. Without compiled code, Lean’s kernel checks the interval computation (3,418 certificate theorems) through decide +kernel in 7.6 processor-hours; the independent checker nanoda accepts the proof.
A Lean 4 formalization of the area law for three-dimensional U(1) lattice gauge theory with the Wilson action
The 221,290-line Lean 4 and Mathlib formalization of the U(1) area law at every coupling, its corollaries, Fröhlich’s comparison and Appendix E. Every formal theorem has no hypotheses and is checked by the kernel alone.
A formal proof in Lean of the finiteness of planar central configurations of five bodies
The Lean 4 and Mathlib formalization of the five-body theorem, checked by Lean’s kernel and by two independent ones.
Homological percolation in characteristic two: the Ising gauge case
Duncan and Schweinhart’s sharp homological percolation threshold holds for the plaquette random-cluster model with F₂ coefficients and q = 2, 4, 8, …, covering part of the characteristic-two case that their proof excluded. Consequently, every ’t Hooft twist free energy of the four-dimensional Ising gauge theory tends to 0 below Wegner’s self-dual coupling and to infinity above it.
Certified lower bounds for the first and the signed third autocorrelation constants
The first autocorrelation constant C₁ is at least 1.337, improving the previous best lower bound of 1.2937. The signed third autocorrelation constant C₃ and its one-sided version C₃′ satisfy C₃ ≥ C₃′ ≥ 4/3, improving the trivial bound of 1.
Certified upper bounds for two sum-difference exponents
The Kakeya-type sum-difference exponent is at most 1.8272963, down from Katz and Tao’s 11/6. The upper bound on Gyarmati, Hennecart and Ruzsa’s sum-difference constant falls from Kleinwaks’ 1.3124 to 1.2961919.
An explicit bound below 2/π for the maximum term of an entire function
For every transcendental entire function, the ratio of the maximum term to the maximum modulus has lower limit at most 0.63005, an explicit bound below Clunie’s 2/π ≈ 0.6366.
Upper and lower bounds for the Schur–Siegel–Smyth trace problem
The Schur–Siegel–Smyth trace constant satisfies 1.8022225 < C₈₆ < 1.8070809, improving Pinho’s upper bound 1.8117251 and the lower bound 1.80220 that Giraudin reported from floating-point checks.
New lower bounds for Romanoff's constant
The integers p + 2ᵃ with p prime and a ≥ 1 have lower density at least 0.110825, improving the previous bound of 0.10788. Assuming a bound that Johnston and Trudgian deduce from Lichtman’s Theorems 1.2 and 1.7, the lower density is at least 0.119178.
An upper bound for the connective constant of the square lattice
The connective constant of self-avoiding walks on the square lattice is at most 2.6586513, improving the upper bound 2.662342426 proved by Couronné. The new bound comes from a finite automaton with integer weights and 24,887,440,008 states.
A lower bound for Moser's worm problem with rotations and translations
For Moser’s worm problem with rotations and translations but no reflections, every convex set that contains a copy of each arc of length 1 has area at least 0.2414. This improves the lower bound 0.239, which follows from Keller’s preprint on the version with reflections. The new bound comes from five polygonal arcs and a branch-and-bound search over their placements; its certificate, with 433,912,890 leaves, is checked in ball arithmetic.
A certified upper bound for the beat the average game
For independent nonnegative X₁, …, X₄ with a common distribution, P[X₁ + X₂ + X₃ < 2X₄] ≤ 0.40069634, improving the earlier upper bound 673/1615 ≈ 0.41672. The new bound comes from samples of nine points and exceeds the conjectured supremum 0.4006953… by less than 9.7 × 10⁻⁷.
An upper bound of 2√2 for the three-dimensional sofa problem in a snake-shaped corridor
If the straight section between the two turns of a snake-shaped corridor of unit-square cross-section is longer than 2 + √2, every connected body that can pass through the corridor has volume at most 2√2.
A lower bound for the essential minimum of the Zhang–Zagier height
The essential minimum of the Zhang–Zagier height h(α) + h(1 − α) is at least 0.24982933, improving Flammang’s lower bound of 0.24874.
Bounds for the weak type (1,1) constant of the centred maximal operator over squares
The weak type (1,1) constant of the centred Hardy–Littlewood maximal operator over axis-parallel squares in the plane is at most 3.59123, improving Lin’s bound of 3.615749. Its lower bound rises from Lin’s 1.6855 to 1.7027237335.
A lower bound for the smallest limit point of the absolute Mahler measure of totally positive algebraic integers
All but finitely many totally positive algebraic numbers have absolute Mahler measure greater than 1.7234615, improving Flammang’s bound of 1.722069.
An upper bound for the smallest limit point of the absolute Mahler measure of totally positive algebraic integers
The smallest limit point of the absolute Mahler measure of totally positive algebraic integers is at most 1.7239501, improving the bound 1.72731… from Smyth’s work.
Bounds for the smallest limit point of the areal Mahler measure of totally positive algebraic integers
For totally positive algebraic integers, the smallest limit point of Pritsker’s areal Mahler measure, taken per degree, lies between 1.3830134 and 1.3839579. The lower end beats the bound of 1.380047 that follows from Flammang’s 2015 theorem.
A lower bound for the Bohr radius of the bidisc
The Bohr radius K₂ of the bidisc exceeds 0.301665. The paper confirms Patel’s unrefereed proof of K₂ > 0.30158758 and improves on it with certified bounds on Sidon constants: S({0, 1, …, 5}) ≤ 2.187, S({0, 1, …, 6}) ≤ 2.363 and S({0, 1, …, 7}) ≤ 2.552.
Bounds for the sign uncertainty constant in dimension one
The one-dimensional sign uncertainty constant satisfies 0.30272004 < A₊(1)² ≤ 0.30349081, tightening the earlier bounds 0.2025 and 0.3089.
Complex solution sets of the planar five-body problem at special masses
Explicit complex solution sets at three special mass vectors, one of which has a continuum of complex solutions. At these masses, finiteness of the real central configurations follows without counting them.
A resource-efficient deep learning framework for pest and disease detection in plants
A lightweight MobileNetV2-based model that identifies plant pests and diseases and is optimized to run on Android.