Skip to content

Pull requests: leanprover-community/physlib

New pull request New
31 Open 984 Closed
31 Open 984 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(Mathematics): add Physlib/Mathematics/GoldenRatio.lean
#1122 opened May 23, 2026 by gHashTag Loading…
1
feat(QuantumInfo): Bargmann invariant and geometric phase
#1121 opened May 23, 2026 by wock9000 Loading…
10
feat(QM): Add LinearPMap.sum t-quantum-mechanics Quantum mechanics
#1120 opened May 23, 2026 by gloges Contributor Loading…
1
feat: Constructive form of curl zero eq grad t-space-time Space and time
#1119 opened May 22, 2026 by jstoobysmith Member Loading…
1
feat: Turn on and modify PR message t-meta Meta
#1117 opened May 22, 2026 by jstoobysmith Member Loading…
1
feat(SpaceAndTime): first-step GalileanGroup API (data type and coordinate action)
#1116 opened May 21, 2026 by MaxwellLaw Loading…
5 tasks done
10
feat(SUSY/N1): add chiral scalar configuration space and coordinate CLMs
#1113 opened May 20, 2026 by pariandrea Loading…
@jstoobysmith
4
feat(FluidDynamics): add Navier-Stokes conservative and convective forms
#1112 opened May 20, 2026 by FloWsnr Contributor Loading…
36
feat: Other implementation
#1111 opened May 20, 2026 by jstoobysmith Member • Draft
feat(QuantumMechanics): sudden frequency change for the QHO
#1109 opened May 19, 2026 by casualPhysics Collaborator Loading…
6 tasks done
feat: Wirtinger calculus and N=1 SUSY scalar Wirtinger derivatives
#1107 opened May 18, 2026 by pariandrea Loading…
@jstoobysmith
22
feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap
#1098 opened May 13, 2026 by dennj Contributor Loading…
4
feat(Tensors): PermCond.snoc PermCond.succAbove ready-to-merge This PR is approved and will be merged shortly t-relativity Relativity
#1097 opened May 13, 2026 by jstoobysmith Member Loading…
@morrison-daniel
3
feat(QuantumMechanics): add Canonical commutation on the Schwartz submodule blocked-by-PR This PR depends on another PR t-quantum-mechanics Quantum mechanics
#1096 opened May 13, 2026 by or4nge19 Collaborator Loading…
15
feat(QuantumMechanics): Uncertainty bounds for partial linear maps t-quantum-mechanics Quantum mechanics
#1095 opened May 13, 2026 by or4nge19 Collaborator Loading…
@jstoobysmith
16
feat(Entropy): prove sandwiched Rényi DPI; remove axiom awaiting-author A reviewer has asked the author a question or requested changes
#1073 opened May 2, 2026 by dennj Contributor Loading…
5
feat: Start split of Distributional EM RFC Request for comment t-electromagnetism Electromagnetism
#1063 opened Apr 28, 2026 by jstoobysmith Member Loading…
7
refactor: Separate Vector.Basic & CoVector.Basic awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master 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 bounded derivative indices awaiting-author A reviewer has asked the author a question or requested changes
#1039 opened Apr 15, 2026 by juanjfndz Contributor • Draft
8
feat: Move variational calculus merge-conflict The PR has a merge conflict with master 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
ProTip! Updated in the last three days: updated:>2026-05-21.