Skip to content

Pull requests: leanprover-community/physlib

New pull request New
43 Open 1,396 Closed
43 Open 1,396 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(Units): reducible rational arithmetic via Exponent awaiting-author A reviewer has asked the author a question or requested changes large t-units Units
#1579 opened Aug 25, 2026 by RaunakChhatwal Contributor Loading…
7
QuantumInfo: StdBasis refactor large
#1578 opened Aug 24, 2026 by Timeroot Collaborator Loading…
1
States, expectation, and uncertainty relations awaiting-author A reviewer has asked the author a question or requested changes medium t-quantum-mechanics Quantum mechanics
#1577 opened Aug 24, 2026 by TomOleDiem Contributor Loading…
12
feat(ClassicalMechanics): SimplePendulum.periodFormula, the classical amplitude-dependent period blocked-by-PR This PR depends on another PR large
#1576 opened Aug 24, 2026 by aadarwal Contributor Loading…
3
feat(ClassicalMechanics): existence and uniqueness for the nonlinear simple pendulum blocked-by-PR This PR depends on another PR large
#1575 opened Aug 24, 2026 by aadarwal Contributor Loading…
1
refactor(Time): general lemmas for the time derivative under reparametrisation and reflection blocked-by-PR This PR depends on another PR medium
#1574 opened Aug 24, 2026 by aadarwal Contributor Loading…
1
feat(ClassicalMechanics): the small-angle regime of the simple pendulum as a harmonic oscillator blocked-by-PR This PR depends on another PR large
#1572 opened Aug 23, 2026 by aadarwal Contributor Loading…
1
feat(ClassicalMechanics): pendulum trajectories on the configuration circle and the bridge to physical space blocked-by-PR This PR depends on another PR large
#1571 opened Aug 23, 2026 by aadarwal Contributor Loading…
1
feat(ClassicalMechanics): Hamiltonian formulation of the simple pendulum and the equivalence of formulations medium
#1570 opened Aug 23, 2026 by aadarwal Contributor Loading…
@nateabr
11
feat(pauli): prove the epsilon triple-product identities medium t-relativity Relativity
#1568 opened Aug 23, 2026 by Robby955 Contributor Loading…
19
feat(tensors): prove the Levi-Civita contraction identities awaiting-author A reviewer has asked the author a question or requested changes large t-relativity Relativity
#1565 opened Aug 22, 2026 by Robby955 Contributor Loading…
25
auto-task(OperatorAlgebra): add API-map.yaml for the observable-algebra API awaiting-author A reviewer has asked the author a question or requested changes small
#1555 opened Aug 20, 2026 by Alex-Zughaid Contributor Loading…
2
feat(PhyslibAlpha): Add results of 2606.13889 to PhyslibAlpha as informal lemmas awaiting-author A reviewer has asked the author a question or requested changes PhyslibAlpha Pull requests which are for modifications to PhyslibAlpha.
#1461 opened Jul 24, 2026 by jstoobysmith Member Loading…
1
feat: Added PR template awaiting-author A reviewer has asked the author a question or requested changes
#1458 opened Jul 22, 2026 by Alex-Zughaid Contributor Loading…
1 of 3 tasks
1
@jstoobysmith
2
feat(QuantumMechanics): derivative operators via Fourier-conjugated m… awaiting-author A reviewer has asked the author a question or requested changes t-quantum-mechanics Quantum mechanics
#1454 opened Jul 21, 2026 by adambornemann-glitch Contributor Loading…
@gloges
16
feat: Github actions workflow to send a message to Zulip thread CI
#1453 opened Jul 21, 2026 by Alex-Zughaid Contributor Loading…
@jstoobysmith
1
feat: Add API map for the SM awaiting-author A reviewer has asked the author a question or requested changes t-particles Particles
#1419 opened Jul 14, 2026 by jstoobysmith Member Loading…
4
feat: Effective potential for Weyl fermions (Stacked on #1404) blocked-by-PR This PR depends on another PR large
#1415 opened Jul 13, 2026 by jstoobysmith Member • Draft
5
feat(PhyslibAlpha): QuantumThermodynamics — thermal state, Landauer bound, area API-map
#1409 opened Jul 10, 2026 by fliingelephant • Draft
6
refactor: Golf Quantum info with fable awaiting-author A reviewer has asked the author a question or requested changes
#1403 opened Jul 9, 2026 by jstoobysmith Member • Draft
1
refactor: golf proofs in HarmonicOscillator, IsExtrema, TotalDerivativeEquivalence, KineticTerm
#1373 opened Jul 6, 2026 by Vilin97 Contributor • Draft
1
feat(Thermodynamics): add foundational API awaiting-author A reviewer has asked the author a question or requested changes RFC Request for comment t-thermodynamics Thermodynamics
#1365 opened Jul 4, 2026 by nateabr Collaborator Loading…
26
feat: Add DropPair ProdP commutation lemma for one orientation awaiting-author A reviewer has asked the author a question or requested changes
#1345 opened Jul 1, 2026 by NicolaBernini Collaborator Loading…
5
auto-task(EffectivePotential): TODO to make Higgs potential polynomial basis-independent awaiting-author A reviewer has asked the author a question or requested changes
#1321 opened Jun 29, 2026 by jstoobysmith Member Loading…
@morrison-daniel
2
feat: Refactor downstream use away from FieldStrengthMatrix awaiting-author A reviewer has asked the author a question or requested changes
#1288 opened Jun 26, 2026 by NicolaBernini Collaborator Loading…
6
ProTip! Exclude everything labeled bug with -label:bug.