papers: 10 relevant math papers from May 2026

1. Singer Sidon Sets in Lean 4 (2605.03274) — 7541 lines, zero sorry
2. AutoformBot: 45K Lean declarations from 26 textbooks (2605.29955)
3. Rust-to-Lean verification pipeline (2605.30106)
4. Hexagonal lattice + RG + fractal dimension (2605.09974)
5. Burgers + Hopf-Cole unified transform (2605.11788)
6. Self-orthogonal Reed-Solomon → quantum ECC (2605.23460)
7. Hash-based GPU 3D reconstruction (2511.21459)
8. Conjugacy classes of positive 3-braids (2604.16876)
9. Navier-Stokes non-uniqueness (2605.29934)
10. Continuum limit of causal fermion systems (2605.30199)

Most relevant to Research Stack:
- #1: Direct Sidon set infrastructure for Lean
- #4: RG + fractal dimension exact results
- #5: Hopf-Cole Burgers (confirms our approach)
- #6: RS codes → quantum ECC (VCN pipeline connection)

shared-data/papers/2026-05/2511.21459.json

@@ -0,0 +1,13 @@
+{
+  "arxiv_id": "2511.21459",
+  "title": "Hash-based GPU 3D Reconstruction",
+  "authors": [
+    "Lorenzo De Rebotti",
+    "Emanuele Giacomini",
+    "Giorgio Grisetti",
+    "Luca Di Giammarino"
+  ],
+  "abstract": "Abstract:Efficient and scalable 3D surface reconstruction from range data remains a core challenge in computer graphics and vision, particularly in real-time and resource-constrained scenarios. Traditional volumetric methods based on fixed-resolution voxel grids or hierarchical structures like octrees often suffer from memory inefficiency, computational overhead, and a lack of GPU support. We propose a novel variance-adaptive, multi-resolution voxel grid that dynamically adjusts voxel size based on the local variance of signed distance field (SDF) observations. Unlike prior multi-resolution approaches that rely on recursive octree structures, our method leverages a flat spatial hash table to store all voxel blocks, supporting constant-time access and full GPU parallelism. This design enables high memory efficiency and real-time scalability. We further demonstrate how our representation supports GPU-accelerated rendering through a parallel quad-tree structure for Gaussian Splatting, enabling effective control over splat density. Our open-source CUDA/C++ implementation achieves up to 13x speedup and 4x lower memory usage compared to fixed-resolution baselines, while maintaining on par results in terms of reconstruction accuracy, offering a practical and extensible solution for high-performance 3D reconstruction.",
+  "url": "https://arxiv.org/abs/2511.21459",
+  "pdf_path": "/home/allaun/Research Stack/shared-data/papers/2026-05/2511.21459.pdf"
+}

shared-data/papers/2026-05/2604.16876.json

@@ -0,0 +1,11 @@
+{
+  "arxiv_id": "2604.16876",
+  "title": "Conjugacy Classes of Positive 3-Braids",
+  "authors": [
+    "Kui-Yo Chen",
+    "Yat-Hin Suen"
+  ],
+  "abstract": "Abstract:The conjugacy problem in braid groups has been extensively studied, particularly from an algorithmic perspective. Established methods based on Garside structures, such as initial summit sets and super summit sets, provide effective procedures for determining whether two braids are conjugate. In contrast, explicit structural descriptions of conjugacy classes are less frequently addressed. Although cyclic sliding offers a powerful mechanism for navigating distinguished subsets within a conjugacy class, it is well known that conjugate braids cannot, in general, be obtained from one another solely through iterated cyclic sliding. In this paper, we provide a direct and explicit characterization of the conjugacy classes of positive $3$-braids. Specifically, for any given positive $3$-braid, we determine all of its conjugates in a concrete and closed form.",
+  "url": "https://arxiv.org/abs/2604.16876",
+  "pdf_path": "/home/allaun/Research Stack/shared-data/papers/2026-05/2604.16876.pdf"
+}

shared-data/papers/2026-05/2605.03274.json

@@ -0,0 +1,13 @@
+{
+  "arxiv_id": "2605.03274",
+  "title": "Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4",
+  "authors": ["Hulak, David B.", "Ramos, Arthur F.", "de Queiroz, Ruy J. G. B."],
+  "abstract": "Erdős Problem 30 asks for sharp asymptotics of the Sidon extremal function h(N), and Singer's construction is the classical source of lower-bound examples matching the main term. We present a Lean 4 formalization of Singer's Sidon set construction, together with reusable Sidon-set infrastructure for additive combinatorics. For every prime power q=p^k, we prove the existence of a Sidon set modulo q^2+q+1 of cardinality q+1; the prime-field case q=p is the base presentation. The proof proceeds through a non-trivial algebraic chain: construction of the base field and its degree-three extension, analysis of the trace kernel as a 2-dimensional subspace over the base field, a geometric argument via subspace intersections establishing the multiplicative Sidon property in the quotient group, and a transfer from quotient multiplication to modular integer addition. Around this central result, we develop a reusable Sidon set library. It comprises interval and modular Sidon sets, the extremal function h(N), Lindström's cross-difference inequality, a Johnson-route shift-incidence upper bound of the form h(N)≤√N+N^{1/4}+O(1), representation-function identities, and unconditional two-sided h(N)=Θ(√N) bounds with exact floor-rounded finite statements for N≥5. We further formalize a conditional reduction: subpolynomial prime gaps together with a full subpolynomial upper-error hypothesis for h(N) imply the Erdős Problem 30 estimate h(N)=√N+O_ε(N^ε) for every ε>0. The Singer/Sidon modules and transfer lemmas comprise 7,541 lines of Lean 4 with zero active uses of sorry.",
+  "url": "https://arxiv.org/abs/2605.03274",
+  "pdf_url": "https://arxiv.org/pdf/2605.03274",
+  "pdf_file": "2605.03274.pdf",
+  "pdf_size": "588K",
+  "date": "2026-05-05",
+  "topics": ["Lean 4", "formalization", "additive combinatorics", "Sidon sets", "Singer construction"],
+  "fetched_at": "2026-05-30"
+}

shared-data/papers/2026-05/2605.09974.json

@@ -0,0 +1,13 @@
+{
+  "arxiv_id": "2605.09974",
+  "title": "Localization phase diagram of the Hexagonal Lattice with irrational magnetic flux",
+  "authors": ["Gao, Qi", "Zhang, Shuo", "Chen, Wei"],
+  "abstract": "We study the Hofstadter model on a hexagonal lattice with irrational magnetic flux in this work. The Hofstadter model of the square lattice with irrational flux has been solved mathematically by Avila in his Fields medal work. However, this theory is usually not applicable to lattices with internal degrees of freedom, such as spin or sub-lattices. In this work, we show that for the hexagonal lattice with only nearest neighbor hopping, the system can still be characterized by a 2x2 transfer matrix and solved exactly by Avila's global theory although this lattice has two sub-lattices. We obtained the exact localization phase diagram of the hexagonal lattice with irrational flux by this theory, which reveals three pure phases, that is, the extended, localized and critical states but no mobility edge due to the chiral symmetry. We used the renormalization group (RG) theory to verify these results, which can determine part of the phase diagram. We then computed the fractal dimension of the remaining part numerically. The results from both the RG theory and numerical analysis confirmed the phase diagram we get from Avila's global theory.",
+  "url": "https://arxiv.org/abs/2605.09974",
+  "pdf_url": "https://arxiv.org/pdf/2605.09974",
+  "pdf_file": "2605.09974.pdf",
+  "pdf_size": "1.3M",
+  "date": "2026-05-14",
+  "topics": ["Hofstadter model", "hexagonal lattice", "irrational magnetic flux", "localization", "renormalization group", "fractal dimension"],
+  "fetched_at": "2026-05-30"
+}

shared-data/papers/2026-05/2605.11788.json

@@ -0,0 +1,13 @@
+{
+  "arxiv_id": "2605.11788",
+  "title": "The unified transform for Burgers' equation: Application to unsaturated flow in finite interval",
+  "authors": ["Kalimeris, Konstantinos", "Mindrinos, Leonidas", "Paraskevopoulos, Athanasios"],
+  "abstract": "In this paper, we focus on one-dimensional vertical infiltration, assuming constant diffusivity and a quadratic relationship between hydraulic conductivity and water content. Under these assumptions, Richards' equation reduces to Burgers' equation, which we then linearize via the Hopf-Cole transformation. This turns the initial boundary value problem into a diffusion equation on a finite interval with mixed boundary conditions. To solve it, we use the Unified Transform Method (also known as the Fokas method). This approach gives an explicit integral representation of the solution, and when evaluated numerically, the results match classical Fourier series solutions exactly, but with better convergence and stability. Two examples from hydrological applications are examined.",
+  "url": "https://arxiv.org/abs/2605.11788",
+  "pdf_url": "https://arxiv.org/pdf/2605.11788",
+  "pdf_file": "2605.11788.pdf",
+  "pdf_size": "1.4M",
+  "date": "2026-05-16",
+  "topics": ["Burgers equation", "Hopf-Cole transformation", "unified transform method", "Fokas method", "hydrology", "Richards equation"],
+  "fetched_at": "2026-05-30"
+}

shared-data/papers/2026-05/2605.23460.json

@@ -0,0 +1,12 @@
+{
+  "arxiv_id": "2605.23460",
+  "title": "Self-Orthogonal Reed-Solomon \u2192 Quantum ECC",
+  "authors": [
+    "Yanxin Chen",
+    "Yanli Wang",
+    "Tongjiang Yan"
+  ],
+  "abstract": "Abstract:In this paper, two classes of twisted generalized Reed-Solomon (TGRS) codes with multi-twists are studied. Firstly, some sufficient and necessary conditions for these codes to be self-orthogonal and self-dual are established. Then several explicit constructions of self-orthogonal and self-dual codes are presented, from which quantum stabilizer codes are further derived. Finally, some corresponding examples are given, especially that some of these codes are MDS, AMDS or NMDS and that some of the resulting quantum stabilizer codes are optimal, achieving the quantum Singleton bound.",
+  "url": "https://arxiv.org/abs/2605.23460",
+  "pdf_path": "/home/allaun/Research Stack/shared-data/papers/2026-05/2605.23460.pdf"
+}

shared-data/papers/2026-05/2605.29934.json

@@ -0,0 +1,12 @@
+{
+  "arxiv_id": "2605.29934",
+  "title": "Navier-Stokes Non-Uniqueness",
+  "authors": [
+    "Zipeng Chen",
+    "Song Liu",
+    "Zhaoyang Yin"
+  ],
+  "abstract": "Abstract:In this paper, we consider the generalized Navier-Stokes equations with fritional dissipation $(-\\Delta)^{\\beta}$ with $\\beta>\\frac{1}{2}$. When $\\beta\\in(1,2)$, We prove that smooth solutions of the generalized Navier-Stokes equations are non-unique with arbitrarily small initial data in $\\dot{B}^{-\\beta-\\alpha}_{\\infty,1}(\\mathbb{T}^d)$ for any $\\alpha>0$. It is worth pointing out that the space $\\dot{B}^{-\\beta-\\alpha}_{\\infty,1}(\\mathbb{T}^d)$ is subcritical for $0<\\alpha<\\beta-1$. To the best of our knowledge, this is the first non-uniqueness result of Navier-Stokes equations with initial data at the critical regularity. To show the sharpness of the above results, for $\\beta>\\frac{1}{2}$, we establish the local well-poseness of the generalized Navier-Stokes equations with small initial data in $\\dot{B}^{-\\beta-\\alpha}_{\\infty,\\infty}(\\mathbb{T}^d)$ with $\\alpha<0$ and $\\alpha\\leq\\beta-1$.",
+  "url": "https://arxiv.org/abs/2605.29934",
+  "pdf_path": "/home/allaun/Research Stack/shared-data/papers/2026-05/2605.29934.pdf"
+}

shared-data/papers/2026-05/2605.29955.json

@@ -0,0 +1,13 @@
+{
+  "arxiv_id": "2605.29955",
+  "title": "Formalizing Mathematics at Scale",
+  "authors": ["Rammal, Ahmad", "Patel, Niket", "Gloeckle, Fabian", "Hayat, Amaury", "Kempe, Julia", "Munos, Remi", "Arnal, Charles", "Cabannes, Vivien"],
+  "abstract": "We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible.",
+  "url": "https://arxiv.org/abs/2605.29955",
+  "pdf_url": "https://arxiv.org/pdf/2605.29955",
+  "pdf_file": "2605.29955.pdf",
+  "pdf_size": "1.1M",
+  "date": "2026-05-30",
+  "topics": ["Lean 4", "autoformalization", "multi-agent", "LLM", "Atlas", "formal verification"],
+  "fetched_at": "2026-05-30"
+}

shared-data/papers/2026-05/2605.30106.json

@@ -0,0 +1,13 @@
+{
+  "arxiv_id": "2605.30106",
+  "title": "A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report",
+  "authors": ["Klaus, Natalia", "Tolmach, Palina", "Conejero, Juan"],
+  "abstract": "We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components: symbolic extraction tools (Charon and Aeneas, or Hax) that lift Rust into Lean 4; formal cryptographic specification libraries (ArkLib and CompPoly, from the Verified zkEVM project) that provide the mathematical targets; and AI provers (Aristotle from Harmonic AI and Aleph from Logical Intelligence) that close the resulting proof obligations. Every proof is checked by the Lean kernel, so AI output cannot compromise soundness. Within the scope of the Ethereum Foundation's zkEVM Verification Project, we applied the pipeline to cryptographic primitives in Plonky3 (FRI folding, Mersenne31 and KoalaBear field arithmetic, Horner polynomial evaluation) and RISC Zero (Merkle inclusion verification). In addition, Aleph authored proofs of two bounds-style theorems in Plonky3's compute_log_arity_for_round that previously stood as sorry.",
+  "url": "https://arxiv.org/abs/2605.30106",
+  "pdf_url": "https://arxiv.org/pdf/2605.30106",
+  "pdf_file": "2605.30106.pdf",
+  "pdf_size": "661K",
+  "date": "2026-05-30",
+  "topics": ["Rust", "Lean 4", "formal verification", "AI provers", "zkEVM", "cryptographic verification"],
+  "fetched_at": "2026-05-30"
+}

shared-data/papers/2026-05/2605.30199.json

@@ -0,0 +1,11 @@
+{
+  "arxiv_id": "2605.30199",
+  "title": "Continuum Limit of Causal Fermion Systems",
+  "authors": [
+    "Patrick Fischer",
+    "Felix Finster"
+  ],
+  "abstract": "Abstract:We construct the causal fermion system for globally hyperbolic spacetimes starting in the framework of algebraic quantum field theory. The fermionic projector is identified with the one-particle density operator of a quasi-free Hadamard state. The ultraviolet regularization is built into the fermionic projector via a chart-independent $i\\varepsilon$-regularization scheme. The continuum limit analysis is developed in globally hyperbolic spacetimes. It is shown that the Euler-Lagrange equations of the causal action principle are satisfied in this setup if and only if the coupled Einstein-Dirac equations hold.",
+  "url": "https://arxiv.org/abs/2605.30199",
+  "pdf_path": "/home/allaun/Research Stack/shared-data/papers/2026-05/2605.30199.pdf"
+}