Pith

open record

sign in

arxiv: 2607.06379 · v1 · pith:ZJI4SAUU · submitted 2026-07-07 · hep-th · cs.LO

Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean

Michael R. Douglas This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 reserved 2026-07-08 07:41 UTCglm-5.2pith:ZJI4SAUUrecord.jsonopen to challenge →

classification hep-th cs.LO MSC 14D0781T6068V20 PACS 11.15.-q11.30.Pb12.60.Jv
keywords Seiberg-Witteninteractive theorem provingLean 4formalization of physicsN=2 supersymmetrySU(2) super-Yang-Millsmodular lambda functionGamma(2) duality
0
0 comments X

The pith

Physics without proofs: machine-checking the Seiberg-Witten solution

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper demonstrates that a celebrated physics result with no rigorous proof — the Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills — can be formalized in the Lean 4 proof assistant by separating it into two layers: a short list of named physical postulates (H0-H7) and machine-checked mathematical theorems that derive the physical consequences from those postulates. The key architectural decision is that physical assumptions live as predicates carried in theorem types, never as global axioms, so the #print axioms command can report exactly which inputs any downstream result depends on. For the genus-one SU(2) case, the paper constructs the effective coupling tau(u) = iK'/K at the curve's modulus, proves it exists on an open chart, and proves it is unique up to a Gamma(2) duality frame — all as sorry-free theorems resting on exactly three logical axioms plus two classical covering-space facts, with no physical input hidden in the mathematical base.

Core claim

The central mechanism is the strict separation of trust: physical postulates become named, inspectable predicates (H0-H7) carried in theorem signatures, while mathematical consequences are proved by the Lean kernel. The headline theorem — uniqueness of the SU(2) effective coupling up to a Gamma(2) duality frame — is machine-certified to depend on nothing beyond standard logic plus two classical facts about the modular lambda covering H/Gamma(2) ≅ C∖{0,1} and lift rigidity. The physical input enters only through the definition SameSWMonodromy (a predicate, not an axiom), so #print axioms confirms the trusted base contains zero physics. The paper also shows that several phenomena previously看来d

What carries the argument

The Lean 4 proof assistant, the #print axioms audit command, and the Gamma(2) modular covering of the thrice-punctured sphere.

If this is right

  • Any trusted-but-unproved physics argument can in principle be formalized this way: state the physical assumptions as named predicates, prove the mathematical spine, and let the kernel certify the dependency chain. The residual trust localizes onto a finite, inspectable list rather than a diffuse narrative.
  • For AI-generated physics derivations, this discipline directly addresses the characteristic failure mode of hallucinated assumptions: if every physical input must be a named predicate in a theorem type, a dropped subtlety or unphysical premise becomes visible to audit rather than hidden in prose.
  • The approach generalizes beyond Seiberg-Witten: the paper sketches a tiered programme where some physical postulates (the BPS bound, Dirac quantization) are themselves theorems in disguise, formalizable to push the assumed frontier deeper. The BPS bound reduces to finite-dimensional linear algebra over the extended N=2 algebra; the Dirac pairing reduces to angular-momentum quantization.
  • The higher-genus SU(N) case is reduced to a single consolidated mathematical debt — the variation of Hodge structure (Gauss-Manin connection with Sp(2r,Z) monodromy) of the SW curve family — making the remaining work a precise, prioritized theorem rather than an open-ended physics problem.
  • The singularity count theorem shows that monodromy data plus the anomaly grading (from R-spurion covariance, H7) together pin exactly two singular points, while neither ingredient alone suffices — a division of labor the formalization makes exact and machine-verified.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the method scales to other non-rigorous but trusted results in quantum field theory (e.g., dualities, confinement arguments, anomaly-matching constraints), it could create a new publication standard where physics papers ship with a formalized dependency audit alongside the prose, making the boundary between derived and assumed fully explicit.
  • The numerical oracle validation protocol — 278 checks at 30-40 digit precision in a codebase sharing no authorship with the Lean — suggests a generalizable two-layer validation pattern: machine-check logical structure, numerically check analytic content, and treat agreement as the empirical anchor for the physical axioms.
  • The discovery that several hypotheses were initially vacuously true (H3, H6) or unsatisfiable (H5 at rank 1) when formalized suggests that much physics prose may contain similar hidden vacuities — formalization could surface these across the field, not just for Seiberg-Witten.

Load-bearing premise

The uniqueness theorem for the SU(2) coupling depends on two classical but unproved-in-Lean facts: that the modular lambda function realizes the covering of the thrice-punctured sphere by the upper half-plane modulo Gamma(2), and that two lifts through this covering agree up to a deck transformation. If either covering fact were wrong, the uniqueness argument would collapse.

What would settle it

Construct two candidate effective couplings for SU(2) that both develop the SW modulus but disagree beyond a Gamma(2) frame change, or show that the Gamma(2) covering does not have the rigidity the lift-uniqueness axiom asserts.

read the original abstract

Mathematicians have embraced interactive theorem provers with growing enthusiasm -- building large shared libraries and machine-checking a string of landmark results. Theoretical physics is different: most of its results are not theorems but justified by arguments the community trusts without a rigorous proof. For many -- the one we treat here among them -- no rigorous proof is within reach. For 4d Yang--Mills theory, deriving exact rigorous results from first principles would first require constructing the interacting theory nonperturbatively, which is a sizable piece of one of the Clay Millennium prize problems. We argue here that an interactive theorem prover can be used to verify some non-rigorous physics arguments. The method is to postulate a short list of explicit, named physical postulates, which imply the physical results by virtue of a machine-checkable proof. The trust that remains then rests on that short, inspectable list, and the prover can report, for any downstream result, exactly which assumptions it used. We carry this out for the Seiberg--Witten solution of ${N}=2$ $SU(2)$ super-Yang--Mills -- the genus-one case -- formalized in Lean 4; the higher-genus $SU(N)$ generalization is developed in the same repository as an axiomatized skeleton and left to future work. We describe what is proved, what is assumed, how the assumptions are checked -- external review and an independent numerical oracle -- and why this discipline is a sound standard for validating AI-generated results in theoretical physics. What we offer is a discipline, reviewable on its own terms: a reader may take the Seiberg--Witten mathematics on trust and still assess the formalization method.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 6 minor

Summary. This paper proposes a formalization discipline for non-rigorous physics arguments using the Lean 4 proof assistant, applied to the Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills. The core methodological claim is that physical input can be isolated as named predicates (H0-H7) carried in theorem types, while all mathematical consequences are machine-checked sorry-free theorems. The headline result is the existence and uniqueness of the effective coupling up to a Gamma(2) duality frame, certified by #print axioms to rest on exactly three logical axioms plus two classical covering facts. The paper documents the math-physics dictionary, the axiom ledger, validation via numerical oracle and adversarial review, and remaining mathematical debt including the higher-genus SU(N) skeleton.

Significance. The paper makes a genuine methodological contribution by demonstrating how interactive theorem provers can audit non-rigorous physics arguments, isolating physical assumptions into inspectable named predicates while proving all mathematical consequences. The sorry-free Lean formalization with #print axioms certification is a concrete strength, as is the explicit documentation of vacuity catches (Section 4.4) and the numerical oracle validation (Section 5). The discipline proposed is timely given the stated motivation of validating AI-generated physics results. The Seiberg-Witten solution is a well-chosen test case: physically certain, mathematically precise, and unprovable from first principles.

major comments (3)
  1. Section 4.3 and Appendix B.2: The central methodological claim is that physical input enters only through H0-H7, with all mathematical consequences proved. The uniqueness theorem sw_su2_unique takes SameSWMonodromy as a hypothesis. The paper states (Section 4.3) that SameSWMonodromy is 'a definition, not a postulate' and that the developing condition lambda(tau(u)) = 2Lambda^2/(u+Lambda^2) is derived from H0-H7 via two intermediate theorems: swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio. However, the #print axioms output is shown only for sw_su2_unique (the final step), not for these intermediate derivation theorems. Without seeing #print axioms for swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio, the reader cannot verify from the manuscript alone that these intermediate theorems take only H0-H7 as physical hypotheses and do not themselves assume the结论
  2. Section 4.3, Appendix B.2: The skeptic's concern about whether swModulusData_of_atlas_and_lifts genuinely derives single-valuedness of lambda composed with tau from H0-H7, or whether it assumes single-valuedness as a hypothesis, is load-bearing. If single-valuedness is assumed rather than derived, then SameSWMonodromy effectively smuggles in a condition stronger than H0-H7. The paper's prose describes the derivation ('descent through the proved Gamma(2)-invariance, plus a removable-singularity dichotomy; no Picard theorems') but the Lean statement of this theorem is not shown in the manuscript. The authors should include the Lean signatures of both intermediate theorems (or their #print axioms output) so that the reader can confirm the chain H0-H7 -> developing condition -> uniqueness is complete.
  3. Repository accessibility: The manuscript references 'mrdouglas/seiberg-witten' (footnote, page 1) but does not provide a commit hash or DOI. Given that the paper's central claims depend on machine-checked proofs whose statements are only partially reproduced in the manuscript, a pinned repository reference is essential for reproducibility and peer review. Without it, neither the #print axioms output nor the intermediate theorem statements can be independently verified.
minor comments (6)
  1. Section 4.2, H7 description: The statement about the Witten-effect frame shift 'F -> F + 1/2 a^T B a with B an integer symmetric matrix constant across the family' could benefit from a reference to the specific physics literature where this form of the shift is discussed.
  2. Section 4.3: The phrase 'footprint standard-3' is used repeatedly but its precise meaning (three logical axioms: propext, Classical.choice, Quot.sound) is defined only implicitly. A brief explicit definition at first use would improve readability.
  3. Appendix A, H6 definition: The Instantonic predicate includes a weighted-homogeneity clause but the connection to the Lambda-independence discussion in Section 4.4 could be made more explicit in the code comments.
  4. Section 5: The numerical oracle is described as using 'mpmath / numpy' at '30-40-digit precision.' A brief mention of the specific convergence criteria or tolerance thresholds used for the 278 checks would strengthen the reproducibility of the validation.
  5. Section 6: The statement 'A first version was caught (adversarial review) asserting a single globally-constant SL(2,Z) frame across a possibly-disconnected overlap' is attributed to adversarial review but the nature of this review process (human, AI-assisted, or both) is not specified.
  6. References: The arXiv identifier for reference [15] (Krippendorf and Tooby-Smith) appears to be 2603.28406, which seems to be a 2026 preprint; this should be verified.

Simulated Author's Rebuttal

3 responses · 0 unresolved

The referee raises three points: (1) #print axioms output for intermediate theorems swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio is not shown, (2) Lean signatures of these intermediate theorems are not included so the reader cannot verify the derivation chain H0-H7 -> developing condition -> uniqueness is complete, and (3) the repository reference lacks a commit hash or DOI. All three are legitimate reproducibility concerns that we will address in revision.

read point-by-point responses

  1. Referee: Section 4.3 and Appendix B.2: #print axioms output is shown only for sw_su2_unique, not for intermediate theorems swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio. The reader cannot verify these intermediate theorems take only H0-H7 as physical hypotheses.

    Authors: The referee is correct. The manuscript shows #print axioms only for the final uniqueness theorem sw_su2_unique, but the methodological claim that physical input enters only through H0-H7 requires the same audit for every intermediate theorem in the derivation chain. We will add #print axioms output for both swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio to Appendix B.2 (or Section 4.3, space permitting). We expect both to report footprint standard-3 (the three logical axioms only), since these theorems derive the developing condition from the atlas and cusp-lift data using purely mathematical reasoning — no physical postulates appear in their statements. Including the machine output makes the chain H0-H7 -> developing condition -> uniqueness auditable end to end, which is the paper's central methodological claim. revision: yes

  2. Referee: Section 4.3, Appendix B.2: The Lean signatures of swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio are not shown, so the reader cannot confirm that single-valuedness of lambda composed with tau is derived from H0-H7 rather than assumed. If single-valuedness is assumed, SameSWMonodromy smuggles in a condition stronger than H0-H7.

    Authors: This is a fair and load-bearing concern. The skeptic's worry — that SameSWMonodromy might assume single-valuedness rather than deriving it — can only be laid to rest by showing the actual Lean signatures. We will include the full Lean signatures of both swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio in the revised manuscript. The signatures will show that the hypotheses of swModulusData_of_atlas_and_lifts are the atlas structure (IsSWCouplingAtlas, carrying H4) and the cusp-lift data (IsGenuineCuspLift, carrying H2+H3), with single-valuedness of lambda composed with tau appearing in the conclusion, not the hypotheses. The derivation proceeds via proved Gamma(2)-invariance of the modular lambda function and a removable-singularity dichotomy, as the prose describes — but the prose alone is insufficient, and the referee is right to demand the formal statements. We will also add a brief commentary explaining how the signatures connect to the informal argument, so a reader who is not a Lean specialist can follow the logical structure. revision: yes

  3. Referee: Repository accessibility: The manuscript references 'mrdouglas/seiberg-witten' but does not provide a commit hash or DOI. A pinned repository reference is essential for reproducibility and peer review.

    Authors: The referee is correct. Given that the paper's central claims depend on machine-checked proofs whose statements are only partially reproduced in the manuscript, a pinned repository reference is essential. We will add a commit hash (or Zenodo DOI, if preferred by the journal) to the footnote referencing the repository on page 1, and will ensure the pinned commit corresponds to the exact state of the codebase that produces the #print axioms output reported in the paper. We note that the manuscript currently references 'mrdouglasny/seiberg-witten' (the footnote on page 1); we will verify the repository name and provide the pinned reference in the revised version. revision: yes

Circularity Check

0 steps flagged

No significant circularity found; the derivation chain is self-contained against classical mathematics, with only minor non-load-bearing self-citations.

full rationale

The paper's central derivation chain is: (1) physical postulates H0–H7 are defined as Lean predicates carried in theorem types, never as global axioms; (2) the uniqueness theorem sw_su2_unique takes SameSWMonodromy as a hypothesis, which is a *definition* (both candidate couplings develop the SW cross-ratio λ(τ(u)) = 2Λ²/(u+Λ²)); (3) the paper claims this developing condition is itself derived from H0–H7 via two intermediate theorems (swModulusData_of_atlas_and_lifts and swModulusData_eq_crossRatio), stated to have 'standard-3' footprints (only the three logical axioms). The #print axioms output for sw_su2_unique confirms the trusted base is exactly three logical axioms plus two classical covering facts (AX_thrice_punctured_uniformization, AX_developing_map_rigidity), with SameSWMonodromy appearing as a defined hypothesis in the theorem type, not as an axiom. The cross-ratio m(u) = 2Λ²/(u+Λ²) is determined numerically by an independent oracle (branch-tracked quadrature of the curve's periods, tested against six Möbius candidates) and then proved in Lean — the oracle shares no code or authorship with the Lean development. The mathematical axioms are all classical, citable results (Ahlfors, Forster, Whittaker–Watson, Arnol'd) independent of Seiberg–Witten physics. The two self-citations ([10] Douglas 'Foundations of QFT', [11] Douglas et al. 'Formalization of QFT') are contextual references about the formalization methodology, not load-bearing mathematical inputs for the SW derivation. The skeptic's concern — whether SameSWMonodromy is genuinely derived from H0–H7 or smuggles in extra physical content — is a verification question (the paper does not show #print axioms for the intermediate theorems, and no repository commit hash is provided), not a circularity question: the paper's own equations and definitions do not exhibit any input defined in terms of its output. The developing condition is defined in terms of the curve's modulus (a definition), not in terms of the uniqueness conclusion.

Axiom & Free-Parameter Ledger

0 free parameters · 7 axioms · 0 invented entities

No free parameters are fitted to data. No invented entities are postulated. The axioms are all either classical mathematical theorems not yet in Mathlib (covering theory, theta identities, Jacobi inversion, Picard–Lefschetz) or one consolidated domain assumption (periodRigidityAxiom) for the higher-genus skeleton. The physical postulates H0–H7 are predicates in theorem types, not global axioms, so they do not appear in this ledger. The paper is transparent about each axiom's status and source.

axioms (7)
  • standard math AX_thrice_punctured_uniformization
    §B.2. The Γ(2) covering H/Γ(2) ≅ C∖{0,1} exists. Classical theorem (Ahlfors [1], Forster [12]). Not yet in Mathlib. Load-bearing for the SU(2) uniqueness theorem.
  • standard math AX_developing_map_rigidity
    §B.2. Two analytic H-valued lifts with the same λ-image agree near a point up to a Γ(2) deck transformation. Classical covering-space theory (Forster [12]). Load-bearing for uniqueness.
  • standard math AX_jacobi_quartic
    §B.2. θ₃⁴ = θ₂⁴ + θ₄⁴. Corollary of the Jacobi triple product (Whittaker–Watson [27]). Repository proves convergence and functional equation but not the identity itself.
  • standard math AX_theta3_ne_zero
    §B.2. θ₃(τ) ≠ 0. Follows from the Jacobi triple product [27].
  • standard math AX_elliptic_inversion
    §6, §B.2. Jacobi's inversion theorem K = (π/2)θ₃², τ = iK′/K. Whittaker–Watson §§21–22. Not on the footprint of the uniqueness headline but needed for the explicit coupling layer.
  • domain assumption periodRigidityAxiom
    §B.1. The Gauss–Manin / variation-of-Hodge-structure period geometry of the SW curve family exists. Single consolidated axiom for the SU(N) skeleton. Discharge is future work.
  • standard math AX_picard_lefschetz_local
    §B.2. Local monodromy equals the Picard–Lefschetz transvection. Classical (Arnol'd–Guseĭn-Zade–Varchenko [5]).

pith-pipeline@v1.1.0-glm · 24444 in / 2869 out tokens · 484300 ms · 2026-07-08T07:41:58.536023+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages · 15 internal anchors

  1. [1]

    Ahlfors,Complex analysis, 3rd ed., McGraw-Hill, 1979

    Lars V. Ahlfors,Complex analysis, 3rd ed., McGraw-Hill, 1979

    work page 1979

  2. [2]

    New Phenomena in SU(3) Supersymmetric Gauge Theory

    Philip C. Argyres and Michael R. Douglas,New phenomena inSU (3)supersymmetric gauge theory, Nuclear Physics B448(1995), 93–126, arXiv:hep-th/9505062

    work page internal anchor Pith review Pith/arXiv arXiv 1995

  3. [3]

    The Vacuum Structure and Spectrum of N=2 Supersymmetric SU(N) Gauge Theory

    Philip C. Argyres and Alon E. Faraggi,Vacuum structure and spectrum ofN = 2supersymmetric SU (n) gauge theory, Physical Review Letters74(1995), 3931–3934, arXiv:hep-th/9411057

    work page internal anchor Pith review Pith/arXiv arXiv 1995

  4. [4]

    New N=2 Superconformal Field Theories in Four Dimensions

    Philip C. Argyres, M. Ronen Plesser, Nathan Seiberg, and Edward Witten,NewN = 2superconformal field theories in four dimensions, Nuclear Physics B461(1996), 71–84, arXiv:hep-th/9511154

    work page internal anchor Pith review Pith/arXiv arXiv 1996

  5. [5]

    V. I. Arnol’d, S. M. Guse˘ ın-Zade, and A. N. Varchenko,Singularities of differentiable maps. Volume 2: Monodromy and asymptotics of integrals, Birkhäuser, 1988

    work page 1988

  6. [6]

    Mathematics and the formal turn

    Jeremy Avigad,Mathematics and the formal turn, Bulletin of the American Mathematical Society61 (2024), no. 2, 225–240, arXiv:2311.00007

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  7. [7]

    Adel Bilal,Duality in N = 2SUSY SU (2)Yang–Mills theory: A pedagogical introduction to the work of Seiberg and Witten, 1996, arXiv:hep-th/9601007

    work page internal anchor Pith review Pith/arXiv arXiv 1996

  8. [8]

    Alexander Braverman and Pavel Etingof,Instanton counting via affine Lie algebras. II. From Whittaker vectors to the Seiberg–Witten prepotential, Studies in Lie Theory, Progress in Mathematics, vol. 243, Birkhäuser, 2006, arXiv:math/0409441, pp. 61–78

    work page internal anchor Pith review Pith/arXiv arXiv 2006

  9. [9]

    Kevin Buzzard,What is the point of computers? A question for pure mathematicians, Proceedings of the International Congress of Mathematicians 2022, EMS Press, 2023, arXiv:2112.11598

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  10. [10]

    Michael R Douglas,Foundations of quantum field theory, String-Math 2011 (2011), 105–124

    work page 2011

  11. [11]

    Douglas, Sarah Hoback, Anna Mei, and Ron Nissim,Formalization of QFT, March 2026

    Michael R. Douglas, Sarah Hoback, Anna Mei, and Ron Nissim,Formalization of QFT, March 2026

    work page 2026

  12. [12]

    81, Springer, 1981

    Otto Forster,Lectures on Riemann surfaces, Graduate Texts in Mathematics, vol. 81, Springer, 1981

    work page 1981

  13. [13]

    Phillip Griffiths and Joseph Harris,Principles of algebraic geometry, Wiley, 1978

    work page 1978

  14. [14]

    Albrecht Klemm, Wolfgang Lerche, Shimon Yankielowicz, and Stefan Theisen,Simple singularities and N = 2supersymmetric Yang–Mills theory, Physics Letters B344(1995), 169–175, arXiv:hep-th/9411048

    work page internal anchor Pith review Pith/arXiv arXiv 1995

  15. [15]

    Sven Krippendorf and Joseph Tooby-Smith,Physics as code: From scans to theorems with ITP APIs in SU(5)model building, (2026), arXiv:2603.28406. 13

    work page arXiv 2026

  16. [16]

    Introduction to Seiberg-Witten Theory and its Stringy Origin

    Wolfgang Lerche,Introduction to Seiberg–Witten theory and its stringy origin, Nuclear Physics B Proceedings Supplements55(1997), no. 2, 83–117, arXiv:hep-th/9611190

    work page internal anchor Pith review Pith/arXiv arXiv 1997

  17. [17]

    Hiraku Nakajima and K¯ ota Yoshioka,Instanton counting on blowup. I. 4-dimensional pure gauge theory, Inventiones Mathematicae162(2005), 313–355, arXiv:math/0306198

    work page internal anchor Pith review Pith/arXiv arXiv 2005

  18. [18]

    Seiberg-Witten Prepotential From Instanton Counting

    Nikita A. Nekrasov,Seiberg–Witten prepotential from instanton counting, Advances in Theoretical and Mathematical Physics7(2003), 831–864, arXiv:hep-th/0206161

    work page internal anchor Pith review Pith/arXiv arXiv 2003

  19. [19]

    Seiberg-Witten Theory and Random Partitions

    Nikita A. Nekrasov and Andrei Okounkov,Seiberg–Witten theory and random partitions, The Unity of Mathematics, Progress in Mathematics, vol. 244, Birkhäuser, 2006, arXiv:hep-th/0306238, pp. 525–596

    work page internal anchor Pith review Pith/arXiv arXiv 2006

  20. [20]

    Paulson,The Riemann mapping theorem, Archive of Formal Proofs,https://isa-afp

    Lawrence C. Paulson,The Riemann mapping theorem, Archive of Formal Proofs,https://isa-afp. org/entries/Riemann_Mapping.html, 2016

    work page 2016

  21. [21]

    Monopole Condensation, And Confinement In N=2 Supersymmetric Yang-Mills Theory

    Nathan Seiberg and Edward Witten,Electric-magnetic duality, monopole condensation, and confinement in N = 2supersymmetric Yang–Mills theory, Nuclear Physics B426(1994), 19–52, Erratum: ibid. B430 (1994) 485–486; arXiv:hep-th/9407087

    work page internal anchor Pith review Pith/arXiv arXiv 1994

  22. [22]

    ,Monopoles, duality and chiral symmetry breaking inN = 2supersymmetric QCD, Nuclear Physics B431(1994), 484–550, arXiv:hep-th/9408099

    work page internal anchor Pith review Pith/arXiv arXiv 1994

  23. [23]

    Terence Tao,Machine-assisted proof, Notices of the American Mathematical Society72(2025), no. 1, 6–13

    work page 2025

  24. [24]

    The mathlib Community,The Lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp. 367–381

    work page 2020

  25. [25]

    HepLean: Digitalising high energy physics

    Joseph Tooby-Smith,HepLean: Digitalising high energy physics, Computer Physics Communications 308(2025), 109457, arXiv:2405.08863. The library continues as PhysLean

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  26. [26]

    ,A perspective on interactive theorem provers in physics, Advanced Science (2025), Motivates the open-source formalized-physics project PhysLean

    work page 2025

  27. [27]

    period frame⇒duality equivalence

    E. T. Whittaker and G. N. Watson,A course of modern analysis, 4th ed., Cambridge University Press, 1927. A The physics hypotheses (H0–H7) — predicates, not axioms The physical inputs arecontentful predicates and structures, they areassumed as hypotheses(bundled in IsPolarizedPeriodChart) by the results that use them, so they never enter the trusted base. ...

    work page 1927