Mathematics · Formal verification
Idris Ali Shaik
Independent researcher working in quantitative number theory and combinatorics. Progress on the Collatz conjecture and proved cases of Gallai’s path-decomposition conjecture, alongside arithmetic graph spectra. Full Lean 4 formalization projects submitted to Palomar; each registered entry specifies the declarations it verifies.
- Open preprints
- 7
- Palomar entries
- 7
- Registered declarations
- 38
- Interactive explainers
- 2
Research
| Result | Preprint | Formal verification | Explore |
|---|---|---|---|
| Collatz dynamics Quantitative almost-all theorems for the Collatz map in ordinary natural density. | |||
| Polylogarithmic Descent for Almost All Collatz Orbits in Natural Density For any f(n) → ∞, almost every n in natural density reaches an iterate below (log n)^A_FP · f(n) after c* log n + O(√(log n log log n)) shortcut steps, with an explicit exponent A_FP ≈ 9.9911. 11B8337P9960G40 | v4.0.22026-10-0410.5281/zenodo.23132901Zenodo · CC BY 4.0 · SSRN | 2026-08-26-000005v4high trust · 4 declarationsFirstPassageLinearTransport · FirstPassageLinearTransport-PalomarLean archive 23043600 | Interactive explainerwritten for v3.2.4Theorem → Lean map |
| Quantitative Endpoint Transport for the Collatz Map with a Natural-Density Descent Application A reusable arbitrary-target endpoint-transport theorem, with exponent asymptotically linear in the input density exponent, giving natural-density descent to exp((log n)^(1−δ)) for every δ < 0.25124…. 11B8337P9960F10 | v2.2.02026-09-0610.5281/zenodo.22544006Zenodo · CC BY 4.0 · SSRN | 2026-08-27-000018v3high trust · 1 declarationCET · CollatzEndpointTransport-PalomarLean archive 22544010 | Interactive explainerwritten for v2.0.3Theorem → Lean map |
| Positive density of Collatz convergence at every rate above 3/log(4/3) A positive proportion of integers reach 1 within c log x ordinary Collatz steps for every fixed c > 3/log(4/3), with one lower density bound independent of c. 11B8337P99 | v1.0.02026-09-2110.5281/zenodo.22871622Zenodo · CC BY 4.0 · SSRN | 2026-09-23-000002v1high trust · 18 declarationsCollatzConvergencePositiveDensity | — |
| Path decompositions Cases of Gallai's conjecture that every connected graph on n vertices splits into at most ⌈n/2⌉ paths. | |||
| Gallai's conjecture with two exceptional even vertices Extends the endpoint form of Gallai's conjecture to two designated even vertices that need not be adjacent, when every other even vertex has at most three even neighbours. 05C3805C70 | v1.0.02026-10-0410.5281/zenodo.23134427Zenodo · CC BY 4.0 | 2026-10-04-000006v1high trust · 4 declarationsgallai-two-exception | — |
| Gallai's Path Decomposition Conjecture for Graphs with Small Bowtie Boundaries Graphs whose even-degree subgraph has a whole-bowtie component with at most four external neighbours admit ⌈|V|/2⌉ path decompositions; a computer-assisted proof with finite reconstruction certificates. 05C3805C70 | v0.82026-09-1410.5281/zenodo.22754815Zenodo · CC BY 4.0 · SSRN | 2026-09-14-000005v1high trust · 6 declarationsgallai-bowtie-removalLean archive 22733632 | — |
| Arithmetic graph spectra Adjacency spectra of graphs built from multiplication by primes. | |||
| Prime-Star Localization and Second-Order Spectra of Finite Divisibility Cover Graphs For the graph joining n to np on [1, X], the top adjacency eigenvalue satisfies λ₁² = π(X) + 4 Σ_{p≤X} 1/(p−1) + o(1), via a large-prime star forest whose first-order perturbation vanishes. 05C5011N05 | v1.12026-08-2910.5281/zenodo.22163492Zenodo · CC BY 4.0 · SSRN | 2026-08-29-000017v2high trust · 3 declarationsprime-star-spectra-formalization | — |
| Prescribed Eigenvalues in Power Bands of Finite Prime-Cover Graphs Prescribed-rank eigenvalue estimates in growing power bands, including an every-centre paper theorem for 21/61 < θ < 1/2. The Palomar formalization covers selected density-one estimates for 0 < θ < 1/2. 05C5011N05 | v2026-09-192026-09-1910.2139/ssrn.7441718SSRN · CC BY 4.0 | 2026-09-10-000004v1high trust · 2 declarationsprime-cover-power-band-spectra-palomar | — |
Versions and dates are those of the latest public record. Titles link to the paper DOI; Zenodo records also list earlier versions. SSRN dates identify the public revision.
Graduate explainers
Long-form companion pages for first-year graduate students: the theorem in context, the proof architecture step by step, and figures computed from the actual map. They are optional reading — the preprint is always the reference.
What the formal verification certifies
Each Palomar entry records a Lean 4 project at one pinned GitHub commit, the selected declarations that were machine-checked against it, and an archival fork that preserves the source. A high trust level means the registry's checks passed for those declarations.
This is mechanical verification and preservation, not peer review. It certifies the listed declarations — not every specialization, remark or literature comparison in the manuscript. Each manuscript is written to be checked independently of its formalization.
Scope. The Collatz results are almost-all statements in natural density, or positive-density statements; none proves the Collatz conjecture or excludes exceptional cycles or divergent orbits. The path-decomposition results settle specific cases; Gallai's conjecture in general remains open.