Issues

• Hamiltonian dynamics extensions

  leanprover-community/physlib#1893 · Filter by author artmountain opened on Oct 20, 2026

• Update the Units directory structure.

  leanprover-community/physlib#1892 · Filter by author jstoobysmith opened on Oct 20, 2026

• Improve Physics documentation (API maps)

  good first issuehelp-wanted
  leanprover-community/physlib#1891 · Filter by author jstoobysmith opened on Oct 20, 2026

• Rename Distributions and add new file for ordinary distributions

  leanprover-community/physlib#1737 · Filter by author Camkhlee opened on Oct 5, 2026
  2

• Add analytic structures for WithDim

  leanprover-community/physlib#1628 · Filter by author catlover-bot opened on Sep 10, 2026
  1

• Add documentation linters to PhyslibAlpha.

  leanprover-community/physlib#1595 · Filter by author jstoobysmith opened on Aug 31, 2026

• TODOs with Line numbers

  leanprover-community/physlib#1594 · Filter by author jstoobysmith opened on Aug 31, 2026
  2

• Documentation typo in tensor product example refers to undefined T1 instead

  good first issuehelp-wanted
  leanprover-community/physlib#1543 · Filter by author Alex-Zughaid opened on Aug 17, 2026
  1

• Incorrect symbol 𝓢 used in documentation of

  good first issuehelp-wanted
  leanprover-community/physlib#1542 · Filter by author Alex-Zughaid opened on Aug 17, 2026
  1

• Incorrect documentation for realLorentzTensor in Basic.lean

  good first issuehelp-wanted
  leanprover-community/physlib#1538 · Filter by author Alex-Zughaid opened on Aug 17, 2026

• Documentation claims support for RHNs in MSSM but code does not implement them

  good first issuehelp-wanted
  leanprover-community/physlib#1535 · Filter by author Alex-Zughaid opened on Aug 17, 2026
  1

• Incorrect 'complex' documentation for real Lorentz tensors in Metrics/Basic.lean

  good first issuehelp-wanted
  leanprover-community/physlib#1532 · Filter by author Alex-Zughaid opened on Aug 17, 2026

• Incorrect initialization of S in ZModCharges definition

  good first issuehelp-wanted
  leanprover-community/physlib#1528 · Filter by author Alex-Zughaid opened on Aug 17, 2026
  1

• Repo needs a PR template

  leanprover-community/physlib#1457 · Filter by author Alex-Zughaid opened on Jul 22, 2026

• AI task runner

  leanprover-community/physlib#1211 · Filter by author jstoobysmith opened on Jun 19, 2026
  3

  

• Style lint technical debt

  leanprover-community/physlib#1180 · Filter by author jfindlay opened on Jun 12, 2026

• fix defsWithUnderscore linter

  leanprover-community/physlib#1147 · Filter by author zhikaip opened on Jun 4, 2026

• Removing pre-Lorentz vectors Co, Contr etc.

  leanprover-community/physlib#1048 · Filter by author jstoobysmith opened on Apr 21, 2026

• Technical debt counter

  leanprover-community/physlib#1038 · Filter by author jstoobysmith opened on Apr 15, 2026

• Lorentz algebra and Lorentz Group

  leanprover-community/physlib#833 · Filter by author jstoobysmith opened on Dec 13, 2025
  4

• Thoughts on the definition of Hilbert Space and Bra-Ket

  leanprover-community/physlib#797 · Filter by author xwang204-bkl opened on Nov 3, 2025
  3

• PhysLean.ClassicalMechanics.HarmonicOscillator.Basic

  leanprover-community/physlib#738 · Filter by author jstoobysmith opened on Sep 12, 2025
  3

• PhysLean.Electromagnetism.Electrostatics.Basic

  leanprover-community/physlib#723 · Filter by author jstoobysmith opened on Aug 29, 2025
  1

• Module doc-string improvements

  leanprover-community/physlib#713 · Filter by author jstoobysmith opened on Aug 26, 2025
  3

• Improving on-boarding documentation

  leanprover-community/physlib#700 · Filter by author jstoobysmith opened on Aug 20, 2025