Search results

Style lint technical debt

Status: Open.

#1180 In leanprover-community/physlib;

· jfindlay opened on Jun 12, 2026

fix defsWithUnderscore linter

Status: Open.

#1147 In leanprover-community/physlib;

· zhikaip opened on Jun 4, 2026

Removing pre-Lorentz vectors Co, Contr etc.

Status: Open.

#1048 In leanprover-community/physlib;

· jstoobysmith opened on Apr 21, 2026

Naming in Anomaly Cancellation for QED

help-wantedExtra attention is needed Extra attention is needed

Status: Open.

#1046 In leanprover-community/physlib;

· jstoobysmith opened on Apr 20, 2026

Technical debt counter

Status: Open.

#1038 In leanprover-community/physlib;

· jstoobysmith opened on Apr 15, 2026

API: Spatial Surfaces

API

help-wantedExtra attention is needed Extra attention is needed

Status: Open.

#943 In leanprover-community/physlib;

· jstoobysmith opened on Feb 13, 2026

API: TimeAndSpace

API

Status: Open.

#939 In leanprover-community/physlib;

· jstoobysmith opened on Feb 13, 2026

API: Integrate Glimm-Jaffe AQFT Framework into PhysLean

Status: Open.

#938 In leanprover-community/physlib;

· or4nge19 opened on Feb 12, 2026

API: Galilean group

API

help-wantedExtra attention is needed Extra attention is needed

Status: Open.

#911 In leanprover-community/physlib;

· jstoobysmith opened on Jan 16, 2026

API: Time Manifold

API

help-wantedExtra attention is needed Extra attention is needed

Status: Open.

#909 In leanprover-community/physlib;

· jstoobysmith opened on Jan 15, 2026

API: Tensors

API

help-wantedExtra attention is needed Extra attention is needed

requirements-neededUsed for API issues where the requirements of the API need to be specified Used for API issues where the requirements of the API need to be specified

Status: Open.

#908 In leanprover-community/physlib;

· jstoobysmith opened on Jan 15, 2026

API: Dirac Fermions

API

help-wantedExtra attention is needed Extra attention is needed

requirements-neededUsed for API issues where the requirements of the API need to be specified Used for API issues where the requirements of the API need to be specified

Status: Open.

#907 In leanprover-community/physlib;

· jstoobysmith opened on Jan 14, 2026