- Brill--Noether generality and gonality for chains of cycles and theta graphs
Nathan Pflueger
Palomar RegistrySep 5, 2026math.COmachine-checkedscore 0
- The optimal universal exponential base for Euclidean kissing numbers
Sébastien Palcoux
Palomar RegistrySep 5, 2026math.MGmachine-checkedscore 0
- N4Code: optimal finite-length block codes of size four for binary symmetric channels
Shenghao Yang, Yanyan Dong
Palomar RegistrySep 5, 2026cs.ITmachine-checkedscore 0
- Exact four-dimensional projection quality of the OneTwo Sobol' table at 65,536 points
Lennart Rudolph
Palomar RegistrySep 5, 2026math.NAmachine-checkedscore 0
- Li's criterion for the Riemann Hypothesis
Nicholas Bulka
Palomar RegistrySep 5, 2026math.NTmachine-checkedscore 0
- The global Kronecker–Weber theorem in Lean 4
Naganori Yamaguchi
Palomar RegistrySep 5, 2026math.NTmachine-checkedscore 0
- Even-order Grünschloß–Keller permutation nets: net property and tiling distance
Lennart Rudolph
Palomar RegistrySep 4, 2026math.NAmachine-checkedscore 0
- Combinatorial core of the K₃,₃,₁-redundancy theorem for tetrahedral balls
Lennart Rudolph
Palomar RegistrySep 4, 2026math.COmachine-checkedscore 0
- A kernel-checked exclusion certificate for Erdős Problem 647, to 10^8
Ibrahim Mian, Shayaan Siddique
Palomar RegistrySep 4, 2026cs.LOmachine-checkedscore 0
- Sharp arithmetic separation in chiral Padovan histories
Stephanie Alexander
Palomar RegistrySep 4, 2026math.DSmachine-checkedscore 0
- Carlet's Kasami cyclic-additive conjecture
D.S. McNeil, Gábor P. Nagy, Attila Vajda
Palomar RegistrySep 4, 2026math.COmachine-checkedscore 0
- rwst/Even-Integral
Ralf Stephan (direction, review, paper author)
Palomar RegistrySep 3, 2026math.NTmachine-checkedscore 0
- lennrt/palomar-formalizations
Lennart Rudolph
Palomar RegistrySep 3, 2026math.COmachine-checkedscore 0
- lennrt/palomar-formalizations
Lennart Rudolph
Palomar RegistrySep 3, 2026math.COmachine-checkedscore 0
- lennrt/palomar-formalizations
Lennart Rudolph
Palomar RegistrySep 3, 2026cs.DSmachine-checkedscore 0
- lennrt/palomar-formalizations
Lennart Rudolph
Palomar RegistrySep 3, 2026cs.GRmachine-checkedscore 0
- lennrt/palomar-formalizations
Lennart Rudolph
Palomar RegistrySep 3, 2026math.COmachine-checkedscore 0
- ukiyois/hs-virial-nbc-identity
ukiyois
Palomar RegistrySep 3, 2026math.COmachine-checkedscore 0
- Levi–Civita connections and metric-determined curvature invariants in Lean
Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
Palomar RegistrySep 3, 2026math.DGmachine-checkedscore 0
- Ore's and Dirac's Theorems on Hamiltonian Cycles
Noah Cohen
Palomar RegistrySep 3, 2026math.COmachine-checkedscore 0
- A proof of Conway's refinement conjecture
Dan Abramov
Palomar RegistrySep 3, 2026math.LOmachine-checkedscore 0
- Tverberg's Partition Theorem, 1D Theorem, and Colorful 1D Theorem
Noah Cohen
Palomar RegistrySep 3, 2026math.MGmachine-checkedscore 0
- Radial harmonic functions on a real inner product space: the classification, the Laplacian of radial functions, and the stability of circular orbits for power-law central forces; Ehrenfest's dimensionality argument (1917) as the application
Stephanie Alexander
Palomar RegistrySep 3, 2026math.CAmachine-checkedscore 0
- Sharp bounds for intervals in finite subgroup lattices
Sébastien Palcoux
Palomar RegistrySep 3, 2026math.GRmachine-checkedscore 0
- Erdős Problem 684: f(n)/log n is unbounded — a Lean 4 formalization of arXiv:2604.23784
Ji Ho Bae
Palomar RegistrySep 3, 2026math.NTmachine-checkedscore 0
- Tucker's Lemma: Full Combinatorial & Topological Parity Suite in 1D and 2D
Noah Cohen
Palomar RegistrySep 3, 2026math.COmachine-checkedscore 0
- Actual F₂ flag homology and the dense extremal counterexample family
Lennart Rudolph
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- Salem's theorem: every Pisot number is a two-sided limit of Salem numbers
Stephanie Alexander
Palomar RegistrySep 2, 2026math.NTmachine-checkedscore 0
- Nash's isometric embedding theorem for closed manifolds (Günther's proof)
David Wiygul
Palomar RegistrySep 2, 2026math.DGmachine-checkedscore 0
- The De Bruijn–Erdős Theorem on Incidence Geometry and Near-Pencil Tightness
Noah Cohen
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- Erdős Problem 625: chromatic versus cochromatic number of a random graph
Samuil Petkov
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- An explicit periodic signing of C_n(1,2) below the conjectured minimum
Lennart Rudolph
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- Mean Value for Random Ideal Lattices: Lean formalization
Nihar Gargava
Palomar RegistrySep 2, 2026math.NTmachine-checkedscore 0
- The Kőnig–Egerváry Theorem on Matchings and Vertex Covers in Bipartite Graphs
Noah Cohen
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- heilbronn-convex-3-8
Tej Stead
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- Chip-Firing with Lean 4
Dhyey Dharmendrakumar Mavani, Nathan Pflueger
Palomar RegistrySep 2, 2026math.COmachine-checkedscore 0
- The trace form of a tensor product of algebras and the signature product rule, with the trace forms of Q[x]/(x^3 - x - 1), Q[x]/(x^4 - x - 1) and their compositum as instances
Stephanie Alexander
Palomar RegistrySep 2, 2026math.NTmachine-checkedscore 0
- JaTaSn/lattice-line-covers
Jan Snellman
Palomar RegistrySep 1, 2026math.COmachine-checkedscore 0
- Marshall Hall's theorem through finite cores
Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
Palomar RegistrySep 1, 2026math.GRmachine-checkedscore 0
- lean-operator-theory
Ezzeri Esa
Palomar RegistrySep 1, 2026math.FAmachine-checkedscore 0
- The entangled Born correlations: a mixed-state entanglement witness through the Born rule forced on the composite algebra
Stephanie Alexander
Palomar RegistrySep 1, 2026quant-phmachine-checkedscore 0
- lean-spectral-theory
Ezzeri Esa
Palomar RegistrySep 1, 2026math.FAmachine-checkedscore 0
- hadamard-b-formal: the bordered Goethals-Seidel characterisation, the s=1 layer, and Theorem D
JD Jones
Palomar RegistrySep 1, 2026math.COmachine-checkedscore 0
- Native Lean equality-saturation certificate checking
Arthur Freitas Ramos
Palomar RegistrySep 1, 2026cs.LOmachine-checkedscore 0
- Only two morphic numbers: the Aarts-Fokkink-Kruijtzer classification of the golden ratio and the plastic number
Stephanie Alexander
Palomar RegistrySep 1, 2026math.NTmachine-checkedscore 0
- Howson's theorem through finite cores and Kurosh decomposition
Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
Palomar RegistrySep 1, 2026math.GRmachine-checkedscore 0
- Proof-Carrying Decreasing-Diagram Confluence Certificates
Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
Palomar RegistrySep 1, 2026cs.LOmachine-checkedscore 0
- Arrow's theorem via Fourier analysis
Joris Roos
Palomar RegistrySep 1, 2026cs.DMmachine-checkedscore 0
- The golden family's boundary at n = 3: general-n theorems for x^n = x + 1
Stephanie Alexander
Palomar RegistrySep 1, 2026math.NTmachine-checkedscore 0
- Grushko--Neumann rank additivity for free products
Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
Palomar RegistrySep 1, 2026math.GRmachine-checkedscore 0