The sl(2)\mathfrak{sl}(2) weight system at c=−3/32c=-3/32 extends to a graph 4-invariant

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.GT — Geometric Topologymath.RT — Representation Theory

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

We prove unconditionally the conjecture of Fomichev, Karev, Pavutnitskiy and Usanov that the specialization of the sl(2)\mathfrak{sl}(2) weight system at c=−3/32c=-3/32 extends to a 44-invariant of graphs. The extension is ξ(G)=(−32)−nSG(−2)\xi(G)=(-32)^{-n}S_G(-2), where SG(N)S_G(N) counts with signs the assignments of 22-element subsets of {1,…,N}\{1,\dots,N\} to the nn vertices of GG.

Provenance statement

The proofs, the text, the figures, the Lean 4 formalization and the Python, Julia, C and C++ programs were carried out by Deep Bhattacharjee with the help of AI assistance (Claude, Anthropic) in the Claude Code environment. The paper proves the conjecture of D. Fomichev, M. Karev, F. Pavutnitskiy and S. Usanov (arXiv:2607.24217, Section 4) that the sl(2) weight system specialised at c = -3/32 extends to a 4-invariant of graphs, with the explicit extension xi(G) = (-32)^{-n} S_G(-2): the chord element acts on Verma modules, the Verma modules of highest weights -1/2 and -3/2 are realised in the oscillator representation, the resulting scalar is a supertrace on the Weyl algebra computed by a Wick formula, the sum over matchings is a trace in a Clifford algebra, and the four-term relation follows from an involution on the assignments. Both parts of the conjecture, the four-term relation for xi and the identity w_D(-3/32) = xi(Gamma(D)) for every chord diagram D, are proved in Lean 4 with Mathlib (SL2W.main_theorem, 16 files, 4120 lines), depending only on the axioms propext, Classical.choice and Quot.sound, with no sorry, native_decide or added axiom; programs in Python, Julia, C and C++ check the theorem on all chord diagrams with at most six chords and reproduce the values tabulated by Fomichev et al. The binomial expansion of S_G(N) (part (a) of the main theorem) is proved by hand and not formalized. No statement rests on a floating-point computation. The earlier value c = 3/8 is due to Fomichev and Karev and to Yan, Deng and Jin and is credited to them. Both authors approved the final version. Tools used: Anthropic - Claude (Claude Code); Lean community - Lean 4 (v4.34.1) with Mathlib; Python; Julia; C; C++; shell. arXiv identifier: none (not posted on arXiv). Formalization: https://github.com/creelie/automatic-memory/blob/main/lean/SL2W/Main.lean (archived at Zenodo, release v2.0.0: https://doi.org/10.5281/zenodo.23384025)

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. M. Kontsevich, Vassiliev's knot invariants, in: I. M. Gel'fand Seminar, Vol. 16, Part 2 of Adv. Soviet Math., Amer. Math. Soc., Providence, RI, 1993, pp. 137--150. doi:10.1090/advsov/016.2/04 (https://doi.org/10.1090/advsov/016.2/04).DOI
  2. D. Bar-Natan, On the V assiliev knot invariants, Topology 34 (2) (1995) 423--472. doi:10.1016/0040-9383(95)93237-2 (https://doi.org/10.1016/0040-9383(95)93237-2).DOI
  3. S. Chmutov, S. Duzhin, J. Mostovoy, Introduction to V assiliev Knot Invariants, Cambridge University Press, Cambridge, 2012. doi:10.1017/CBO9781139107846 (https://doi.org/10.1017/CBO9781139107846).DOI
  4. S. Chmutov, S. Lando, Mutant knots and intersection graphs, Algebr. Geom. Topol. 7 (3) (2007) 1579--1598. doi:10.2140/agt.2007.7.1579 (https://doi.org/10.2140/agt.2007.7.1579).DOI
  5. S. K. Lando, On a H opf algebra in graph theory, J. Combin. Theory Ser. B 80 (1) (2000) 104--121. doi:10.1006/jctb.2000.1973 (https://doi.org/10.1006/jctb.2000.1973).DOI
  6. M. E. Kazarian, S. K. Lando, Weight systems and invariants of graphs and embedded graphs, Russian Math. Surveys 77 (5) (2022) 893--942. doi:10.4213/rm10054e (https://doi.org/10.4213/rm10054e).DOI
  7. E. Krasilnikov, An extension of the sl2\mathfrak{sl}_2 weight system to graphs with n≤8n \le 8 vertices, Arnold Math. J. 7 (2021) 609--618. doi:10.1007/s40598-021-00187-7 (https://doi.org/10.1007/s40598-021-00187-7).DOI
  8. D. Fomichev, M. Karev, F. Pavutnitskiy, S. Usanov, sl(2)\mathfrak{sl}(2) -weight system does not extend to a graph 4-invariant, arXiv:2607.24217, data: https://github.com/fomichev-d/sl2_at_-3_32 (2026).arXiv
  9. D. Fomichev, M. Karev, The sl(2)\mathfrak{sl}(2) -weight system at c=3/8c = 3/8 for graphs, European J. Combin. 127 (2025) 104160. doi:10.1016/j.ejc.2025.104160 (https://doi.org/10.1016/j.ejc.2025.104160).DOI
  10. Q. Yan, Q. Deng, X. Jin, Proof of a conjecture of F omichev and K arev, European J. Combin. 135 (2026) 104365. doi:10.1016/j.ejc.2026.104365 (https://doi.org/10.1016/j.ejc.2026.104365).DOI
Show all 18 referencesShow fewer references
  1. S. V. Chmutov, A. N. Varchenko, Remarks on the V assiliev knot invariants coming from sl2\mathfrak{sl}_2 , Topology 36 (1) (1997) 153--178. doi:10.1016/0040-9383(95)00071-2 (https://doi.org/10.1016/0040-9383(95)00071-2).DOI
  2. J. E. Humphreys, Representations of Semisimple L ie Algebras in the BGG Category O\mathcal{O} , Vol. 94 of Grad. Stud. Math., Amer. Math. Soc., Providence, RI, 2008. doi:10.1090/gsm/094 (https://doi.org/10.1090/gsm/094).DOI
  3. L. de Moura, S. Ullrich, The L ean 4 theorem prover and programming language, in: Automated Deduction -- CADE 28, Vol. 12699 of Lecture Notes in Comput. Sci., Springer, Cham, 2021, pp. 625--635. doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  4. The mathlib Community , The L ean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, New York, 2020, pp. 367--381. doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  5. D. Bhattacharjee, Establishing equivariant class [O][O] for hyperbolic groups, Asian Res. J. Math. 18 (11) (2022) 362--369. doi:10.9734/arjom/2022/v18i11615 (https://doi.org/10.9734/arjom/2022/v18i11615).DOI
  6. D. Bhattacharjee, U. Bhattacharya, Iterated nerve complexes for kk-fold sensor coverage, Preprints.org (2026). doi:10.20944/preprints202606.1351.v2 (https://doi.org/10.20944/preprints202606.1351.v2).DOI
  7. D. Bhattacharjee, Non-commutativity over canonical suspension η\eta for genus g≥1g\ge1 in hypercomplex structures for potential ρϕ\rho\phi, Asian Res. J. Math. 18 (11) (2022) 332--341. doi:10.9734/arjom/2022/v18i11607 (https://doi.org/10.9734/arjom/2022/v18i11607).DOI
  8. D. Bhattacharjee, U. Bhattacharya, The sl(2)\mathfrak{sl}(2) weight system at c=−3/32c=-3/32 extends to a graph 4-invariant: Lean 4 formalization and verification code, Zenodo (2026). doi: (https://doi.org/\zenodoID).link

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 17, 2026