- Chain Bounding
Pedro Sánchez Terraf
Palomar RegistrySep 17, 2026math.LOmachine-checkedscore 0
- ns-lean: Naslund's Conjecture 13 is false at q = 3, k = 2, for every n congruent to 0 mod 4 with n >= 8
JD Jones
Palomar RegistrySep 17, 2026math.NTmachine-checkedscore 0
- A formalization of Chang, Liu, and Liu's proof of Chvátal's conjecture
Boon Suan Ho
Palomar RegistrySep 17, 2026math.COmachine-checkedscore 0
- Sectorial asymptotics for centered Riemann-xi coefficients
John Savva
Palomar RegistrySep 17, 2026math.NTmachine-checkedscore 0
- Resonance-cluster analysis for a proposed counterexample to Fried's conjecture
Benjamin Lawton
Palomar RegistrySep 17, 2026math.DSmachine-checkedscore 0
- The exponential map is chaotic
Lasse Rempe
Palomar RegistrySep 16, 2026math.DSmachine-checkedscore 0
- BSCAveraging
Georg Pichler
Palomar RegistrySep 15, 2026cs.ITmachine-checkedscore 0
- Boundary regularity for non-local operators with symmetric kernels and vanishing horizon
Philipp Svinger
Palomar RegistrySep 15, 2026math.APmachine-checkedscore 0
- Integral Matrices of Fixed Rank over Number Fields: Lean formalization
Nihar Gargava
Palomar RegistrySep 15, 2026math.NTmachine-checkedscore 0
- Erdős Problem 190: every canonical N exceeds (Ck)^k for large k, and H(k)^{1/k}/k → ∞ under the existence hypothesis — a Lean 4 formalization of the qualitative statement of arXiv:2604.20588
Ji Ho Bae
Palomar RegistrySep 15, 2026math.COmachine-checkedscore 0
- B. C. Carlson's approach to special functions of applied mathematics
Bastiaan J Braams
Palomar RegistrySep 15, 2026math.CAmachine-checkedscore 0
- Constructive families and an extension theorem for binary permutation X-rays
JD Jones
Palomar RegistrySep 15, 2026math.COmachine-checkedscore 0
- CoarseGraining
Scott Armstrong, Tuomo Kuusi
Palomar RegistrySep 15, 2026math.APmachine-checkedscore 0
- MarkovProcess
Scott Armstrong
Palomar RegistrySep 15, 2026math.PRmachine-checkedscore 0
- Formalization of norm-variation of multiple ergodic averages for commuting transformations
Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, Christoph Thiele
Palomar RegistrySep 15, 2026math.CAmachine-checkedscore 0
- A Tight Upper Bound for Fully Dynamic Matching on the Line
Yash Kanoria
Palomar RegistrySep 14, 2026math.OCmachine-checkedscore 0
- md-lean: exact height span, dart mass, and adjugate scaling for Mazur's greedy construction
JD Jones
Palomar RegistrySep 14, 2026math.COmachine-checkedscore 0
- A Surjunctive Group That Is Not Sofic
Sauers
Palomar RegistrySep 14, 2026math.GRmachine-checkedscore 0
- A proof of Nivat's conjecture
Boon Suan Ho
Palomar RegistrySep 14, 2026math.DSmachine-checkedscore 0
- To cover a permutohedron
Bochao Kong
Palomar RegistrySep 14, 2026math.COmachine-checkedscore 0
- Gallai’s Path Decomposition Conjecture for Graphs with Small Bowtie Boundaries
Idris Ali Shaik
Palomar RegistrySep 14, 2026math.COmachine-checkedscore 0
- MI-32: Lean formalization of the parity and positive-polynomial upper bound
Diar Heidary
Palomar RegistrySep 14, 2026math.PRmachine-checkedscore 0
- Robin1984
Jonas Whidden
Palomar RegistrySep 14, 2026math.NTmachine-checkedscore 0
- A Counterexample to the Trace Problem for Uniform Tracial Completions
Sauers
Palomar RegistrySep 14, 2026math.OAmachine-checkedscore 0
- Certified naturality and the obstruction to unrestricted naturality in a typed two-dimensional calculus
Arthur F. Ramos
Palomar RegistrySep 14, 2026math.LOmachine-checkedscore 0
- Explicit Fourier–Jacobi Haar-core evaluation and Abel limits
Abhishek Saha
Palomar RegistrySep 14, 2026math.NTmachine-checkedscore 0
- Rational invariants of three frames in the split Albert algebra: a Lean formalization
Robert R. MacGregor
Palomar RegistrySep 13, 2026math.RAmachine-checkedscore 0
- An Infinite Simple Group with Property (T) That Is Sofic and Hyperlinear
Sauers
Palomar RegistrySep 13, 2026math.GRmachine-checkedscore 0
- Lean proofs of Dimitrov's Conjectures 1 and 3
Michael Mazur
Palomar RegistrySep 13, 2026math.NTmachine-checkedscore 0
- The Broughton--Huff theorem on increasing unions of sigma-fields
Yi-Jing Tseng
Palomar RegistrySep 12, 2026math.PRmachine-checkedscore 0
- Confinement schemas and the reach of block certificates for powers of rational numbers modulo one
Ralf Stephan
Palomar RegistrySep 12, 2026math.NTmachine-checkedscore 0
- rk-lean: the directed construction for k-th-power-difference-free sets at every k, with the exponents 0.912145 (k = 4) and 0.950826 (k = 6)
JD Jones
Palomar RegistrySep 12, 2026math.NTmachine-checkedscore 0
- Independent Bonnet--Myers diameter and compactness theorem
Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
Palomar RegistrySep 11, 2026math.DGmachine-checkedscore 0
- The Kolmogorov-Arnold representation theorem
George A. Constantinides
Palomar RegistrySep 11, 2026math.CAmachine-checkedscore 0
- ry-lean: sets avoiding {x, x+y, x+y²} — Younis's two-set construction and the exponent 0.77028
JD Jones
Palomar RegistrySep 11, 2026math.NTmachine-checkedscore 0
- All-ones polynomials over GF(2) under the substitution X ↦ X² + X + 1 (OEIS A071642, TheoremDB P12771)
Brandon Yates
Palomar RegistrySep 11, 2026math.NTmachine-checkedscore 0
- Three Sharp Bounds for Hansen Polytopes of Cographs
Jeremy P Parker
Palomar RegistrySep 10, 2026math.MGmachine-checkedscore 0
- Short-Cycle Decompositions and Full Zombie Damage in Cubic Graphs
Lennart Rudolph
Palomar RegistrySep 10, 2026math.COmachine-checkedscore 0
- KR-mod9-lean
Yuma Mizuno
Palomar RegistrySep 10, 2026math.NTmachine-checkedscore 0
- Irreducible improper phi-regret in Lean
Arthur Freitas Ramos
Palomar RegistrySep 10, 2026cs.GTmachine-checkedscore 0
- Density-one prescribed-rank spectra of prime-cover graphs
Idris Ali Shaik
Palomar RegistrySep 10, 2026math.COmachine-checkedscore 0
- The classification of compact 1-manifolds
Jim Fowler, Dennis Sweeney
Palomar RegistrySep 10, 2026math.GTmachine-checkedscore 0
- Global Stafford
Christopher Albert
Palomar RegistrySep 9, 2026math.RAmachine-checkedscore 0
- Verified external-to-swap regret reduction and correlated-equilibrium solver
Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz
Palomar RegistrySep 9, 2026cs.GTmachine-checkedscore 0
- Rerandomized Subsampled Trigonometric Transforms
Diar Heidary
Palomar RegistrySep 9, 2026math.NAmachine-checkedscore 0
- Formalization of power weight inequalities for spherical maximal functions
Joris Roos
Palomar RegistrySep 8, 2026math.CAmachine-checkedscore 0
- Finite correlated equilibria and regret certificates
Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz
Palomar RegistrySep 8, 2026cs.GTmachine-checkedscore 0
- Verified regret matching and finite-time equilibrium computation
Arthur Freitas Ramos
Palomar RegistrySep 8, 2026cs.GTmachine-checkedscore 0
- Erdős–Rado negative stepping-up for ordinal order types
Bruno Jartoux
Palomar RegistrySep 8, 2026math.LOmachine-checkedscore 0
- A real affine (23_4) configuration
Will Strinz
Palomar RegistrySep 8, 2026math.COmachine-checkedscore 0