-
Notifications
You must be signed in to change notification settings - Fork 1
Pull requests: rjwalters/lean-genius
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
Enrich The Second Chebyshev Function ψ and Legendre's Identity (chebyshev-bounds-oq-02)
#30346
opened Jun 26, 2026 by
rjwalters
Owner
Loading…
research(erdos-1204): define A(k) and prove A(k) ≤ (k-1)·primorial(k) [verified, 0 axioms]
research
Research agent work
#30227
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(erdos-748-incomplete-01): max sum-free subset size = ⌈n/2⌉ [verified, +3 thm/0 axiom]
research
Research agent work
#30202
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(burnside-oq04oq02oq02): verified reflection-half of the dihedral bracelet sum
research
Research agent work
#30015
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(birthday-oq-03-01-01-03-03): general k-fold coincidence threshold n=(k!·d^{k-1}·ln2)^{1/k}+O(1) [verified, 0-axiom, original]
#29898
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(burnside-counting-oq-03-oq-02-oq-01-oq-02): cyclic necklace count in divisor-sum form ∑_{d∣n} φ(n/d)·k^d = (#necklaces)·n [verified, 0-axiom, original]
research
Research agent work
#29892
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(burnside-counting-oq-03-oq-02-oq-01-oq-02): necklace divisor-sum ∑_r k^{gcd(n,r)} = ∑_{d|n} φ(n/d)·k^d [verified, 0-axiom, original]
#29889
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(area-of-circle-oq-07-oq-05-oq-02): Gaussian second moment as Γ(3/2) via u=x² substitution
research
Research agent work
#29878
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research: cantor-diagonalization-oq-07-oq-01 + euler-totient + morleys-theorem-oq-02 [verified, 0-axiom]
research
Research agent work
#29819
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(cauchy-group-theorem-oq-01-oq-01-oq-01-oq-01-oq-03-oq-02-oq-01): power map over an arbitrary finite abelian group [verified, 0-axiom, original]
research
Research agent work
#29806
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
Research: Frobenius power subgroups recover the divisor lattice (⟨frob^e⟩ ≤ ⟨frob^d⟩ ⇔ d ∣ e)
research
Research agent work
#29794
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(spectral-trace-det-eigenvalues-oq-01-oq-01-oq-02-oq-01): Newton's fourth power sum tr(A⁴)=λ₁⁴+λ₂⁴+λ₃⁴+λ₄⁴ [verified, 0-axiom, original]
research
Research agent work
#29783
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(spectral-trace-det-eigenvalues-oq-01-oq-01-oq-02-oq-01): Newton's fourth power sum tr(A⁴)=Σλᵢ⁴ in dimension four [verified, 0-axiom, original]
#29782
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(catalan-numbers-oq-01-oq-04): strict log-convexity C(n+1)²<C(n)·C(n+2) [verified, 0-axiom, original]
#29663
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(pell-equation-oq-01-oq-04-oq-01): Pell regulator is ℤ-linear — norm & regulator laws for all integer powers [verified, 0-axiom]
#29618
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(stirling-second-kind-oq-01-oq-03): second subdiagonal S(n,n−2)=C(n,3)+3C(n,4) [verified, 0-axiom, original]
#29577
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(mellin-oq-01-oq-01): general interval (b^s-a^s)/s and power-weighted strip Re s > -c
#29555
opened Jun 25, 2026 by
rjwalters
Owner
Loading…
research(kummer-theorem-oq-04-oq-01-oq-01): C(2n,n) divisible by 4 exactly ⟺ n = 2^a+2^b (popcount 2) [verified, 0-axiom, original]
#29445
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
research(mantel-theorem-oq-03-oq-01): sharpness of the Mantel minimum-degree bound [verified, 0-axiom, original]
research
Research agent work
#29444
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
research(dyck-catalan-count-oq-01-oq-01): rooted plane trees counted by Catalan via explicit Dyck-word bijection [verified, 0-axiom, original]
#29402
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
research(stirling-second-kind-oq-01-oq-01): third column S(n,3)=(3ⁿ⁻¹+1)/2−2ⁿ⁻¹ [verified, 0-axiom]
research
Research agent work
#29388
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
research(wilsons-theorem-oq-05-oq-01-oq-01-oq-01-oq-01): Kempner function determined by prime powers — S(n) = max S(p^k) [verified, 0-axiom]
research
Research agent work
#29350
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
research(baire-category-theorem-oq-01-oq-03): ℚ is not a Gδ; no function continuous exactly at the rationals [verified, 0-axiom]
research
Research agent work
#29317
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
research(combinations-formula-oq-01-oq-01-oq-02): signed shallow-diagonal sum is 6-periodic [verified, 0-axiom]
research
Research agent work
#29302
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
Enrich Carmichael lcm of prime-power values
enrichment
Gallery proof enrichment
#29224
opened Jun 24, 2026 by
rjwalters
Owner
Loading…
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.