Skip to content

Pull requests: leanprover-community/physlib

New pull request New
28 Open 944 Closed
28 Open 944 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

feat(ClassicalMechanics/HarmonicOsciallator): a few refactors and a new lemma
#1079 opened May 4, 2026 by Bergschaf Loading…
11
feat(StatMech): prove partition-function analyticity; drop Z-smoothness sorry
#1077 opened May 3, 2026 by dennj Contributor Loading…
feat(MatrixNorm/TraceNorm): trace-norm/SVD/Hölder API
#1076 opened May 3, 2026 by dennj Contributor Loading…
1
feat(HermitianMat/Rpow): prove Lieb-Thirring and trace subadditivity
#1075 opened May 3, 2026 by dennj Contributor Loading…
feat(HermitianMat/Proj): add projector positivity, kernel, and posPart=0 lemmas
#1074 opened May 2, 2026 by dennj Contributor Loading…
3
feat(Entropy): prove sandwiched Rényi DPI; remove axiom
#1073 opened May 2, 2026 by dennj Contributor Loading…
feat(QM): Adds radius unbounded operators awaiting-author A reviewer has asked the author a question or requested changes t-quantum-mechanics Quantum mechanics
#1072 opened May 2, 2026 by gloges Contributor Loading…
5
feat(QuantumInfo): close sorries and proof_wanted across foundation and capacity
#1070 opened May 1, 2026 by dennj Contributor Loading…
feat: Basic field strength equalities ready-to-merge This PR is approved and will be merged shortly t-electromagnetism Electromagnetism
#1068 opened May 1, 2026 by jstoobysmith Member Loading…
7
feat(CPTPMap): close 6 sorries around piProd
#1067 opened Apr 30, 2026 by dennj Contributor Loading…
3
feat(QuantumInfo): discharge sorries in ClassicalInfo.Capacity and Regularized
#1066 opened Apr 30, 2026 by dennj Contributor Loading…
2
feat: Start split of Distributional EM RFC Request for comment t-electromagnetism Electromagnetism
#1063 opened Apr 28, 2026 by jstoobysmith Member Loading…
7
fix: Initial Commit for Orbital Mechanics, Vis Viva Version 2
#1057 opened Apr 22, 2026 by hannxmarie Loading…
5
refactor: Separate Vector.Basic & CoVector.Basic RFC Request for comment t-relativity Relativity
#1050 opened Apr 21, 2026 by jstoobysmith Member Loading…
3
Rename and split QED anomaly cancellation plane definitions for clarity
#1047 opened Apr 20, 2026 by Copilot AI • Draft
1
@jstoobysmith
52
Add the core LocalJet coordinate object awaiting-author A reviewer has asked the author a question or requested changes
#1039 opened Apr 15, 2026 by juanjfndz Contributor • Draft
4
feat(Regularized): prove to_SupRegularized and of_Subadditive awaiting-author A reviewer has asked the author a question or requested changes
#1022 opened Apr 5, 2026 by pitmonticone Member Loading…
2
feat: Move variational calculus RFC Request for comment
#1018 opened Apr 1, 2026 by jstoobysmith Member Loading…
1
feat: Adds a diffeormorphism for the harmonic oscillator awaiting-author A reviewer has asked the author a question or requested changes
#1004 opened Mar 25, 2026 by jstoobysmith Member Loading…
3
feat(LaplaceRungeLenzVector): prove angularMomentum_commutation_lrl awaiting-author A reviewer has asked the author a question or requested changes
#991 opened Mar 14, 2026 by pitmonticone Member Loading…
10
feat(temperature): PositiveTemperature refactor t-thermodynamics Thermodynamics
#976 opened Mar 5, 2026 by ichxorya Contributor • Draft
41
feat(Pseudo-Riemannian/Lorentzian): major refactor / add Lorentzian metric
#968 opened Mar 3, 2026 by or4nge19 Collaborator Loading…
2
feat(SolidSphere): prove solidSphere_inertiaTensor awaiting-author A reviewer has asked the author a question or requested changes
#962 opened Feb 25, 2026 by pitmonticone Member Loading…
5
feat: Static EM awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master t-electromagnetism Electromagnetism
#953 opened Feb 19, 2026 by jstoobysmith Member Loading…
6
Initial IdealFluid structure awaiting-author A reviewer has asked the author a question or requested changes
#949 opened Feb 16, 2026 by mog1el • Draft
9 tasks done
7
ProTip! Follow long discussions with comments:>50.