Open Research Index

871 records

  1. Lean proofs of Dimitrov's Conjectures 1 and 3

    Michael Mazur

    Palomar RegistrySep 13, 2026math.NTmachine-checkedscore 0

  2. The Broughton--Huff theorem on increasing unions of sigma-fields

    Yi-Jing Tseng

    Palomar RegistrySep 12, 2026math.PRmachine-checkedscore 0

  3. Confinement schemas and the reach of block certificates for powers of rational numbers modulo one

    Ralf Stephan

    Palomar RegistrySep 12, 2026math.NTmachine-checkedscore 0

  4. 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

  5. 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

  6. The Kolmogorov-Arnold representation theorem

    George A. Constantinides

    Palomar RegistrySep 11, 2026math.CAmachine-checkedscore 0

  7. 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

  8. 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

  9. Three Sharp Bounds for Hansen Polytopes of Cographs

    Jeremy P Parker

    Palomar RegistrySep 10, 2026math.MGmachine-checkedscore 0

  10. Short-Cycle Decompositions and Full Zombie Damage in Cubic Graphs

    Lennart Rudolph

    Palomar RegistrySep 10, 2026math.COmachine-checkedscore 0

  11. KR-mod9-lean

    Yuma Mizuno

    Palomar RegistrySep 10, 2026math.NTmachine-checkedscore 0

  12. Irreducible improper phi-regret in Lean

    Arthur Freitas Ramos

    Palomar RegistrySep 10, 2026cs.GTmachine-checkedscore 0

  13. Density-one prescribed-rank spectra of prime-cover graphs

    Idris Ali Shaik

    Palomar RegistrySep 10, 2026math.COmachine-checkedscore 0

  14. The classification of compact 1-manifolds

    Jim Fowler, Dennis Sweeney

    Palomar RegistrySep 10, 2026math.GTmachine-checkedscore 0

  15. Global Stafford

    Christopher Albert

    Palomar RegistrySep 9, 2026math.RAmachine-checkedscore 0

  16. 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

  17. Rerandomized Subsampled Trigonometric Transforms

    Diar Heidary

    Palomar RegistrySep 9, 2026math.NAmachine-checkedscore 0

  18. Formalization of power weight inequalities for spherical maximal functions

    Joris Roos

    Palomar RegistrySep 8, 2026math.CAmachine-checkedscore 0

  19. 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

  20. Verified regret matching and finite-time equilibrium computation

    Arthur Freitas Ramos

    Palomar RegistrySep 8, 2026cs.GTmachine-checkedscore 0

  21. Erdős–Rado negative stepping-up for ordinal order types

    Bruno Jartoux

    Palomar RegistrySep 8, 2026math.LOmachine-checkedscore 0

  22. A real affine (23_4) configuration

    Will Strinz

    Palomar RegistrySep 8, 2026math.COmachine-checkedscore 0

  23. Sharp Bounds for Graph Matrices

    Diar Heidary

    Palomar RegistrySep 8, 2026math.PRmachine-checkedscore 0

  24. Lichnerowicz--Obata first eigenvalue and round-sphere rigidity

    Arthur Freitas Ramos

    Palomar RegistrySep 8, 2026math.DGmachine-checkedscore 0

  25. Refined Arbitrary-Target Transport Through Collatz Endpoints

    Idris Ali Shaik

    Palomar RegistrySep 7, 2026math.NTmachine-checkedscore 0

  26. Subspace embeddings with the rerandomized SRHT

    Yuning Yang

    Palomar RegistrySep 7, 2026math.NAmachine-checkedscore 0

  27. A proof of the Bollobás–Nikiforov conjecture in Lean

    Gabriel Coutinho, Yinchen Liu, Thomás Jung Spier, Quanyu Tang, Shengtong Zhang

    Palomar RegistrySep 7, 2026math.COmachine-checkedscore 0

  28. Distance-shell tomography: product kernels and sharp grid sensing

    Lennart Rudolph

    Palomar RegistrySep 7, 2026math.COmachine-checkedscore 0

  29. The rearrangement number: non(M) ≤ rr

    Vinicius de Oliveira Rodrigues

    Palomar RegistrySep 7, 2026math.LOmachine-checkedscore 0

  30. Dimension-independent Hlawka constants for Schatten norms

    Ezzeri Esa

    Palomar RegistrySep 7, 2026math.FAmachine-checkedscore 0

  31. Ceiling orbits of rational bases are not P-recursive

    Ralf Stephan

    Palomar RegistrySep 7, 2026math.NTmachine-checkedscore 0

  32. The maximal difference theorem for s-numbers

    Mario Ullrich

    Palomar RegistrySep 7, 2026math.FAmachine-checkedscore 0

  33. Native Lean finite Nash equilibria

    Arthur Freitas Ramos

    Palomar RegistrySep 7, 2026math.LOmachine-checkedscore 0

  34. A two-to-one executable map between Tunnell representation sets under the Tunnell balance

    Aakash Gurung

    Palomar RegistrySep 7, 2026math.NTmachine-checkedscore 0

  35. Hoeffding's extrema of the number of successes at a fixed mean

    George A. Constantinides

    Palomar RegistrySep 7, 2026math.PRmachine-checkedscore 0

  36. gn-lean: the Gurvich–Naumova partition conjecture

    JD Jones

    Palomar RegistrySep 7, 2026math.COmachine-checkedscore 0

  37. Dependent finite mixed Nash equilibria in Lean

    Arthur Freitas Ramos

    Palomar RegistrySep 7, 2026math.LOmachine-checkedscore 0

  38. De Lellis--Topping almost-Schur inequality

    Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz

    Palomar RegistrySep 7, 2026math.DGmachine-checkedscore 0

  39. elliotglazer/erdos501

    Elliot Glazer

    Palomar RegistrySep 6, 2026math.LOmachine-checkedscore 0

  40. A proof of the Regts–Sevenster conjecture, formalized

    William Whistler

    Palomar RegistrySep 6, 2026math.COmachine-checkedscore 0

  41. rwst/Square-Roots

    Ralf Stephan (direction, review, paper author)

    Palomar RegistrySep 6, 2026math.NTmachine-checkedscore 0

  42. rwst/Confinement-Certificates

    Ralf Stephan (direction, review, paper author)

    Palomar RegistrySep 6, 2026math.NTmachine-checkedscore 0

  43. Polylogarithmic Descent for Almost All Collatz Orbits in Natural Density

    Idris Ali Shaik

    Palomar RegistrySep 6, 2026math.NTmachine-checkedscore 0

  44. Lean formalization toward Bugeaud Problem 10.61

    Ralf Stephan

    Palomar RegistrySep 6, 2026math.NTmachine-checkedscore 0

  45. Convex geometry and the Erdős–Ginzburg–Ziv problem: Theorem 1.2

    Dmitrii Zakharov

    Palomar RegistrySep 6, 2026math.COmachine-checkedscore 0

  46. The sharp finite-field Nikodym exponent

    Ting-Wei Chao, Zach Hunter, Cosmin Pohoata, Hung-Hsun Hans Yu, Shengtong Zhang

    Palomar RegistrySep 6, 2026math.COmachine-checkedscore 0

  47. Spherical maximal functions: theorems of Stein and Bourgain

    Joris Roos

    Palomar RegistrySep 6, 2026math.CAmachine-checkedscore 0

  48. Double-contracted second Bianchi identity for metric-compatible torsion-free connections

    Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz

    Palomar RegistrySep 6, 2026math.DGmachine-checkedscore 0

  49. The density Hales–Jewett theorem and Szemerédi's theorem

    Gabriel Dahia

    Palomar RegistrySep 6, 2026math.COmachine-checkedscore 0

  50. Marton's conjecture (the polynomial Freiman-Ruzsa conjecture)

    Aaron Anderson, Mantas Bakšys, Jonas Bayer, Mauricio Collares, Rémy Degenne, Yaël Dillies, Ben Eltschig, Sébastien Gouëzel

    Palomar RegistrySep 6, 2026math.COmachine-checkedscore 0

Next page