Skip to content

Pull requests: leanprover-community/physlib

New pull request New
51 Open 1,475 Closed
51 Open 1,475 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: lift angular momentum to Hilbert space awaiting-author A reviewer has asked the author a question or requested changes medium t-quantum-mechanics Quantum mechanics
#1673 opened Sep 22, 2026 by lizr-phys Contributor Loading…
4
feat(ProbabilisticTheory): state separation blocked-by-PR This PR depends on another PR large
#1672 opened Sep 20, 2026 by TomOleDiem Contributor Loading…
1
feat(ProbabilisticTheory): states blocked-by-PR This PR depends on another PR large
#1671 opened Sep 20, 2026 by TomOleDiem Contributor Loading…
1
feat(ProbabilisticTheory): channels and weights blocked-by-PR This PR depends on another PR large
#1670 opened Sep 20, 2026 by TomOleDiem Contributor Loading…
1
feat(ProbabilisticTheory): effects blocked-by-PR This PR depends on another PR large
#1668 opened Sep 20, 2026 by TomOleDiem Contributor Loading…
1
feat(ProbabilisticTheory): order-unit spaces large review-claimed
#1667 opened Sep 20, 2026 by TomOleDiem Contributor Loading…
@morrison-daniel
4
feat(QuantumMechanics): Hamiltonian and related operators of the Pöschl-Teller system medium review-claimed t-quantum-mechanics Quantum mechanics
#1651 opened Sep 11, 2026 by KevorkianPhilippe Contributor Loading…
@nateabr
4
feat(QuantumMechanics): Rydberg formula and spectral series of the hydrogen atom medium t-quantum-mechanics Quantum mechanics
#1648 opened Sep 11, 2026 by KevorkianPhilippe Contributor Loading…
@gloges
22
feat(QuantumMechanics): ladder operators on the harmonic oscillator eigenstates, eigenvalue equation blocked-by-PR This PR depends on another PR large review-claimed t-quantum-mechanics Quantum mechanics
#1646 opened Sep 11, 2026 by KevorkianPhilippe Contributor Loading…
@jstoobysmith
4
feat(Cosmology): conformal time, conformal Hubble factor and the Friedmann equations in conformal time blocked-by-PR This PR depends on another PR large t-cosmology Cosmology
#1641 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
1
feat(Cosmology): lookback time, luminosity and angular-diameter distances, Etherington, low-redshift coefficients blocked-by-PR This PR depends on another PR large t-cosmology Cosmology
#1640 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
1
feat(Cosmology): comoving distance, redshift, Hubble-Lemaitre law, transverse distance and horizons blocked-by-PR This PR depends on another PR large t-cosmology Cosmology
#1639 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
1
feat(Cosmology): energy conditions, acceleration criterion, deceleration parameter, eternal expansion and Big-Bang bound blocked-by-PR This PR depends on another PR large t-cosmology Cosmology
#1638 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
1
feat(Cosmology): density parameters, closure relation, reduced Hubble function and age blocked-by-PR This PR depends on another PR large t-cosmology Cosmology
#1637 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
1
feat(Cosmology): barotropic equation of state, density scaling laws, cosmological constant as a fluid blocked-by-PR This PR depends on another PR medium t-cosmology Cosmology
#1636 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
1
feat(Cosmology): continuity equation of the cosmic fluid from the Friedmann equations blocked-by-PR This PR depends on another PR medium t-cosmology Cosmology
#1635 opened Sep 10, 2026 by KevorkianPhilippe Contributor Loading…
@doxtor6
19
refactor(OperatorAlgebra): Implement states in more Mathlib-aligned style (RFC) large t-quantum-mechanics Quantum mechanics
#1602 opened Sep 1, 2026 by goliath-klein • Draft
3
docs: Add API map prompt small
#1597 opened Aug 31, 2026 by jstoobysmith Member Loading…
2
feat(QuantumInfo): Robertson uncertainty relation for mixed states medium t-measurements-qi
#1587 opened Aug 29, 2026 by naype888-cloud Contributor Loading…
22
QuantumInfo: StdBasis refactor awaiting-author A reviewer has asked the author a question or requested changes large
#1578 opened Aug 24, 2026 by Timeroot Collaborator Loading…
9
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…
8
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
ProTip! Mix and match filters to narrow down what you’re looking for.