Pith. sign in

REVIEW 3 major objections 6 minor 1 cited by

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

T0 review · 3 major / 6 minor · reviewed 2026-07-08 · glm-5.2

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Physics without proofs: machine-checking the Seiberg-Witten solution

desk verdict A genuine methodological contribution: formalizing a non-rigorous physics argument in Lean by separating named physical postulates from machine-checked mathematical consequences, applied to the Seiberg-Witten SU(2) solution. read the letter →

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

Michael R. Douglas This is my paper · ORCID
classification hep-thcs.LO MSC 14D0781T6068V20 PACS 11.15.-q11.30.Pb12.60.Jv
keywords Seiberg-WitteninteractivetheoremprovingLean4formalizationofphysicsN=2supersymmetrySU(2)super-Yang-MillsmodularlambdafunctionGamma(2)duality
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

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.

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.

Watch

Extended reading notes

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

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.

Editorial extensions

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.

Reading between the lines

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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

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 · score 1.0 of 10

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.

Assumptions & free parameters 0 free parameters · 7 assumptions · 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.

assumptions (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]).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean." pith.science (2026). https://pith.science/paper/ZJI4SAUU

@misc{pith2026260706379,
  author       = {Pith},
  title        = {Pith review of: Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZJI4SAUU}},
  note         = {Machine review of arXiv:2607.06379}
}
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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Algebraic versus physical uniqueness of MHV gravity numerators

    hep-th 2026-08 conditional novelty 7.0 of 10 partial

    Pair-zero and degree conditions admit extra six-dimensional hook solutions at seven points and a two-dimensional plane at eight; Bose symmetry and one normalized physical boundary condition single out the Hodges numerator.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages · cited by 1 Pith paper

  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 Pith review 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 Pith review 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 Pith review 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 Pith review 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 Pith review 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 Pith review arXiv 2006

Show all 27 references
  1. [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

    2022 arXiv

  2. [10]

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

    2011

  3. [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

    2026

  4. [12]

    81, Springer, 1981

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

    1981

  5. [13]

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

    1978

  6. [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

    1995 arXiv

  7. [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

    2026

  8. [16]

    2, 83–117, arXiv:hep-th/9611190

    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

    1997 arXiv

  9. [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

    2005 arXiv

  10. [18]

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

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

    2003 arXiv

  11. [19]

    Nekrasov and Andrei Okounkov,Seiberg–Witten theory and random partitions, The Unity of Mathematics, Progress in Mathematics, vol

    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

    2006 arXiv

  12. [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

    2016

  13. [21]

    B430 (1994) 485–486; arXiv:hep-th/9407087

    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

    1994 arXiv

  14. [22]

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

    1994 arXiv

  15. [23]

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

    2025

  16. [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

    2020

  17. [25]

    The library continues as PhysLean

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

    2025 arXiv

  18. [26]

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

    2025

  19. [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 IsPolarizedP...

    1927

Pith tools

Reviewed July 8, 2026 · model on record in the stance chip above.