Skip to content

Pull requests: thefundamentaltheor3m/Sphere-Packing-Lean

New pull request New
37 Open 330 Closed
37 Open 330 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

refactor(ComplexIntegrands): extract Möbius -1/(z+c) holomorphicity API
#425 opened Jun 21, 2026 by cameronfreer Contributor Loading…
1 task done
Fix #218: restate extracted_1 with X ⊆ Λ hypothesis and prove finiteness
#424 opened Jun 20, 2026 by Robby955 Loading…
1
golf(JacobiTheta): tendsto_cont, \mapsto awaiting review The PR is ready to be reviewed
#422 opened Jun 18, 2026 by seewoo5 Collaborator Loading…
Bump Lean to v4.31.0
#421 opened Jun 18, 2026 by seewoo5 Collaborator Loading…
[gauss] Cleaning Up Cohn-Elkies and Poisson Summation
#420 opened Jun 12, 2026 by thefundamentaltheor3m Owner • Draft
1
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 review The PR is ready to be reviewed
#416 opened May 19, 2026 by thefundamentaltheor3m Owner Loading…
7
Add Cleanup Tasks to gauss2
#415 opened May 5, 2026 by thefundamentaltheor3m Owner Loading…
2
Cleanup and golf FG.lean
#410 opened Apr 26, 2026 by seewoo5 Collaborator Loading…
1 of 2 tasks
2
[codex] Move slash MDiff lemmas to ForMathlib awaiting review The PR is ready to be reviewed
#392 opened Apr 14, 2026 by seewoo5 Collaborator Loading…
3
[gauss2] [wip] golf HExpansions.lean
#388 opened Apr 1, 2026 by b-mehta Collaborator Loading…
4
[gauss2] Import Trees
#386 opened Mar 31, 2026 by thefundamentaltheor3m Owner • Draft
feat: extend tendsto_cont with dischargers, nhdsWithin, and trace mode
#384 opened Mar 30, 2026 by cameronfreer Contributor Loading…
feat: Gauss formalization of E₈ optimality in ℝ⁸ (rebased)
#356 opened Mar 12, 2026 by arajasek Collaborator • Draft
feat: norm_numI improvements from Gauss
#345 opened Mar 4, 2026 by dwrensha Collaborator Loading…
9
Gauss: complete formalization of E₈ optimality in ℝ⁸
#341 opened Feb 23, 2026 by augustepoiroux Collaborator • Draft
19
feat(FG): prove F_eq_FReal, G_eq_GReal, FmodG_eq_FmodGReal, FReal_Differentiable, GReal_Differentiable
#340 opened Feb 22, 2026 by pitmonticone Collaborator Loading…
2
feat(Schwartz): prove I₃'_decay' awaiting review The PR is ready to be reviewed
#339 opened Feb 22, 2026 by pitmonticone Collaborator Loading…
Prove FG_inequality_1 and FG_inequality_2 awaiting-review
#331 opened Feb 3, 2026 by seewoo5 Collaborator Loading…
5
chore: integrate LeanArchitect and bump infrastructure
#329 opened Jan 31, 2026 by hanwenzhu Contributor • Draft
@pitmonticone
filling sorries in LPBound
#319 opened Jan 28, 2026 by ster-oc Loading…
5
feat(FourierExpansions): q-series infrastructure and Fourier expansion identities
#317 opened Jan 28, 2026 by cameronfreer Contributor • Draft
2
Existence of smooth cutoff function
#316 opened Jan 27, 2026 by mattcushman Contributor Loading…
Compute limit $\lim_{t \to 0^+} F(it) / G(it) = 18 / \pi^2$ awaiting-review
#307 opened Jan 21, 2026 by seewoo5 Collaborator Loading…
1
19
feat(MagicFunction): add FourierExpansions and PhiBounds for phi norm bounds awaiting-review
#304 opened Jan 20, 2026 by cameronfreer Contributor Loading…
2 tasks done
3
ProTip! Add no:assignee to see everything that’s not assigned.