-
Notifications
You must be signed in to change notification settings - Fork 55
Pull requests: thefundamentaltheor3m/Sphere-Packing-Lean
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
Use upstreamed modular form derivative theorems
#478
opened Sep 8, 2026 by
seewoo5
Collaborator
Loading…
refactor: extract shared pointwise q-series bounds
#477
opened Sep 8, 2026 by
cameronfreer
Contributor
Loading…
feat(MagicFunction): uniform quantitative contour bounds
#476
opened Sep 8, 2026 by
cameronfreer
Contributor
•
Draft
Updates available and ready to merge
auto-update-lean
#475
opened Sep 8, 2026 by
github-actions
Bot
Loading…
Updates available and ready to merge
auto-update-lean
#474
opened Sep 8, 2026 by
github-actions
Bot
Loading…
feat(MagicFunction): exact Fourier expansions of the quadratic products
#473
opened Sep 1, 2026 by
cameronfreer
Contributor
•
Draft
feat(MagicFunction): polynomial bounds on Cauchy-product coefficients
awaiting-review
This PR is ready to be reviewed.
#472
opened Sep 1, 2026 by
cameronfreer
Contributor
Loading…
fix(MagicFunction): remove the invalid norm_φ₀_le proof path
#468
opened Sep 1, 2026 by
cameronfreer
Contributor
•
Draft
refactor(CauchyGoursat): assume vanishing of the top-edge integral
awaiting-review
This PR is ready to be reviewed.
#467
opened Sep 1, 2026 by
cameronfreer
Contributor
Loading…
feat(MagicFunction): estimates for the double-zero contour deformation
#466
opened Sep 1, 2026 by
cameronfreer
Contributor
•
Draft
feat(MagicFunction): estimates near the cusp for φ₀ on the imaginary axis
#465
opened Sep 1, 2026 by
cameronfreer
Contributor
•
Draft
feat(MagicFunction): joint integrability and Fubini for the contour integrals Iⱼ
#464
opened Sep 1, 2026 by
cameronfreer
Contributor
•
Draft
feat(MagicFunction): shared integrable majorants for contour integrands
#463
opened Sep 1, 2026 by
cameronfreer
Contributor
•
Draft
chore: bump mathlib to v4.34.0-rc2
awaiting-author
Awaiting the author's response to a comment or review.
#462
opened Aug 31, 2026 by
thefundamentaltheor3m
Owner
Loading…
feat: improving bounds and restating things in the language of radial Schwartz functions
awaiting-author
Awaiting the author's response to a comment or review.
#460
opened Aug 25, 2026 by
thefundamentaltheor3m
Owner
Loading…
3 tasks done
blueprint: Refine sections on Fourier analysis, Cohn–Elkies and the Fourier eigenfunctions
awaiting-author
Awaiting the author's response to a comment or review.
#437
opened Jul 14, 2026 by
thefundamentaltheor3m
Owner
Loading…
feat(Tactic): nine custom tactics + repo-wide golf sweep
experimental
WON'T MERGE
This (should be draft if not already) PR is for showcase only, not merging!
[gauss] Cleaning Up Cohn-Elkies and Poisson Summation
#420
opened Jun 12, 2026 by
thefundamentaltheor3m
Owner
Loading…
feat(framework): re-prove rectLeft/rectRight via LeanModularForms HW-3.3 framework
#419
opened Jun 9, 2026 by
CBirkbeck
Collaborator
Loading…
Prepare defs for mathlib
awaiting-author
Awaiting the author's response to a comment or review.
#416
opened May 19, 2026 by
thefundamentaltheor3m
Owner
Loading…
Cleanup and golf FG.lean + update blueprint
awaiting-review
This PR is ready to be reviewed.
#410
opened Apr 26, 2026 by
seewoo5
Collaborator
Loading…
Golf Jacobi theta related code
awaiting-review
This PR is ready to be reviewed.
#392
opened Apr 14, 2026 by
seewoo5
Collaborator
Loading…
[gauss2] Import Trees
WON'T MERGE
This (should be draft if not already) PR is for showcase only, not merging!
#386
opened Mar 31, 2026 by
thefundamentaltheor3m
Owner
•
Draft
Previous Next
ProTip!
Updated in the last three days: updated:>2026-09-09.