Skip to content

Pull requests: leanprover-community/physlib

New pull request New
29 Open 1,128 Closed
29 Open 1,128 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

auto-task(quantumCapacity): minimize imports of QuantumInfo/Capacity/Capacity.lean
#1270 opened Jun 25, 2026 by jstoobysmith Member Loading…
1
refactor: PermCond -> IsReindexing
#1269 opened Jun 25, 2026 by jstoobysmith Member Loading…
1
auto-task(Time): add API-map.yaml tracking the Time API
#1268 opened Jun 25, 2026 by jstoobysmith Member Loading…
1
auto-task(CanonicalEnsemble): add API-map.yaml tracking the canonical ensemble API
#1266 opened Jun 25, 2026 by doxtor6 Contributor Loading…
3
refactor: golf Physlib proofs (CKM rows; ongoing)
#1263 opened Jun 25, 2026 by Vilin97 • Draft
1
feat: Adding Additive Structure for ElectromagneticPotential awaiting-author A reviewer has asked the author a question or requested changes
#1256 opened Jun 24, 2026 by NicolaBernini Contributor Loading…
2
refactor: Add Contractions in terms of representations t-relativity Relativity
#1253 opened Jun 24, 2026 by jstoobysmith Member Loading…
1
chore(QuantumInfo): clear 56 files from the linter exemption list
#1244 opened Jun 24, 2026 by tracyphasespace Contributor Loading…
3
Susy n1 conj foundation awaiting-author A reviewer has asked the author a question or requested changes
#1223 opened Jun 22, 2026 by pariandrea Contributor Loading…
25
feat(meta): add agent-review rubric and example GitHub Action
#1209 opened Jun 19, 2026 by jfindlay Contributor • Draft
9
feat: gamma anticommutator and slash of Lorentz vector awaiting-author A reviewer has asked the author a question or requested changes
#1206 opened Jun 18, 2026 by wdconinc Contributor Loading…
21
feat(QuantumInfo): angle-parameterized qubit ket for Pancharatnam connection awaiting-author A reviewer has asked the author a question or requested changes
#1139 opened Jun 2, 2026 by wock9000 Contributor Loading…
1
feat(FluidDynamics): Adding more fluid dynamics - continuation of PR #949 and #1112 , awaiting-author A reviewer has asked the author a question or requested changes
#1125 opened May 26, 2026 by FloWsnr Contributor Loading…
42
feat(Mathematics): add Physlib/Mathematics/GoldenRatio.lean awaiting-author A reviewer has asked the author a question or requested changes
#1122 opened May 23, 2026 by gHashTag Loading…
4
feat(SpaceAndTime): first-step GalileanGroup API (data type and coordinate action) awaiting-author A reviewer has asked the author a question or requested changes
#1116 opened May 21, 2026 by MaxwellLaw Loading…
5 tasks done
10
feat: Other implementation RFC Request for comment
#1111 opened May 20, 2026 by jstoobysmith Member Loading…
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 Contributor Loading…
@jstoobysmith
22
feat(AxiomatizedEntropy): expand RelEntropy API and add Hellinger overlap awaiting-author A reviewer has asked the author a question or requested changes
#1098 opened May 13, 2026 by dennj Contributor Loading…
6
feat(QuantumMechanics): add Canonical commutation on the Schwartz submodule awaiting-author A reviewer has asked the author a question or requested changes blocked-by-PR This PR depends on another PR t-quantum-mechanics Quantum mechanics
#1096 opened May 13, 2026 by or4nge19 Collaborator Loading…
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: 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…
4
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 awaiting-author A reviewer has asked the author a question or requested changes t-thermodynamics Thermodynamics
#976 opened Mar 5, 2026 by ichxorya Contributor • Draft
42
feat(Pseudo-Riemannian/Lorentzian): major refactor / add Lorentzian metric awaiting-author A reviewer has asked the author a question or requested changes
#968 opened Mar 3, 2026 by or4nge19 Collaborator Loading…
2
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.