Symplectic matrices have determinant 1

symplectic_matrix_det

Submitter: Kim Morrison.

Notes: §39 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. For any commutative ring R and 2n × 2n symplectic matrix A over R (A * J * Aᵀ = J with J = [[0, -I], [I, 0]]), det A = 1. Taking determinants of AᵀJA = J only forces (det A)² = 1; the sign requires the Pfaffian argument. Mathlib has `Matrix.symplecticGroup` and proves `symplectic_det` (IsUnit (det A)) but the equals-1 claim is an explicit TODO in Mathlib/LinearAlgebra/SymplecticGroup.lean; no formalization of the identity was found in any other proof assistant.

Source: Folklore (Pfaffian computation). Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Marked as an open TODO at the head of Mathlib/LinearAlgebra/SymplecticGroup.lean (rev 5450b53e5ddc).

Informal solution: Apply the Pfaffian: for any 2n × 2n matrix M and antisymmetric 2n × 2n matrix Ω, Pf(Mᵀ Ω M) = det(M) · Pf(Ω). With Ω = J (so Pf(J) ≠ 0) and Aᵀ J A = J for A ∈ Sp_{2n}(R), one gets Pf(J) = det(A) · Pf(J), hence det A = 1. (This requires the Pfaffian for matrices over a commutative ring R; the construction is purely algebraic.)

theorem declaration uses `sorry`symplectic_matrix_det {l R : Type*} [DecidableEq l] [Fintype l] [CommRing R]
    {A : Matrix (l ⊕ l) (l ⊕ l) R} (_hA : A ∈ Matrix.symplecticGroup l R) :
    A.det = 1 := byl:Type u_1R:Type u_2inst✝²:DecidableEq linst✝¹:Fintype linst✝:CommRing RA:Matrix (l ⊕ l) (l ⊕ l) R_hA:A ∈ symplecticGroup l R⊢ A.det = 1
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 25, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026

• @JohnEdwardJennings with Aristotle (Harmonic) on Jun 1, 2026